|    This example is from "Relations in biomedical ontologies" by Barry Smith et al,
|    Genome Biology 2005.  http://genomebiology.com/2005/6/5/R46
|
|    3. C part_of C1 = [definition] for all c, t, if Cct then
|                                   there is some c1 such that C1c1t and c part_of c1 at t.
  

for all c, t, if eg-C c t then there is some c1 such that eg-C1 c1 t and c part_of c1 at t
------------------------------------------------------------------------------------------
3. that-C is a part_of the Continuant class that-C1


(A c,t) [ eg-C c t => (E c1) [ eg-C1 c1 t and c part_of c1 at t ] ]
------------------------------------------------------------------------------------------
for all c, t, if eg-C c t then there is some c1 such that eg-C1 c1 t and c part_of c1 at t


some-C and some-C1 are two different Non-process classes with instances
not : (E c,t) [ that-C c t and not (E c1) [ that-C1 c1 t and c part_of c1 at t ] ]
-----------------------------------------------------------------------------------
(A c,t) [ that-C c t => (E c1) [ that-C1 c1 t and c part_of c1 at t ] ]


some-C and some-C1 are two different Non-process classes with instances
some-c is an instance_of that-C at some-t
not : (E c1) [ that-C1 c1 that-t and that-c part_of c1 at that-t ]
----------------------------------------------------------------------------
(E c,t) [ that-C c t and not (E c1) [ that-C1 c1 t and c part_of c1 at t ] ]


some-c1 is an instance_of some-C1 at some-t
some-c is a part_of that-c1 at that-t
------------------------------------------------------------
(E c1) [ that-C1 c1 that-t and that-c part_of c1 at that-t ]



this-item is an instance_of this-Class at this-t
========================================================
  c1                           C1          1
  c                            C           1
  c1                           C1          2
  c                            C           2


this-item1 is a part_of this-item2 at this-t
=============================================
  c                     c1                 1
  c                     c1                 2


the class this-class is of type this-type
==========================================
             C                 Non-process
             C1                Non-process




the class some-C is of type Non-process and has at least one instance
the class some-C1 is of type Non-process and has at least one instance
that-C and that-C1 are different
-----------------------------------------------------------------------
that-C and that-C1 are two different Non-process classes with instances


the class some-C is of type Non-process
some-c is an instance_of that-C at some-t
--------------------------------------------------------------------
the class that-C is of type Non-process and has at least one instance

some-t1 is less than some-t2
-------------------------------------
that-t1 is earlier than that-t2

some-C1 is not equal some-C2
-------------------------------
that-C1 and that-C2 are different