From a2e7e54d90c2b21ac6dbd9cc6bb9197aa96a930a Mon Sep 17 00:00:00 2001
From: gruninger <gruninger@mie.utoronto.ca>
Date: Mon, 7 Mar 2016 20:59:24 -0500
Subject: [PATCH] new hierarchies, theories, and  theorems related  to SUMO
 temporal concepts

---
 ontologies/sumo/sumo_temporalPart             | 259 +++++++++++++
 ontologies/sumo/sumo_time.clif                | 343 ++++++++++++++++++
 ontologies/sumo/sumo_timepoints               |  89 +++++
 ontologies/sumo/theorems/input/sumo_time.in   |  85 +++++
 ontologies/sumo/theorems/output/ex128-1.in    |  30 ++
 ontologies/sumo/theorems/output/ex128-1.model |  55 +++
 ontologies/sumo/theorems/output/ex128-2.in    |  27 ++
 ontologies/sumo/theorems/output/ex128-2.model |  49 +++
 ontologies/sumo/theorems/output/ex128-3.in    |  52 +++
 ontologies/sumo/theorems/output/ex128-3.model | 275 ++++++++++++++
 .../theorems/timepoints_entails/ex129-1.in    |  39 ++
 .../theorems/timepoints_entails/ex129-1.proof |  35 ++
 .../theorems/timepoints_entails/ex129-10.in   |  38 ++
 .../timepoints_entails/ex129-10.proof         |  43 +++
 .../theorems/timepoints_entails/ex129-2.in    |  39 ++
 .../theorems/timepoints_entails/ex129-2.proof |  26 ++
 .../theorems/timepoints_entails/ex129-3.in    |  39 ++
 .../theorems/timepoints_entails/ex129-3.proof |  39 ++
 .../theorems/timepoints_entails/ex129-4.in    |  38 ++
 .../theorems/timepoints_entails/ex129-4.proof |  43 +++
 .../theorems/timepoints_entails/ex129-5.in    |  38 ++
 .../theorems/timepoints_entails/ex129-5.proof |  28 ++
 .../theorems/timepoints_entails/ex129-6.in    |  38 ++
 .../theorems/timepoints_entails/ex129-6.proof |  35 ++
 .../theorems/timepoints_entails/ex129-7.in    |  38 ++
 .../theorems/timepoints_entails/ex129-7.proof |  35 ++
 .../theorems/timepoints_entails/ex129-8.in    |  38 ++
 .../theorems/timepoints_entails/ex129-8.proof |  33 ++
 .../theorems/timepoints_entails/ex129-9.in    |  38 ++
 .../theorems/timepoints_entails/ex129-9.proof |  33 ++
 .../sumo_timeintervals/mappings/delta.in      |  33 ++
 ontologies/sumo_timeintervals/mappings/pi.in  |  10 +
 .../sumo_timeintervals.clif                   |  56 +++
 .../sumo_ordered_timepoints.clif              |  55 +++
 34 files changed, 2151 insertions(+)
 create mode 100644 ontologies/sumo/sumo_temporalPart
 create mode 100644 ontologies/sumo/sumo_time.clif
 create mode 100644 ontologies/sumo/sumo_timepoints
 create mode 100644 ontologies/sumo/theorems/input/sumo_time.in
 create mode 100644 ontologies/sumo/theorems/output/ex128-1.in
 create mode 100644 ontologies/sumo/theorems/output/ex128-1.model
 create mode 100644 ontologies/sumo/theorems/output/ex128-2.in
 create mode 100644 ontologies/sumo/theorems/output/ex128-2.model
 create mode 100644 ontologies/sumo/theorems/output/ex128-3.in
 create mode 100644 ontologies/sumo/theorems/output/ex128-3.model
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-1.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-1.proof
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-10.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-10.proof
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-2.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-2.proof
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-3.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-3.proof
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-4.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-4.proof
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-5.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-5.proof
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-6.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-6.proof
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-7.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-7.proof
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-8.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-8.proof
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-9.in
 create mode 100644 ontologies/sumo/theorems/timepoints_entails/ex129-9.proof
 create mode 100644 ontologies/sumo_timeintervals/mappings/delta.in
 create mode 100644 ontologies/sumo_timeintervals/mappings/pi.in
 create mode 100644 ontologies/sumo_timeintervals/sumo_timeintervals.clif
 create mode 100644 ontologies/sumo_timepoints/sumo_ordered_timepoints.clif

diff --git a/ontologies/sumo/sumo_temporalPart b/ontologies/sumo/sumo_temporalPart
new file mode 100644
index 000000000..657cdd5a2
--- /dev/null
+++ b/ontologies/sumo/sumo_temporalPart
@@ -0,0 +1,259 @@
+
+(cl-text colore.oor.net/sumo/sumo_temporalPart
+
+(forall (x y)
+	(if	(and	(temporalPart x y)
+			(temporalPart y x))
+		(= x y)))
+
+(forall (x y z)
+	(if	(and	(temporalPart x y)
+			(temporalPart y z))
+		(temporalPart x z)))
+
+(forall (x y)
+	(if	(overlapsTemporally x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(overlapsTemporally x x)))
+
+(forall (x y)
+	(if	(overlapsTemporally x y)
+		(overlapsTemporally y x)))
+
+(forall (x y)
+	(iff	(overlapsTemporally x y)
+		(exists (z)
+			(and	(TimeInterval z)
+				(temporalPart z x)
+				(temporalPart z y)))))
+
+(forall (x y)
+	(if	(starts x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(starts x y)
+			(starts y z))
+		(starts x z)))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (starts x x))))
+
+(forall (x y)
+	(if	(starts x y)
+		(temporalPart x y)))
+
+(forall (x y)
+	(iff	(starts x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(before (EndFn x) (EndFn y))
+			(= (BeginFn x) (BeginFn y)))))
+
+(forall (x y)
+	(if	(finishes x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(finishes x y)
+			(finishes y z))
+		(finishes x z)))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (finishes x x))))
+
+(forall (x y)
+	(if	(finishes x y)
+		(temporalPart x y)))
+
+(forall (x y)
+	(iff	(finishes x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(before (BeginFn x) (BeginFn y))
+			(= (EndFn x) (EndFn y)))))
+
+(forall (x y)
+	(if	(during x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(during x y)
+			(during y z))
+		(during x z)))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (during x x))))
+
+(forall (x y)
+	(if	(during x y)
+		(temporalPart x y)))
+
+(forall (x y)
+	(if	(during x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(before (EndFn x) (EndFn y))
+			(before (BeginFn y) (BeginFn x)))))
+
+(forall (x y)
+	(if	(earlier x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(earlier x y)
+			(earlier y z))
+		(earlier x z)))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (earlier x x))))
+
+(forall (x y)
+	(iff	(earlier x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(before (EndFn x) (BeginFn y)))))
+
+(forall (x y)
+	(if	(meetsTemporally x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(meetsTemporally x y)
+			(meetsTemporally y z))
+		(not (meetsTemporally x z))))
+
+(forall (x y)
+	(if	(meetsTemporally x y)
+		(not (meetsTemporally y x))))
+
+(forall (x y)
+	(iff	(meetTemporally x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(= (EndFn x) (BeginFn y)))))
+
+(forall (x)
+	(TimeInterval x)
+	(temporalPart x x))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(Timeposition x)))
+
+(forall (x)
+	(if	(TimePoint x)
+		(Timeposition x)))
+
+(forall (x)
+	(if	(TimePosition x)
+		(or	(TimeInterval x)
+			(TimePoint x))))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (TimePoint x))))
+
+(forall (x y)
+	(if	(temporalPart x y)
+		(and	(TimePosition x)
+			(TimePosition y))))
+
+(forall (x)
+	(if	(TimePosition x)
+		(temporalPart x x)))
+
+(forall (x)
+	(if	(and	(temporalPart x y)
+			(temporalPart y x))
+		(= x y)))
+
+(forall (x y z)
+	(if	(and	(temporalPart x y)
+			(temporalPart y z))
+		(temporalPart x z)))
+
+(forall (x)
+	(if	(TimePoint x)
+		(exists (y)
+			(and	(TimeInterval y)
+				(temporalPart x y)))))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(exists (y)
+			(and	(TimePoint y)
+				(temporalPart y x)))))
+
+(forall (x y z t)
+	(if	(and	(TimePoint x)
+			(TimePoint y)
+			(TimeInterval z)
+			(= (TimeIntervalFn x y) z)
+			(TimePoint t))
+		(iff	(temporallyBetweenOrEqual x t y)
+			(temporalPart t z))))
+
+(forall (x y z)
+	(if	(and	(TimePoint x)
+			(TimePoint y)
+			(TimeInterval z)
+			(= (TimeIntervalFn x y) z))
+		(and	(= (BeginFn z) x)
+			(= (EndFn z) y))))
+
+(forall (x y z t)
+	(if	(and	(TimeInterval x)
+			(TimeInterval y)
+			(TimePoint z)
+			(TimePoint t)
+			(= (BeginFn x) z)
+			(= (BeginFn y) z)
+			(= (EndFn x) t)
+			(= (EndFn y) t))
+		(= x y)))
+
+(forall (x y)
+	(if	(and	(TimeInterval x)
+			(TimePoint y)
+			(= (BeginFn x) y))
+		(forall (z)
+			(if	(and	(temporalPart z x)
+					(TimePoint z)
+					(not (= z y)))
+				(before y z)))))
+
+(forall (x y)
+	(if	(and	(TimeInterval x)
+			(TimePoint y)
+			(= (EndFn x) y))
+		(forall (z)
+			(if	(and	(temporalPart z x)
+					(TimePoint z)
+					(not (= z y)))
+				(before z y)))))
+
+(forall (z u v)
+	(if	(and	(TimeInterval z)
+			(TimePoint u)
+			(TimePoint v)
+			(= (BeginFn z) u)
+			(= (EndFn z) v))
+		(before u v)))
+
+
+
+)
diff --git a/ontologies/sumo/sumo_time.clif b/ontologies/sumo/sumo_time.clif
new file mode 100644
index 000000000..4455a90d5
--- /dev/null
+++ b/ontologies/sumo/sumo_time.clif
@@ -0,0 +1,343 @@
+
+(cl-text colore.oor.net/sumo/sumo_time.clif
+
+(forall (x y)
+	(if	(beforeOrEqual x y)
+		(and	(TimePoint x)
+			(TimePoint y))))
+
+(forall (x)
+	(if	(TimePoint x)
+		(beforeOrEqual x x)))
+
+(forall (x y z)
+	(if	(and	(beforeOrEqual x y)
+			(beforeOrEqual y z))
+		(beforeOrEqual x z)))
+
+(forall (x y)
+	(if	(beforeOrEqual x y)
+		(before x y)))
+
+(forall (x y)
+	(if	(before x y)
+		(and	(TimePoint x)
+			(TimePoint y))))
+
+(forall (x)
+	(if	(TimePoint x)
+		(not (before x x))))
+
+(forall (x y z)
+	(if	(and	(before x y)
+			(before y z))
+		(before x z)))
+
+(forall (x y z)
+	(if	(temporallyBetween x y z)
+		(and	(TimePoint x)
+			(TimePoint y)
+			(TimePoint z))))
+
+(forall (x y z)
+	(if	(temporallyBetween x y z)
+		(temporallyBetweenOrEqual x y z)))
+
+(forall (x y z)
+	(iff	(temporallyBetween x y z)
+		(and	(before x y)
+			(before y z))))
+
+(forall (x y z)
+	(iff	(temporallyBetween x y z)
+		(and	(beforeOrEqual x y)
+			(beforeOrEqual y z))))
+
+(forall (x y z)
+	(if	(temporallyBetweenorEqual x y z)
+		(and	(TimePoint x)
+			(TimePoint y)
+			(TimePoint z))))
+
+(TimePoint PositiveInfinity)
+
+(TimePoint NegativeInfinity)
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x PositiveInfinity)))
+		(before x PositiveInfinity)))
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x NegativeInfinity)))
+		(before NegativeInfinity x)))
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x PositiveInfinity)))
+		(exists (y)
+			(temporallyBetween x y PositiveInfinity))))
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x NegativeInfinity)))
+		(exists (y)
+			(temporallyBetween NegativeInfinity y x))))
+
+(forall (x y)
+	(if	(and	(temporalPart x y)
+			(temporalPart y x))
+		(= x y)))
+
+(forall (x y z)
+	(if	(and	(temporalPart x y)
+			(temporalPart y z))
+		(temporalPart x z)))
+
+(forall (x y)
+	(if	(overlapsTemporally x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(overlapsTemporally x x)))
+
+(forall (x y)
+	(if	(overlapsTemporally x y)
+		(overlapsTemporally y x)))
+
+(forall (x y)
+	(iff	(overlapsTemporally x y)
+		(exists (z)
+			(and	(TimeInterval z)
+				(temporalPart z x)
+				(temporalPart z y)))))
+
+(forall (x y)
+	(if	(starts x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(starts x y)
+			(starts y z))
+		(starts x z)))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (starts x x))))
+
+(forall (x y)
+	(if	(starts x y)
+		(temporalPart x y)))
+
+(forall (x y)
+	(iff	(starts x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(before (EndFn x) (EndFn y))
+			(= (BeginFn x) (BeginFn y)))))
+
+(forall (x y)
+	(if	(finishes x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(finishes x y)
+			(finishes y z))
+		(finishes x z)))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (finishes x x))))
+
+(forall (x y)
+	(if	(finishes x y)
+		(temporalPart x y)))
+
+(forall (x y)
+	(iff	(finishes x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(before (BeginFn x) (BeginFn y))
+			(= (EndFn x) (EndFn y)))))
+
+(forall (x y)
+	(if	(during x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(during x y)
+			(during y z))
+		(during x z)))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (during x x))))
+
+(forall (x y)
+	(if	(during x y)
+		(temporalPart x y)))
+
+(forall (x y)
+	(if	(during x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(before (EndFn x) (EndFn y))
+			(before (BeginFn y) (BeginFn x)))))
+
+(forall (x y)
+	(if	(earlier x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(earlier x y)
+			(earlier y z))
+		(earlier x z)))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (earlier x x))))
+
+(forall (x y)
+	(iff	(earlier x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(before (EndFn x) (BeginFn y)))))
+
+(forall (x y)
+	(if	(meetsTemporally x y)
+		(and	(TimeInterval x)
+			(TimeInterval y))))
+
+(forall (x y z)
+	(if	(and	(meetsTemporally x y)
+			(meetsTemporally y z))
+		(not (meetsTemporally x z))))
+
+(forall (x y)
+	(if	(meetsTemporally x y)
+		(not (meetsTemporally y x))))
+
+(forall (x y)
+	(iff	(meetTemporally x y)
+		(and	(TimeInterval x)
+			(TimeInterval y)
+			(= (EndFn x) (BeginFn y)))))
+
+(forall (x)
+	(TimeInterval x)
+	(temporalPart x x))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(Timeposition x)))
+
+(forall (x)
+	(if	(TimePoint x)
+		(Timeposition x)))
+
+(forall (x)
+	(if	(TimePosition x)
+		(or	(TimeInterval x)
+			(TimePoint x))))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (TimePoint x))))
+
+(forall (x y)
+	(if	(temporalPart x y)
+		(and	(TimePosition x)
+			(TimePosition y))))
+
+(forall (x)
+	(if	(TimePosition x)
+		(temporalPart x x)))
+
+(forall (x)
+	(if	(and	(temporalPart x y)
+			(temporalPart y x))
+		(= x y)))
+
+(forall (x y z)
+	(if	(and	(temporalPart x y)
+			(temporalPart y z))
+		(temporalPart x z)))
+
+(forall (x)
+	(if	(TimePoint x)
+		(exists (y)
+			(and	(TimeInterval y)
+				(temporalPart x y)))))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(exists (y)
+			(and	(TimePoint y)
+				(temporalPart y x)))))
+
+(forall (x y z t)
+	(if	(and	(TimePoint x)
+			(TimePoint y)
+			(TimeInterval z)
+			(= (TimeIntervalFn x y) z)
+			(TimePoint t))
+		(iff	(temporallyBetweenOrEqual x t y)
+			(temporalPart t z))))
+
+(forall (x y z)
+	(if	(and	(TimePoint x)
+			(TimePoint y)
+			(TimeInterval z)
+			(= (TimeIntervalFn x y) z))
+		(and	(= (BeginFn z) x)
+			(= (EndFn z) y))))
+
+(forall (x y z t)
+	(if	(and	(TimeInterval x)
+			(TimeInterval y)
+			(TimePoint z)
+			(TimePoint t)
+			(= (BeginFn x) z)
+			(= (BeginFn y) z)
+			(= (EndFn x) t)
+			(= (EndFn y) t))
+		(= x y)))
+
+(forall (x y)
+	(if	(and	(TimeInterval x)
+			(TimePoint y)
+			(= (BeginFn x) y))
+		(forall (z)
+			(if	(and	(temporalPart z x)
+					(TimePoint z)
+					(not (= z y)))
+				(before y z)))))
+
+(forall (x y)
+	(if	(and	(TimeInterval x)
+			(TimePoint y)
+			(= (EndFn x) y))
+		(forall (z)
+			(if	(and	(temporalPart z x)
+					(TimePoint z)
+					(not (= z y)))
+				(before z y)))))
+
+(forall (z u v)
+	(if	(and	(TimeInterval z)
+			(TimePoint u)
+			(TimePoint v)
+			(= (BeginFn z) u)
+			(= (EndFn z) v))
+		(before u v)))
+
+
+
+)
diff --git a/ontologies/sumo/sumo_timepoints b/ontologies/sumo/sumo_timepoints
new file mode 100644
index 000000000..e2ec9e685
--- /dev/null
+++ b/ontologies/sumo/sumo_timepoints
@@ -0,0 +1,89 @@
+
+(cl-text colore.oor.net/sumo/sumo_timepoints.clif
+
+(forall (x y)
+	(if	(beforeOrEqual x y)
+		(and	(TimePoint x)
+			(TimePoint y))))
+
+(forall (x)
+	(if	(TimePoint x)
+		(beforeOrEqual x x)))
+
+(forall (x y z)
+	(if	(and	(beforeOrEqual x y)
+			(beforeOrEqual y z))
+		(beforeOrEqual x z)))
+
+(forall (x y)
+	(if	(beforeOrEqual x y)
+		(before x y)))
+
+(forall (x y)
+	(if	(before x y)
+		(and	(TimePoint x)
+			(TimePoint y))))
+
+(forall (x)
+	(if	(TimePoint x)
+		(not (before x x))))
+
+(forall (x y z)
+	(if	(and	(before x y)
+			(before y z))
+		(before x z)))
+
+(forall (x y z)
+	(if	(temporallyBetween x y z)
+		(and	(TimePoint x)
+			(TimePoint y)
+			(TimePoint z))))
+
+(forall (x y z)
+	(if	(temporallyBetween x y z)
+		(temporallyBetweenOrEqual x y z)))
+
+(forall (x y z)
+	(iff	(temporallyBetween x y z)
+		(and	(before x y)
+			(before y z))))
+
+(forall (x y z)
+	(iff	(temporallyBetween x y z)
+		(and	(beforeOrEqual x y)
+			(beforeOrEqual y z))))
+
+(forall (x y z)
+	(if	(temporallyBetweenorEqual x y z)
+		(and	(TimePoint x)
+			(TimePoint y)
+			(TimePoint z))))
+
+(TimePoint PositiveInfinity)
+
+(TimePoint NegativeInfinity)
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x PositiveInfinity)))
+		(before x PositiveInfinity)))
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x NegativeInfinity)))
+		(before NegativeInfinity x)))
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x PositiveInfinity)))
+		(exists (y)
+			(temporallyBetween x y PositiveInfinity))))
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x NegativeInfinity)))
+		(exists (y)
+			(temporallyBetween NegativeInfinity y x))))
+
+
+)
diff --git a/ontologies/sumo/theorems/input/sumo_time.in b/ontologies/sumo/theorems/input/sumo_time.in
new file mode 100644
index 000000000..2a90adeec
--- /dev/null
+++ b/ontologies/sumo/theorems/input/sumo_time.in
@@ -0,0 +1,85 @@
+formulas(assumptions).
+
+%-------------------------------------------------------------------------------------------------
+% Ordered TimePoints
+%-------------------------------------------------------------------------------------------------
+all x all y (beforeOrEqual(x,y)-> TimePoint(x) & TimePoint(y)).%1
+all x (TimePoint(x)-> beforeOrEqual(x,x)).%2
+all x all y (beforeOrEqual(x,y) & beforeOrEqual(y,x)) -> (x=y).%3
+all x all y all z ((beforeOrEqual(x,y) & beforeOrEqual(y,z))-> beforeOrEqual(x,z)).%4
+all x all y (beforeOrEqual(x,y)->(before(x,y) | (x=y))).%5
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y (before(x,y)-> beforeOrEqual(x,y)).%10
+all x all y all z (temporallyBetween(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z)).%11
+all x all y all z (temporallyBetween(x,y,z)-> temporallyBetweenOrEqual(x,y,z)).%12
+all y all z all x (temporallyBetween(x,y,z)<->(before(x,y) & before(y,z))).%13 
+all y all z all x (temporallyBetweenOrEqual(x,y,z)<->(beforeOrEqual(x,y) & beforeOrEqual(y,z))).%14
+all x all y all z (temporallyBetweenOrEqual(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z)).%15
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+%-------------------------------------------------------------------------------------------------
+% Intervals Mereology
+%-------------------------------------------------------------------------------------------------
+all x all y ((temporalPart(x,y) & temporalPart(y,x)) -> (x=y)). %22
+all x all y all z ((temporalPart(x,y) & temporalPart(y,z))-> temporalPart(x,z)). %23
+all x all y (overlapsTemporally(x,y)-> TimeInterval(x) & TimeInterval(y)).%24
+all x (TimeInterval(x)-> overlapsTemporally(x,x)). %25  
+all x all y (overlapsTemporally(x,y)-> overlapsTemporally(y,x)).%26
+all x all y (overlapsTemporally(x,y)<->(exists z (TimeInterval(z) & temporalPart(z,x) & temporalPart(z,y)))).%27->
+all x all y (starts(x,y)-> TimeInterval(x) & TimeInterval(y)).%28
+all x all y all z ((starts(x,y) & starts(y,z))-> starts(x,z)).%29
+all x (TimeInterval(x)->(-(starts(x,x)))).  %30
+all x all y (starts(x,y)-> temporalPart(x,y)).%31
+all x all y (starts(x,y) <-> (TimeInterval(x) & TimeInterval(y) & (BeginFn(x)=BeginFn(y))
+& before(EndFn(x),EndFn(y)))).
+all x all y (finishes(x,y)-> TimeInterval(x) & TimeInterval(y)). %32
+all x all y all z ((finishes(x,y) & finishes(y,z))-> finishes(x,z)).%33
+all x (TimeInterval(x)->(-(finishes(x,x)))). %34
+all x all y (finishes(x,y)-> temporalPart(x,y)).%35
+all x all y (finishes(x,y) <-> (TimeInterval(x) & TimeInterval(y) & before(BeginFn(x),BeginFn(y))
+& (EndFn(x)=EndFn(y)))).
+all x all y (during(x,y)-> TimeInterval(x) & TimeInterval(y)).%36 
+all x all y all z ((during(x,y) & during(y,z))-> during(x,z)).%37
+all x (TimeInterval(x)->(-(during(x,x)))).%38
+all x all y (during(x,y)-> temporalPart(x,y)). %39 
+all x all y (during(x,y)-> overlapsTemporally(x,y)). %40
+all x all y (during(x,y) -> (TimeInterval(x) & TimeInterval(y) & before(BeginFn(y),BeginFn(x))
+& before(EndFn(x),EndFn(y)))).
+all x all y (earlier(x,y)-> TimeInterval(x) & TimeInterval(y)). %41
+all x all y all z ((earlier(x,y) & earlier(y,z))-> earlier(x,z)).%42
+all x (TimeInterval(x)->(-(earlier(x,x)))).  %43
+all x all y (earlier(x,y) <-> (TimeInterval(x) & TimeInterval(y) & before(EndFn(x),BeginFn(y)))).
+all x all y (meetsTemporally(x,y)-> TimeInterval(x) & TimeInterval(y)).%44
+all x all y (meetsTemporally(x,y)-> -(meetsTemporally(y,x))).%45
+all x all y all z ((meetsTemporally(x,y) & meetsTemporally(y,z))-> -meetsTemporally(x,z)).%46
+all x all y (meetsTemporally(x,y) <-> (TimeInterval(x) & TimeInterval(y) & (EndFn(x)=BeginFn(y)))).
+
+all x (TimeInterval(x)-> temporalPart(x,x)). %47
+
+%-------------------------------------------------------------------------------------------------
+% Intervals and Points Mereology
+%-------------------------------------------------------------------------------------------------
+all x (TimeInterval(x)-> TimePosition(x)).%48
+all x (TimePoint(x)-> TimePosition(x)).%49
+all x (TimePosition(x)-> TimeInterval(x) | TimePoint(x)).%50
+all x (TimeInterval(x)-> -(TimePoint(x))).%51
+all x all y (temporalPart(x,y)-> TimePosition(x) & TimePosition(y)).%52
+all x (TimePosition(x)-> temporalPart(x,x)). %53
+all x (TimePoint(x) ->(exists y (TimeInterval(y) & temporalPart(x,y)))). %55
+all x (TimeInterval(x)->(exists y (TimePoint(y) & temporalPart(y,x)))). %56
+all x all y all z all t (TimePoint(x) & TimePoint(y) & TimeInterval(z) & (TimeIntervalFn(x,y)=z) & TimePoint(t)-> (temporallyBetweenOrEqual(x,t,y)<->temporalPart(t,z))).%57 
+all x all y all z (TimePoint(x) & TimePoint(y) & TimeInterval(z) & (TimeIntervalFn(x,y)=z)->(BeginFn(z)=x) & (EndFn(z)=y)).%58
+all x all y all z all t(TimeInterval(x) & TimeInterval(y) & TimePoint(z) & TimePoint(t) ->
+((BeginFn(x)=z) & (BeginFn(y)=z) & (EndFn(x)=t) & (EndFn(y)=t)-> (x=y))).%59
+all x all y (TimeInterval(x) & TimePoint(y)  &(BeginFn(x)=y) -> all z(temporalPart(z,x) & TimePoint(z) & -(z=y)->before(y,z))).%60
+all x all y (TimeInterval(x) & TimePoint(y)  &(EndFn(x)=y) -> all z(temporalPart(z,x) & TimePoint(z) & -(z=y)->before(z,y))).%61
+all z all u all v(TimeInterval(z) & TimePoint(u) & TimePoint(v)-> ((BeginFn(z)=u) & (EndFn(z)=v)-> before(u,v))).%62
+all x (TimePosition(x)).%68
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/output/ex128-1.in b/ontologies/sumo/theorems/output/ex128-1.in
new file mode 100644
index 000000000..c14eff87e
--- /dev/null
+++ b/ontologies/sumo/theorems/output/ex128-1.in
@@ -0,0 +1,30 @@
+formulas(assumptions).
+
+%-------------------------------------------------------------------------------------------------
+% Ordered TimePoints
+%-------------------------------------------------------------------------------------------------
+all x all y (beforeOrEqual(x,y)-> TimePoint(x) & TimePoint(y)).%1
+all x (TimePoint(x)-> beforeOrEqual(x,x)).%2
+all x all y (beforeOrEqual(x,y) & beforeOrEqual(y,x)) -> (x=y).%3
+all x all y all z ((beforeOrEqual(x,y) & beforeOrEqual(y,z))-> beforeOrEqual(x,z)).%4
+all x all y (beforeOrEqual(x,y)->(before(x,y) | (x=y))).%5
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y (TimePoint(x) & TimePoint(y) -> (before(x,y) | before(y,x) | (x=y))).%9
+all x all y (before(x,y)-> beforeOrEqual(x,y)).%10
+all x all y all z (temporallyBetween(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z)).%11
+all x all y all z (temporallyBetween(x,y,z)-> temporallyBetweenOrEqual(x,y,z)).%12
+all y all z all x (temporallyBetween(x,y,z)<->(before(x,y) & before(y,z))).%13 
+all y all z all x (temporallyBetweenOrEqual(x,y,z)<->(beforeOrEqual(x,y) & beforeOrEqual(y,z))).%14
+all x all y all z (temporallyBetweenOrEqual(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z)).%15
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(PositiveInfinity = NegativeInfinity).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/output/ex128-1.model b/ontologies/sumo/theorems/output/ex128-1.model
new file mode 100644
index 000000000..a297b0ac1
--- /dev/null
+++ b/ontologies/sumo/theorems/output/ex128-1.model
@@ -0,0 +1,55 @@
+% number = 1
+% seconds = 0
+
+% Interpretation of size 2
+
+NegativeInfinity = 0.
+
+PositiveInfinity = 0.
+
+f3(0) = 0.
+f3(1) = 0.
+
+f4(0) = 0.
+f4(1) = 0.
+
+f1(0,0) = 0.
+f1(0,1) = 0.
+f1(1,0) = 0.
+f1(1,1) = 0.
+
+f2(0,0) = 0.
+f2(0,1) = 1.
+f2(1,0) = 1.
+f2(1,1) = 0.
+
+  TimePoint(0).
+- TimePoint(1).
+
+- before(0,0).
+- before(0,1).
+- before(1,0).
+- before(1,1).
+
+  beforeOrEqual(0,0).
+- beforeOrEqual(0,1).
+- beforeOrEqual(1,0).
+- beforeOrEqual(1,1).
+
+- temporallyBetween(0,0,0).
+- temporallyBetween(0,0,1).
+- temporallyBetween(0,1,0).
+- temporallyBetween(0,1,1).
+- temporallyBetween(1,0,0).
+- temporallyBetween(1,0,1).
+- temporallyBetween(1,1,0).
+- temporallyBetween(1,1,1).
+
+  temporallyBetweenOrEqual(0,0,0).
+- temporallyBetweenOrEqual(0,0,1).
+- temporallyBetweenOrEqual(0,1,0).
+- temporallyBetweenOrEqual(0,1,1).
+- temporallyBetweenOrEqual(1,0,0).
+- temporallyBetweenOrEqual(1,0,1).
+- temporallyBetweenOrEqual(1,1,0).
+- temporallyBetweenOrEqual(1,1,1).
diff --git a/ontologies/sumo/theorems/output/ex128-2.in b/ontologies/sumo/theorems/output/ex128-2.in
new file mode 100644
index 000000000..e21439608
--- /dev/null
+++ b/ontologies/sumo/theorems/output/ex128-2.in
@@ -0,0 +1,27 @@
+formulas(assumptions).
+
+%-------------------------------------------------------------------------------------------------
+% Ordered TimePoints
+%-------------------------------------------------------------------------------------------------
+all x all y (beforeOrEqual(x,y)-> TimePoint(x) & TimePoint(y)).%1
+all x (TimePoint(x)-> beforeOrEqual(x,x)).%2
+all x all y (beforeOrEqual(x,y) & beforeOrEqual(y,x)) -> (x=y).%3
+all x all y all z ((beforeOrEqual(x,y) & beforeOrEqual(y,z))-> beforeOrEqual(x,z)).%4
+all x all y (beforeOrEqual(x,y)->(before(x,y) | (x=y))).%5
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y (before(x,y)-> beforeOrEqual(x,y)).%10
+all x all y all z (temporallyBetween(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z)).%11
+all x all y all z (temporallyBetween(x,y,z)-> temporallyBetweenOrEqual(x,y,z)).%12
+all y all z all x (temporallyBetween(x,y,z)<->(before(x,y) & before(y,z))).%13 
+all y all z all x (temporallyBetweenOrEqual(x,y,z)<->(beforeOrEqual(x,y) & beforeOrEqual(y,z))).%14
+all x all y all z (temporallyBetweenOrEqual(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z)).%15
+
+-(all t1 all t2
+	((TimePoint(t1)
+	& TimePoint(t2))
+	->
+	(before(t1,t2) | before(t2,t1) | (t1=t2)))).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/output/ex128-2.model b/ontologies/sumo/theorems/output/ex128-2.model
new file mode 100644
index 000000000..6ec011a6a
--- /dev/null
+++ b/ontologies/sumo/theorems/output/ex128-2.model
@@ -0,0 +1,49 @@
+% number = 1
+% seconds = 0
+
+% Interpretation of size 2
+
+c1 = 0.
+
+c2 = 1.
+
+f1(0,0) = 0.
+f1(0,1) = 0.
+f1(1,0) = 0.
+f1(1,1) = 0.
+
+f2(0,0) = 0.
+f2(0,1) = 1.
+f2(1,0) = 1.
+f2(1,1) = 0.
+
+  TimePoint(0).
+  TimePoint(1).
+
+- before(0,0).
+- before(0,1).
+- before(1,0).
+- before(1,1).
+
+  beforeOrEqual(0,0).
+- beforeOrEqual(0,1).
+- beforeOrEqual(1,0).
+  beforeOrEqual(1,1).
+
+- temporallyBetween(0,0,0).
+- temporallyBetween(0,0,1).
+- temporallyBetween(0,1,0).
+- temporallyBetween(0,1,1).
+- temporallyBetween(1,0,0).
+- temporallyBetween(1,0,1).
+- temporallyBetween(1,1,0).
+- temporallyBetween(1,1,1).
+
+  temporallyBetweenOrEqual(0,0,0).
+- temporallyBetweenOrEqual(0,0,1).
+- temporallyBetweenOrEqual(0,1,0).
+- temporallyBetweenOrEqual(0,1,1).
+- temporallyBetweenOrEqual(1,0,0).
+- temporallyBetweenOrEqual(1,0,1).
+- temporallyBetweenOrEqual(1,1,0).
+  temporallyBetweenOrEqual(1,1,1).
diff --git a/ontologies/sumo/theorems/output/ex128-3.in b/ontologies/sumo/theorems/output/ex128-3.in
new file mode 100644
index 000000000..c3bb84cd1
--- /dev/null
+++ b/ontologies/sumo/theorems/output/ex128-3.in
@@ -0,0 +1,52 @@
+formulas(assumptions).
+
+%-------------------------------------------------------------------------------------------------
+% Ordered TimePoints
+%-------------------------------------------------------------------------------------------------
+all x all y (beforeOrEqual(x,y)-> TimePoint(x) & TimePoint(y)).%1
+all x (TimePoint(x)-> beforeOrEqual(x,x)).%2
+all x all y (beforeOrEqual(x,y) & beforeOrEqual(y,x)) -> (x=y).%3
+all x all y all z ((beforeOrEqual(x,y) & beforeOrEqual(y,z))-> beforeOrEqual(x,z)).%4
+all x all y (beforeOrEqual(x,y)->(before(x,y) | (x=y))).%5
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y (before(x,y)-> beforeOrEqual(x,y)).%10
+all x all y all z (temporallyBetween(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z)).%11
+all x all y all z (temporallyBetween(x,y,z)-> temporallyBetweenOrEqual(x,y,z)).%12
+all y all z all x (temporallyBetween(x,y,z)<->(before(x,y) & before(y,z))).%13 
+all y all z all x (temporallyBetweenOrEqual(x,y,z)<->(beforeOrEqual(x,y) & beforeOrEqual(y,z))).%14
+all x all y all z (temporallyBetweenOrEqual(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z)).%15
+%-------------------------------------------------------------------------------------------------
+% Intervals Mereology
+%-------------------------------------------------------------------------------------------------
+all x all y ((temporalPart(x,y) & temporalPart(y,x)) -> (x=y)). %22
+all x all y all z ((temporalPart(x,y) & temporalPart(y,z))-> temporalPart(x,z)). %23
+all x (TimeInterval(x)-> temporalPart(x,x)). %47
+
+%-------------------------------------------------------------------------------------------------
+% Intervals and Points Mereology
+%-------------------------------------------------------------------------------------------------
+all x (TimeInterval(x)-> TimePosition(x)).%48
+all x (TimePoint(x)-> TimePosition(x)).%49
+all x (TimePosition(x)-> TimeInterval(x) | TimePoint(x)).%50
+all x (TimeInterval(x)-> -(TimePoint(x))).%51
+all x all y (temporalPart(x,y)-> TimePosition(x) & TimePosition(y)).%52
+all x (TimePosition(x)-> temporalPart(x,x)). %53
+all x (TimePoint(x) ->(exists y (TimeInterval(y) & temporalPart(x,y)))). %55
+all x (TimeInterval(x)->(exists y (TimePoint(y) & temporalPart(y,x)))). %56
+all x all y all z all t (TimePoint(x) & TimePoint(y) & TimeInterval(z) & (TimeIntervalFn(x,y)=z) & TimePoint(t)-> (temporallyBetweenOrEqual(x,t,y)<->temporalPart(t,z))).%57 
+all x all y all z (TimePoint(x) & TimePoint(y) & TimeInterval(z) & (TimeIntervalFn(x,y)=z)->(BeginFn(z)=x) & (EndFn(z)=y)).%58
+all x all y all z all t(TimeInterval(x) & TimeInterval(y) & TimePoint(z) & TimePoint(t) ->
+((BeginFn(x)=z) & (BeginFn(y)=z) & (EndFn(x)=t) & (EndFn(y)=t)-> (x=y))).%59
+all x all y (TimeInterval(x) & TimePoint(y)  &(BeginFn(x)=y) -> all z(temporalPart(z,x) & TimePoint(z) & -(z=y)->before(y,z))).%60
+all x all y (TimeInterval(x) & TimePoint(y)  &(EndFn(x)=y) -> all z(temporalPart(z,x) & TimePoint(z) & -(z=y)->before(z,y))).%61
+all z all u all v(TimeInterval(z) & TimePoint(u) & TimePoint(v)-> ((BeginFn(z)=u) & (EndFn(z)=v)-> before(u,v))).%62
+all x (TimePosition(x)).%68
+
+(exists x exists y
+	(TimePoint(x)
+	& TimeInterval(y)
+	& temporalPart(y,x))).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/output/ex128-3.model b/ontologies/sumo/theorems/output/ex128-3.model
new file mode 100644
index 000000000..17e720b2d
--- /dev/null
+++ b/ontologies/sumo/theorems/output/ex128-3.model
@@ -0,0 +1,275 @@
+% number = 1
+% seconds = 0
+
+% Interpretation of size 4
+
+c1 = 0.
+
+c2 = 1.
+
+BeginFn(0) = 0.
+BeginFn(1) = 0.
+BeginFn(2) = 0.
+BeginFn(3) = 0.
+
+EndFn(0) = 0.
+EndFn(1) = 1.
+EndFn(2) = 1.
+EndFn(3) = 0.
+
+f3(0) = 2.
+f3(1) = 0.
+f3(2) = 0.
+f3(3) = 1.
+
+f4(0) = 0.
+f4(1) = 3.
+f4(2) = 0.
+f4(3) = 0.
+
+TimeIntervalFn(0,0) = 0.
+TimeIntervalFn(0,1) = 0.
+TimeIntervalFn(0,2) = 0.
+TimeIntervalFn(0,3) = 0.
+TimeIntervalFn(1,0) = 0.
+TimeIntervalFn(1,1) = 0.
+TimeIntervalFn(1,2) = 0.
+TimeIntervalFn(1,3) = 0.
+TimeIntervalFn(2,0) = 0.
+TimeIntervalFn(2,1) = 0.
+TimeIntervalFn(2,2) = 0.
+TimeIntervalFn(2,3) = 0.
+TimeIntervalFn(3,0) = 0.
+TimeIntervalFn(3,1) = 0.
+TimeIntervalFn(3,2) = 0.
+TimeIntervalFn(3,3) = 0.
+
+f1(0,0) = 0.
+f1(0,1) = 0.
+f1(0,2) = 0.
+f1(0,3) = 0.
+f1(1,0) = 0.
+f1(1,1) = 0.
+f1(1,2) = 0.
+f1(1,3) = 0.
+f1(2,0) = 0.
+f1(2,1) = 0.
+f1(2,2) = 0.
+f1(2,3) = 0.
+f1(3,0) = 0.
+f1(3,1) = 0.
+f1(3,2) = 0.
+f1(3,3) = 0.
+
+f2(0,0) = 0.
+f2(0,1) = 1.
+f2(0,2) = 1.
+f2(0,3) = 1.
+f2(1,0) = 1.
+f2(1,1) = 0.
+f2(1,2) = 1.
+f2(1,3) = 1.
+f2(2,0) = 1.
+f2(2,1) = 1.
+f2(2,2) = 0.
+f2(2,3) = 1.
+f2(3,0) = 1.
+f2(3,1) = 1.
+f2(3,2) = 1.
+f2(3,3) = 0.
+
+- TimeInterval(0).
+  TimeInterval(1).
+  TimeInterval(2).
+- TimeInterval(3).
+
+  TimePoint(0).
+- TimePoint(1).
+- TimePoint(2).
+  TimePoint(3).
+
+  TimePosition(0).
+  TimePosition(1).
+  TimePosition(2).
+  TimePosition(3).
+
+- before(0,0).
+- before(0,1).
+- before(0,2).
+  before(0,3).
+- before(1,0).
+- before(1,1).
+- before(1,2).
+- before(1,3).
+- before(2,0).
+- before(2,1).
+- before(2,2).
+- before(2,3).
+- before(3,0).
+- before(3,1).
+- before(3,2).
+- before(3,3).
+
+  beforeOrEqual(0,0).
+- beforeOrEqual(0,1).
+- beforeOrEqual(0,2).
+  beforeOrEqual(0,3).
+- beforeOrEqual(1,0).
+- beforeOrEqual(1,1).
+- beforeOrEqual(1,2).
+- beforeOrEqual(1,3).
+- beforeOrEqual(2,0).
+- beforeOrEqual(2,1).
+- beforeOrEqual(2,2).
+- beforeOrEqual(2,3).
+- beforeOrEqual(3,0).
+- beforeOrEqual(3,1).
+- beforeOrEqual(3,2).
+  beforeOrEqual(3,3).
+
+  temporalPart(0,0).
+- temporalPart(0,1).
+  temporalPart(0,2).
+- temporalPart(0,3).
+  temporalPart(1,0).
+  temporalPart(1,1).
+  temporalPart(1,2).
+- temporalPart(1,3).
+- temporalPart(2,0).
+- temporalPart(2,1).
+  temporalPart(2,2).
+- temporalPart(2,3).
+  temporalPart(3,0).
+  temporalPart(3,1).
+  temporalPart(3,2).
+  temporalPart(3,3).
+
+- temporallyBetween(0,0,0).
+- temporallyBetween(0,0,1).
+- temporallyBetween(0,0,2).
+- temporallyBetween(0,0,3).
+- temporallyBetween(0,1,0).
+- temporallyBetween(0,1,1).
+- temporallyBetween(0,1,2).
+- temporallyBetween(0,1,3).
+- temporallyBetween(0,2,0).
+- temporallyBetween(0,2,1).
+- temporallyBetween(0,2,2).
+- temporallyBetween(0,2,3).
+- temporallyBetween(0,3,0).
+- temporallyBetween(0,3,1).
+- temporallyBetween(0,3,2).
+- temporallyBetween(0,3,3).
+- temporallyBetween(1,0,0).
+- temporallyBetween(1,0,1).
+- temporallyBetween(1,0,2).
+- temporallyBetween(1,0,3).
+- temporallyBetween(1,1,0).
+- temporallyBetween(1,1,1).
+- temporallyBetween(1,1,2).
+- temporallyBetween(1,1,3).
+- temporallyBetween(1,2,0).
+- temporallyBetween(1,2,1).
+- temporallyBetween(1,2,2).
+- temporallyBetween(1,2,3).
+- temporallyBetween(1,3,0).
+- temporallyBetween(1,3,1).
+- temporallyBetween(1,3,2).
+- temporallyBetween(1,3,3).
+- temporallyBetween(2,0,0).
+- temporallyBetween(2,0,1).
+- temporallyBetween(2,0,2).
+- temporallyBetween(2,0,3).
+- temporallyBetween(2,1,0).
+- temporallyBetween(2,1,1).
+- temporallyBetween(2,1,2).
+- temporallyBetween(2,1,3).
+- temporallyBetween(2,2,0).
+- temporallyBetween(2,2,1).
+- temporallyBetween(2,2,2).
+- temporallyBetween(2,2,3).
+- temporallyBetween(2,3,0).
+- temporallyBetween(2,3,1).
+- temporallyBetween(2,3,2).
+- temporallyBetween(2,3,3).
+- temporallyBetween(3,0,0).
+- temporallyBetween(3,0,1).
+- temporallyBetween(3,0,2).
+- temporallyBetween(3,0,3).
+- temporallyBetween(3,1,0).
+- temporallyBetween(3,1,1).
+- temporallyBetween(3,1,2).
+- temporallyBetween(3,1,3).
+- temporallyBetween(3,2,0).
+- temporallyBetween(3,2,1).
+- temporallyBetween(3,2,2).
+- temporallyBetween(3,2,3).
+- temporallyBetween(3,3,0).
+- temporallyBetween(3,3,1).
+- temporallyBetween(3,3,2).
+- temporallyBetween(3,3,3).
+
+  temporallyBetweenOrEqual(0,0,0).
+- temporallyBetweenOrEqual(0,0,1).
+- temporallyBetweenOrEqual(0,0,2).
+  temporallyBetweenOrEqual(0,0,3).
+- temporallyBetweenOrEqual(0,1,0).
+- temporallyBetweenOrEqual(0,1,1).
+- temporallyBetweenOrEqual(0,1,2).
+- temporallyBetweenOrEqual(0,1,3).
+- temporallyBetweenOrEqual(0,2,0).
+- temporallyBetweenOrEqual(0,2,1).
+- temporallyBetweenOrEqual(0,2,2).
+- temporallyBetweenOrEqual(0,2,3).
+- temporallyBetweenOrEqual(0,3,0).
+- temporallyBetweenOrEqual(0,3,1).
+- temporallyBetweenOrEqual(0,3,2).
+  temporallyBetweenOrEqual(0,3,3).
+- temporallyBetweenOrEqual(1,0,0).
+- temporallyBetweenOrEqual(1,0,1).
+- temporallyBetweenOrEqual(1,0,2).
+- temporallyBetweenOrEqual(1,0,3).
+- temporallyBetweenOrEqual(1,1,0).
+- temporallyBetweenOrEqual(1,1,1).
+- temporallyBetweenOrEqual(1,1,2).
+- temporallyBetweenOrEqual(1,1,3).
+- temporallyBetweenOrEqual(1,2,0).
+- temporallyBetweenOrEqual(1,2,1).
+- temporallyBetweenOrEqual(1,2,2).
+- temporallyBetweenOrEqual(1,2,3).
+- temporallyBetweenOrEqual(1,3,0).
+- temporallyBetweenOrEqual(1,3,1).
+- temporallyBetweenOrEqual(1,3,2).
+- temporallyBetweenOrEqual(1,3,3).
+- temporallyBetweenOrEqual(2,0,0).
+- temporallyBetweenOrEqual(2,0,1).
+- temporallyBetweenOrEqual(2,0,2).
+- temporallyBetweenOrEqual(2,0,3).
+- temporallyBetweenOrEqual(2,1,0).
+- temporallyBetweenOrEqual(2,1,1).
+- temporallyBetweenOrEqual(2,1,2).
+- temporallyBetweenOrEqual(2,1,3).
+- temporallyBetweenOrEqual(2,2,0).
+- temporallyBetweenOrEqual(2,2,1).
+- temporallyBetweenOrEqual(2,2,2).
+- temporallyBetweenOrEqual(2,2,3).
+- temporallyBetweenOrEqual(2,3,0).
+- temporallyBetweenOrEqual(2,3,1).
+- temporallyBetweenOrEqual(2,3,2).
+- temporallyBetweenOrEqual(2,3,3).
+- temporallyBetweenOrEqual(3,0,0).
+- temporallyBetweenOrEqual(3,0,1).
+- temporallyBetweenOrEqual(3,0,2).
+- temporallyBetweenOrEqual(3,0,3).
+- temporallyBetweenOrEqual(3,1,0).
+- temporallyBetweenOrEqual(3,1,1).
+- temporallyBetweenOrEqual(3,1,2).
+- temporallyBetweenOrEqual(3,1,3).
+- temporallyBetweenOrEqual(3,2,0).
+- temporallyBetweenOrEqual(3,2,1).
+- temporallyBetweenOrEqual(3,2,2).
+- temporallyBetweenOrEqual(3,2,3).
+- temporallyBetweenOrEqual(3,3,0).
+- temporallyBetweenOrEqual(3,3,1).
+- temporallyBetweenOrEqual(3,3,2).
+  temporallyBetweenOrEqual(3,3,3).
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-1.in b/ontologies/sumo/theorems/timepoints_entails/ex129-1.in
new file mode 100644
index 000000000..110f0a560
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-1.in
@@ -0,0 +1,39 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all x all y (beforeOrEqual(x,y)-> (TimePoint(x) & TimePoint(y)))).
+
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-1.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-1.proof
new file mode 100644
index 000000000..dcc864195
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-1.proof
@@ -0,0 +1,35 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8596 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 14:59:03 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.00 (+ 0.00) seconds.
+% Length of proof is 15.
+% Level of proof is 6.
+% Maximum clause weight is 6.
+% Given clauses 17.
+
+1 (all x all y (before(x,y) -> TimePoint(x) & TimePoint(y))) # label(non_clause).  [assumption].
+9 (all x all y (beforeOrEqual(x,y) <-> before(x,y) | TimePoint(x) & x = y)) # label(non_clause).  [assumption].
+12 -(all x all y (beforeOrEqual(x,y) -> TimePoint(x) & TimePoint(y))) # label(non_clause).  [assumption].
+22 -beforeOrEqual(x,y) | before(x,y) | TimePoint(x).  [clausify(9)].
+23 -beforeOrEqual(x,y) | before(x,y) | y = x.  [clausify(9)].
+25 beforeOrEqual(c1,c2).  [clausify(12)].
+26 -before(x,y) | TimePoint(x).  [clausify(1)].
+27 -before(x,y) | TimePoint(y).  [clausify(1)].
+36 -TimePoint(c1) | -TimePoint(c2).  [clausify(12)].
+41 before(c1,c2) | TimePoint(c1).  [resolve(25,a,22,a)].
+42 before(c1,c2) | c2 = c1.  [resolve(25,a,23,a)].
+53 TimePoint(c1).  [resolve(41,a,26,a),merge(b)].
+54 -TimePoint(c2).  [back_unit_del(36),unit_del(a,53)].
+57 c2 = c1.  [resolve(42,a,27,a),unit_del(b,54)].
+58 $F.  [back_rewrite(54),rewrite([57(1)]),unit_del(a,53)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-10.in b/ontologies/sumo/theorems/timepoints_entails/ex129-10.in
new file mode 100644
index 000000000..fd5936c3e
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-10.in
@@ -0,0 +1,38 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all x all y all z (temporallyBetweenOrEqual(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z))).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-10.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-10.proof
new file mode 100644
index 000000000..678332bd8
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-10.proof
@@ -0,0 +1,43 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8738 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 15:05:30 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.00 (+ 0.00) seconds.
+% Length of proof is 23.
+% Level of proof is 8.
+% Maximum clause weight is 6.
+% Given clauses 19.
+
+1 (all x all y (before(x,y) -> TimePoint(x) & TimePoint(y))) # label(non_clause).  [assumption].
+9 (all x all y (beforeOrEqual(x,y) <-> before(x,y) | TimePoint(x) & x = y)) # label(non_clause).  [assumption].
+11 (all x all y (temporallyBetweenOrEqual(x,y,z) <-> beforeOrEqual(x,y) & beforeOrEqual(y,z))) # label(non_clause).  [assumption].
+12 -(all x all y all z (temporallyBetweenOrEqual(x,y,z) -> TimePoint(x) & TimePoint(y) & TimePoint(z))) # label(non_clause).  [assumption].
+19 -temporallyBetweenOrEqual(x,y,z) | beforeOrEqual(x,y).  [clausify(11)].
+20 -temporallyBetweenOrEqual(x,y,z) | beforeOrEqual(y,z).  [clausify(11)].
+21 temporallyBetweenOrEqual(c1,c2,c3).  [clausify(12)].
+23 -beforeOrEqual(x,y) | before(x,y) | TimePoint(x).  [clausify(9)].
+24 -beforeOrEqual(x,y) | before(x,y) | y = x.  [clausify(9)].
+26 beforeOrEqual(c1,c2).  [resolve(21,a,19,a)].
+27 beforeOrEqual(c2,c3).  [resolve(21,a,20,a)].
+28 -before(x,y) | TimePoint(x).  [clausify(1)].
+29 -before(x,y) | TimePoint(y).  [clausify(1)].
+38 -TimePoint(c1) | -TimePoint(c2) | -TimePoint(c3).  [clausify(12)].
+43 before(c1,c2) | TimePoint(c1).  [resolve(26,a,23,a)].
+45 before(c2,c3) | TimePoint(c2).  [resolve(27,a,23,a)].
+46 before(c2,c3) | c3 = c2.  [resolve(27,a,24,a)].
+57 TimePoint(c1).  [resolve(43,a,28,a),merge(b)].
+58 -TimePoint(c2) | -TimePoint(c3).  [back_unit_del(38),unit_del(a,57)].
+64 TimePoint(c2).  [resolve(45,a,28,a),merge(b)].
+65 -TimePoint(c3).  [back_unit_del(58),unit_del(a,64)].
+68 c3 = c2.  [resolve(46,a,29,a),unit_del(b,65)].
+69 $F.  [back_rewrite(65),rewrite([68(1)]),unit_del(a,64)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-2.in b/ontologies/sumo/theorems/timepoints_entails/ex129-2.in
new file mode 100644
index 000000000..90c119391
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-2.in
@@ -0,0 +1,39 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all x (TimePoint(x)-> beforeOrEqual(x,x))).
+
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-2.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-2.proof
new file mode 100644
index 000000000..403ee80da
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-2.proof
@@ -0,0 +1,26 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8615 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 14:59:49 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.00 (+ 0.00) seconds.
+% Length of proof is 6.
+% Level of proof is 2.
+% Maximum clause weight is 8.
+% Given clauses 16.
+
+9 (all x all y (beforeOrEqual(x,y) <-> before(x,y) | TimePoint(x) & x = y)) # label(non_clause).  [assumption].
+12 -(all x (TimePoint(x) -> beforeOrEqual(x,x))) # label(non_clause).  [assumption].
+34 beforeOrEqual(x,y) | -TimePoint(x) | y != x.  [clausify(9)].
+35 TimePoint(c1).  [clausify(12)].
+36 -beforeOrEqual(c1,c1).  [clausify(12)].
+53 $F.  [ur(34,a,36,a,c,xx),unit_del(a,35)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-3.in b/ontologies/sumo/theorems/timepoints_entails/ex129-3.in
new file mode 100644
index 000000000..dcc1d61fe
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-3.in
@@ -0,0 +1,39 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all x all y ((beforeOrEqual(x,y) & beforeOrEqual(y,x)) -> (x=y))).
+
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-3.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-3.proof
new file mode 100644
index 000000000..26bc5f2c7
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-3.proof
@@ -0,0 +1,39 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8642 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 15:01:05 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.00 (+ 0.00) seconds.
+% Length of proof is 19.
+% Level of proof is 6.
+% Maximum clause weight is 9.
+% Given clauses 26.
+
+1 (all x all y (before(x,y) -> TimePoint(x) & TimePoint(y))) # label(non_clause).  [assumption].
+2 (all x (TimePoint(x) -> -before(x,x))) # label(non_clause).  [assumption].
+3 (all x all y all z (before(x,y) & before(y,z) -> before(x,z))) # label(non_clause).  [assumption].
+9 (all x all y (beforeOrEqual(x,y) <-> before(x,y) | TimePoint(x) & x = y)) # label(non_clause).  [assumption].
+12 -(all x all y (beforeOrEqual(x,y) & beforeOrEqual(y,x) -> x = y)) # label(non_clause).  [assumption].
+23 -beforeOrEqual(x,y) | before(x,y) | y = x.  [clausify(9)].
+25 beforeOrEqual(c1,c2).  [clausify(12)].
+26 beforeOrEqual(c2,c1).  [clausify(12)].
+28 -before(x,y) | TimePoint(y).  [clausify(1)].
+29 -TimePoint(x) | -before(x,x).  [clausify(2)].
+30 -before(x,y) | -before(y,z) | before(x,z).  [clausify(3)].
+37 c2 != c1.  [clausify(12)].
+43 before(c1,c2) | c2 = c1.  [resolve(25,a,23,a)].
+44 before(c1,c2).  [copy(43),unit_del(b,37)].
+46 before(c2,c1) | c1 = c2.  [resolve(26,a,23,a)].
+47 before(c2,c1).  [copy(46),flip(b),unit_del(b,37)].
+58 TimePoint(c2).  [resolve(44,a,28,a)].
+70 -before(c2,c2).  [ur(29,a,58,a)].
+82 $F.  [ur(30,b,44,a,c,70,a),unit_del(a,47)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-4.in b/ontologies/sumo/theorems/timepoints_entails/ex129-4.in
new file mode 100644
index 000000000..ad00813b6
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-4.in
@@ -0,0 +1,38 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all x all y all z ((beforeOrEqual(x,y) & beforeOrEqual(y,z))-> beforeOrEqual(x,z))).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-4.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-4.proof
new file mode 100644
index 000000000..575354dc5
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-4.proof
@@ -0,0 +1,43 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8659 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 15:01:41 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.01 (+ 0.00) seconds.
+% Length of proof is 23.
+% Level of proof is 6.
+% Maximum clause weight is 9.
+% Given clauses 89.
+
+1 (all x all y (before(x,y) -> TimePoint(x) & TimePoint(y))) # label(non_clause).  [assumption].
+3 (all x all y all z (before(x,y) & before(y,z) -> before(x,z))) # label(non_clause).  [assumption].
+9 (all x all y (beforeOrEqual(x,y) <-> before(x,y) | TimePoint(x) & x = y)) # label(non_clause).  [assumption].
+12 -(all x all y all z (beforeOrEqual(x,y) & beforeOrEqual(y,z) -> beforeOrEqual(x,z))) # label(non_clause).  [assumption].
+21 -before(x,y) | TimePoint(x).  [clausify(1)].
+24 -before(x,y) | -before(y,z) | before(x,z).  [clausify(3)].
+31 -beforeOrEqual(x,y) | before(x,y) | TimePoint(x).  [clausify(9)].
+32 -beforeOrEqual(x,y) | before(x,y) | y = x.  [clausify(9)].
+33 beforeOrEqual(x,y) | -before(x,y).  [clausify(9)].
+34 beforeOrEqual(x,y) | -TimePoint(x) | y != x.  [clausify(9)].
+35 beforeOrEqual(c1,c2).  [clausify(12)].
+36 beforeOrEqual(c2,c3).  [clausify(12)].
+37 -beforeOrEqual(c1,c3).  [clausify(12)].
+49 before(c1,c2) | c2 = c1.  [resolve(35,a,32,a)].
+50 before(c1,c2) | TimePoint(c1).  [resolve(35,a,31,a)].
+51 before(c2,c3) | c3 = c2.  [resolve(36,a,32,a)].
+53 -before(c1,c3).  [ur(33,a,37,a)].
+61 TimePoint(c1).  [resolve(50,a,21,a),merge(b)].
+70 c3 != c1.  [ur(34,a,37,a,b,61,a)].
+87 c2 = c1 | -before(c2,x) | before(c1,x).  [resolve(49,a,24,a)].
+212 c2 = c1 | c3 = c2.  [resolve(87,b,51,a),unit_del(b,53)].
+213 c2 = c1.  [para(212(b,1),37(a,2)),unit_del(b,35)].
+229 $F.  [back_rewrite(51),rewrite([213(1),213(5)]),unit_del(a,53),unit_del(b,70)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-5.in b/ontologies/sumo/theorems/timepoints_entails/ex129-5.in
new file mode 100644
index 000000000..d51c41001
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-5.in
@@ -0,0 +1,38 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all x all y (beforeOrEqual(x,y)->(before(x,y) | (x=y)))).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-5.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-5.proof
new file mode 100644
index 000000000..6e59dff96
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-5.proof
@@ -0,0 +1,28 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8672 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 15:02:22 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.00 (+ 0.00) seconds.
+% Length of proof is 8.
+% Level of proof is 3.
+% Maximum clause weight is 3.
+% Given clauses 0.
+
+9 (all x all y (beforeOrEqual(x,y) <-> before(x,y) | TimePoint(x) & x = y)) # label(non_clause).  [assumption].
+12 -(all x all y (beforeOrEqual(x,y) -> before(x,y) | x = y)) # label(non_clause).  [assumption].
+23 -beforeOrEqual(x,y) | before(x,y) | y = x.  [clausify(9)].
+25 beforeOrEqual(c1,c2).  [clausify(12)].
+36 -before(c1,c2).  [clausify(12)].
+37 c2 != c1.  [clausify(12)].
+44 before(c1,c2) | c2 = c1.  [resolve(25,a,23,a)].
+45 $F.  [copy(44),unit_del(a,36),unit_del(b,37)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-6.in b/ontologies/sumo/theorems/timepoints_entails/ex129-6.in
new file mode 100644
index 000000000..31949b907
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-6.in
@@ -0,0 +1,38 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all x all y all z (temporallyBetween(x,y,z)-> TimePoint(x) & TimePoint(y) & TimePoint(z))).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-6.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-6.proof
new file mode 100644
index 000000000..1008d6000
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-6.proof
@@ -0,0 +1,35 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8685 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 15:03:00 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.00 (+ 0.00) seconds.
+% Length of proof is 15.
+% Level of proof is 5.
+% Maximum clause weight is 6.
+% Given clauses 17.
+
+1 (all x all y (before(x,y) -> TimePoint(x) & TimePoint(y))) # label(non_clause).  [assumption].
+10 (all x all y (temporallyBetween(x,y,z) <-> before(x,y) & before(y,z))) # label(non_clause).  [assumption].
+12 -(all x all y all z (temporallyBetween(x,y,z) -> TimePoint(x) & TimePoint(y) & TimePoint(z))) # label(non_clause).  [assumption].
+13 -temporallyBetween(x,y,z) | before(x,y).  [clausify(10)].
+16 -temporallyBetween(x,y,z) | before(y,z).  [clausify(10)].
+18 temporallyBetween(c1,c2,c3).  [clausify(12)].
+26 -before(x,y) | TimePoint(x).  [clausify(1)].
+27 -before(x,y) | TimePoint(y).  [clausify(1)].
+36 -TimePoint(c1) | -TimePoint(c2) | -TimePoint(c3).  [clausify(12)].
+41 before(c1,c2).  [resolve(18,a,13,a)].
+42 before(c2,c3).  [resolve(18,a,16,a)].
+53 TimePoint(c2).  [resolve(41,a,27,a)].
+54 TimePoint(c1).  [resolve(41,a,26,a)].
+55 -TimePoint(c3).  [back_unit_del(36),unit_del(a,54),unit_del(b,53)].
+58 $F.  [resolve(42,a,27,a),unit_del(a,55)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-7.in b/ontologies/sumo/theorems/timepoints_entails/ex129-7.in
new file mode 100644
index 000000000..548e05f50
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-7.in
@@ -0,0 +1,38 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all x all y all z (temporallyBetween(x,y,z)-> temporallyBetweenOrEqual(x,y,z))).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-7.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-7.proof
new file mode 100644
index 000000000..c65dbd65f
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-7.proof
@@ -0,0 +1,35 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8698 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 15:03:48 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.00 (+ 0.00) seconds.
+% Length of proof is 15.
+% Level of proof is 4.
+% Maximum clause weight is 10.
+% Given clauses 38.
+
+9 (all x all y (beforeOrEqual(x,y) <-> before(x,y) | TimePoint(x) & x = y)) # label(non_clause).  [assumption].
+10 (all x all y (temporallyBetween(x,y,z) <-> before(x,y) & before(y,z))) # label(non_clause).  [assumption].
+11 (all x all y (temporallyBetweenOrEqual(x,y,z) <-> beforeOrEqual(x,y) & beforeOrEqual(y,z))) # label(non_clause).  [assumption].
+12 -(all x all y all z (temporallyBetween(x,y,z) -> temporallyBetweenOrEqual(x,y,z))) # label(non_clause).  [assumption].
+13 -temporallyBetween(x,y,z) | before(x,y).  [clausify(10)].
+16 -temporallyBetween(x,y,z) | before(y,z).  [clausify(10)].
+18 temporallyBetween(c1,c2,c3).  [clausify(12)].
+31 beforeOrEqual(x,y) | -before(x,y).  [clausify(9)].
+35 temporallyBetweenOrEqual(x,y,z) | -beforeOrEqual(x,y) | -beforeOrEqual(y,z).  [clausify(11)].
+36 -temporallyBetweenOrEqual(c1,c2,c3).  [clausify(12)].
+41 before(c1,c2).  [resolve(18,a,13,a)].
+42 before(c2,c3).  [resolve(18,a,16,a)].
+55 beforeOrEqual(c1,c2).  [resolve(41,a,31,b)].
+60 beforeOrEqual(c2,c3).  [resolve(42,a,31,b)].
+99 $F.  [ur(35,a,36,a,b,55,a),unit_del(a,60)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-8.in b/ontologies/sumo/theorems/timepoints_entails/ex129-8.in
new file mode 100644
index 000000000..4a562fd24
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-8.in
@@ -0,0 +1,38 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all y all z all x (temporallyBetween(x,y,z)<->(before(x,y) & before(y,z)))).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-8.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-8.proof
new file mode 100644
index 000000000..5e7d0e588
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-8.proof
@@ -0,0 +1,33 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8711 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 15:04:18 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.00 (+ 0.00) seconds.
+% Length of proof is 13.
+% Level of proof is 5.
+% Maximum clause weight is 10.
+% Given clauses 24.
+
+10 (all x all y (temporallyBetween(x,y,z) <-> before(x,y) & before(y,z))) # label(non_clause).  [assumption].
+12 -(all x all y all z (temporallyBetween(z,x,y) <-> before(z,x) & before(x,y))) # label(non_clause).  [assumption].
+32 -temporallyBetween(x,y,z) | before(x,y).  [clausify(10)].
+33 -temporallyBetween(x,y,z) | before(y,z).  [clausify(10)].
+34 temporallyBetween(x,y,z) | -before(x,y) | -before(y,z).  [clausify(10)].
+35 temporallyBetween(c3,c1,c2) | before(c3,c1).  [clausify(12)].
+36 temporallyBetween(c3,c1,c2) | before(c1,c2).  [clausify(12)].
+37 -temporallyBetween(c3,c1,c2) | -before(c3,c1) | -before(c1,c2).  [clausify(12)].
+48 before(c3,c1).  [resolve(35,a,32,a),merge(b)].
+49 -temporallyBetween(c3,c1,c2) | -before(c1,c2).  [back_unit_del(37),unit_del(b,48)].
+50 before(c1,c2).  [resolve(36,a,33,a),merge(b)].
+51 -temporallyBetween(c3,c1,c2).  [back_unit_del(49),unit_del(b,50)].
+65 $F.  [ur(34,a,51,a,b,48,a),unit_del(a,50)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-9.in b/ontologies/sumo/theorems/timepoints_entails/ex129-9.in
new file mode 100644
index 000000000..531100b6e
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-9.in
@@ -0,0 +1,38 @@
+formulas(assumptions).
+
+all x all y (before(x,y)-> TimePoint(x) & TimePoint(y)).%6
+all x (TimePoint(x)->(-(before(x,x)))).%7
+all x all y all z ((before(x,y) & before(y,z))-> before(x,z)).%8
+all x all y
+	((TimePoint(x)
+	& TimePoint(y))
+	->
+	(before(x,y) | before(y,x) | (x=y))).
+TimePoint(PositiveInfinity).%16
+TimePoint(NegativeInfinity).%17
+before(NegativeInfinity,PositiveInfinity).
+all x (TimePoint(x) & (-(x=PositiveInfinity))->before(x,PositiveInfinity)).%18
+all x (TimePoint(x) & (-(x=NegativeInfinity))->before(NegativeInfinity,x)).%19
+all x (TimePoint(x) & (-(x=PositiveInfinity))->(exists y temporallyBetween(x,y,PositiveInfinity))).%20
+all x (TimePoint(x) & (-(x=NegativeInfinity))->(exists y temporallyBetween(NegativeInfinity,y,x))).%21
+
+(all x all y
+	(beforeOrEqual(x,y)
+	<->
+	(before(x,y) | (TimePoint(x) & (x=y))))).
+
+(all x all y
+	(temporallyBetween(x,y,z)
+	<->
+	(before(x,y)
+	& before(y,z)))).
+
+(all x all y
+	(temporallyBetweenOrEqual(x,y,z)
+	<->
+	(beforeOrEqual(x,y)
+	& beforeOrEqual(y,z)))).
+
+-(all y all z all x (temporallyBetweenOrEqual(x,y,z)<->(beforeOrEqual(x,y) & beforeOrEqual(y,z)))).
+
+end_of_list.
diff --git a/ontologies/sumo/theorems/timepoints_entails/ex129-9.proof b/ontologies/sumo/theorems/timepoints_entails/ex129-9.proof
new file mode 100644
index 000000000..d266e5eea
--- /dev/null
+++ b/ontologies/sumo/theorems/timepoints_entails/ex129-9.proof
@@ -0,0 +1,33 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 8724 was started by mudcat on mie-17-83.internal.mie.utoronto.ca,
+Mon Mar  7 15:04:56 2016
+The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.00 (+ 0.00) seconds.
+% Length of proof is 13.
+% Level of proof is 5.
+% Maximum clause weight is 10.
+% Given clauses 30.
+
+11 (all x all y (temporallyBetweenOrEqual(x,y,z) <-> beforeOrEqual(x,y) & beforeOrEqual(y,z))) # label(non_clause).  [assumption].
+12 -(all x all y all z (temporallyBetweenOrEqual(z,x,y) <-> beforeOrEqual(z,x) & beforeOrEqual(x,y))) # label(non_clause).  [assumption].
+32 -temporallyBetweenOrEqual(x,y,z) | beforeOrEqual(x,y).  [clausify(11)].
+33 -temporallyBetweenOrEqual(x,y,z) | beforeOrEqual(y,z).  [clausify(11)].
+34 temporallyBetweenOrEqual(x,y,z) | -beforeOrEqual(x,y) | -beforeOrEqual(y,z).  [clausify(11)].
+35 temporallyBetweenOrEqual(c3,c1,c2) | beforeOrEqual(c3,c1).  [clausify(12)].
+36 temporallyBetweenOrEqual(c3,c1,c2) | beforeOrEqual(c1,c2).  [clausify(12)].
+37 -temporallyBetweenOrEqual(c3,c1,c2) | -beforeOrEqual(c3,c1) | -beforeOrEqual(c1,c2).  [clausify(12)].
+51 beforeOrEqual(c3,c1).  [resolve(35,a,32,a),merge(b)].
+52 -temporallyBetweenOrEqual(c3,c1,c2) | -beforeOrEqual(c1,c2).  [back_unit_del(37),unit_del(b,51)].
+53 beforeOrEqual(c1,c2).  [resolve(36,a,33,a),merge(b)].
+54 -temporallyBetweenOrEqual(c3,c1,c2).  [back_unit_del(52),unit_del(b,53)].
+66 $F.  [ur(34,a,54,a,b,51,a),unit_del(a,53)].
+
+============================== end of proof ==========================
diff --git a/ontologies/sumo_timeintervals/mappings/delta.in b/ontologies/sumo_timeintervals/mappings/delta.in
new file mode 100644
index 000000000..cf173e211
--- /dev/null
+++ b/ontologies/sumo_timeintervals/mappings/delta.in
@@ -0,0 +1,33 @@
+
+(all x all y
+	(begin(x,y)
+	<->
+	(in(y,x)
+	& line(x)
+	& point(y)
+	& (all z
+		((point(z)
+		& in(z,x))
+		->
+		leq(y,z)))))).
+
+(all x all y
+	(end(x,y)
+	<->
+	(in(y,x)
+	& line(x)
+	& point(y)
+	& (all z
+		((point(z)
+		& in(z,x))
+		->
+		leq(z,y)))))).
+
+(all x all y all z
+	(interval(x,y,z)
+	<->
+	(point(x)
+	& point(y)
+	& line(z)
+	& beginLn(z,x)
+	& endLn(z,y)))).
diff --git a/ontologies/sumo_timeintervals/mappings/pi.in b/ontologies/sumo_timeintervals/mappings/pi.in
new file mode 100644
index 000000000..b9f867b64
--- /dev/null
+++ b/ontologies/sumo_timeintervals/mappings/pi.in
@@ -0,0 +1,10 @@
+
+(all x all y
+	(lt(x,y) <-> before(x,y))).
+
+(all x all y
+	(in(x,y)
+	<->
+	((Timeposition(x) & (x=y))
+	| ((begin(y,x) | end(y,x)) & Timepoint(x) & TimeInterval(y))
+	| ((begin(x,y) | end(x,y)) & Timepoint(y) & TimeInterval(x))))).
diff --git a/ontologies/sumo_timeintervals/sumo_timeintervals.clif b/ontologies/sumo_timeintervals/sumo_timeintervals.clif
new file mode 100644
index 000000000..44aead076
--- /dev/null
+++ b/ontologies/sumo_timeintervals/sumo_timeintervals.clif
@@ -0,0 +1,56 @@
+
+(cl-text colore.oor.net/sumo_timeintervals/sumo_timeintervals.clif
+
+(cl-imports colore.oor.net/sumo_timepoints/sumo_ordered_timepoints.clif)
+
+(forall (x)
+	(TimeInterval x)
+	(temporalPart x x))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(Timeposition x)))
+
+(forall (x)
+	(if	(TimePoint x)
+		(Timeposition x)))
+
+(forall (x)
+	(if	(TimePosition x)
+		(or	(TimeInterval x)
+			(TimePoint x))))
+
+(forall (x)
+	(if	(TimeInterval x)
+		(not (TimePoint x))))
+
+(forall (x y z)
+	(if	(and	(TimePoint x)
+			(TimePoint y)
+			(TimeInterval z)
+			(= (TimeIntervalFn x y) z))
+		(and	(= (BeginFn z) x)
+			(= (EndFn z) y))))
+
+(forall (x y z t)
+	(if	(and	(TimeInterval x)
+			(TimeInterval y)
+			(TimePoint z)
+			(TimePoint t)
+			(= (BeginFn x) z)
+			(= (BeginFn y) z)
+			(= (EndFn x) t)
+			(= (EndFn y) t))
+		(= x y)))
+
+(forall (z u v)
+	(if	(and	(TimeInterval z)
+			(TimePoint u)
+			(TimePoint v)
+			(= (BeginFn z) u)
+			(= (EndFn z) v))
+		(before u v)))
+
+
+
+)
diff --git a/ontologies/sumo_timepoints/sumo_ordered_timepoints.clif b/ontologies/sumo_timepoints/sumo_ordered_timepoints.clif
new file mode 100644
index 000000000..d9b562e3b
--- /dev/null
+++ b/ontologies/sumo_timepoints/sumo_ordered_timepoints.clif
@@ -0,0 +1,55 @@
+
+(cl-text colore.oor.net/sumo/sumo_timepoints/sumo_ordered_timepoints.clif
+
+(cl-imports colore.oor.net/sumo/sumo_timepoints/sumo_timepoints_def.clif)
+
+(forall (x y)
+	(if	(before x y)
+		(and	(TimePoint x)
+			(TimePoint y))))
+
+(forall (x)
+	(if	(TimePoint x)
+		(not (before x x))))
+
+(forall (x y z)
+	(if	(and	(before x y)
+			(before y z))
+		(before x z)))
+
+(TimePoint PositiveInfinity)
+
+(TimePoint NegativeInfinity)
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x PositiveInfinity)))
+		(before x PositiveInfinity)))
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x NegativeInfinity)))
+		(before NegativeInfinity x)))
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x PositiveInfinity)))
+		(exists (y)
+			(temporallyBetween x y PositiveInfinity))))
+
+(forall (x)
+	(if	(and	(TimePoint x)
+			(not (= x NegativeInfinity)))
+		(exists (y)
+			(temporallyBetween NegativeInfinity y x))))
+
+(before NegativeInfinity PositiveInfinity)
+
+(forall (t1 t2)
+	(if	(and	(TimePoint t1)
+			(TimePoint t2))
+		(or	(before t1 t2)
+			(before t2 t1)
+			(= t1 t2))))
+
+)