(cl:comment 'moduleName: Date-Time Vocabulary')
(cl:comment 'moduleAbbreviation: DTV')
(cl:comment 'moduleVersion: 1.0')
(cl:comment 'moduleAbstract: This file contains CLIF for portions of the Date-Time Vocabulary.  See http://www.omg.org/spec/DTV.')
(cl:comment 'filename: dtv.clif')
(cl:comment 'documentNumber: dtc/2012-12-09')
(cl:comment 'documentURL: http:/www.omg.org/spec/DTV/20121201/dtv.clif')
(cl:comment 'isNormative: true')
(cl:comment 'contentType: vocabulary')
(cl:comment 'contentLanguage: http://standards.iso.org/ittf/PubliclyAvailableStandards/c039175_ISO_IEC_24707_2007%28E%29.zip')
(cl:comment 'format: CLIF')
(cl:comment 'directSource: http:/www.omg.org/cgi-bin/doc?dtc/2012-12-06')
(cl:comment 'copyright: Copyright (c) 2012, Object Management Group')

(cl:comment 'Time interval2 is a component of time interval1. Every instant in time interval1 is also in time interval2. Everything that happens in time interval1 happens in time interval2')
(forall (t1 t2)
  (if ("time interval1 is part of time interval2" t1 t2)
    (and ("time interval" t1) ("time interval" t2)
       ("thing1 is part of thing2" t1 t2))))

				
(cl:comment 'time interval1 overlaps time interval2 ')
(forall (t1 t2)
  (if ("time interval1 overlaps time interval2" t1 t2)
    (and ("time interval" t1) ("time interval" t2)
       ("thing1 overlaps thing2" t1 t2))))

				
(cl:comment 'time interval1 is a proper part of time interval2 ')
(forall (t1 t2)
  (if ("time interval1 is proper part of time interval2" t1 t2)
    (and ("time interval" t1) ("time interval" t2)
       ("thing1 is proper part of thing2" t1 t2))))

				
(cl:comment 'For each time interval1, there is at least one time interval2 that is a proper part of time interval1.')
(forall (ti1 "time interval")
  (exists (ti2 "time interval")
    ("proper part of" ti2 ti1) ))

				
(cl:comment 'time interval1 ends before/when time interval2 starts ')
(forall (t1 t2)
  (if ("time interval1 is before time interval2" t1 t2)
    (and ("time interval" t1) ("time interval" t2))))

				
(cl:comment 'If a time interval1 overlaps a time interval2, then the time interval1 is not before the time interval2.')
(forall (t1 t2)
  (if ("time interval1 overlaps time interval2" t1 t2)
    (and
       (not ("time interval1 is before time interval2" t1 t2))
       (not ("time interval1 is before time interval2" t2 t1)) )))

				
(cl:comment 'If a time interval1 does not overlap a time interval2, then the time interval1 is before the time interval2 or the time interval2 is before the time interval1.')
(forall ((t1 "time interval") (t2 "time interval"))
  (if (not ("time interval1 overlaps time interval2" t1 t2))
      (or ("time interval1 is before time interval2"
           t1 t2)
          ("time interval1 is before time interval2"
           t2 t1))))

				
(cl:comment 'A given time interval is not before the time interval.')
(forall ((t1 "time interval"))
  (not (
"time interval1 is before time interval2"
 t1 t1)))

				
(cl:comment 'If a time interval1 is before a time interval2, then the time interval2 is not before the time interval1.')
(forall (t1 t2)
  (if ("time interval1 is before time interval2" t1 t2)
       (not ("time interval1 is before time interval2" t2 t1))))

				
(cl:comment 'Each time interval1 overlaps each time interval2 and time interval1 is not before time interval2 and time interval2 is not before time interval1, or time interval1 is before time interval2 and time interval1 does not overlap time interval2 and time interval2 is not before time interval1, or time interval2 is before time interval1 and time interval1 does not overlap time interval2 and time interval1 is not before time interval2.')
(forall ((t1 "time interval") (t2 "time interval"))
  (or
     ("time interval1 overlaps time interval2" t1 t2)
    (and
       ("time interval1 is before time interval2" t1 t2)
       (not ("time interval1 overlaps time interval2" t1 t2)))
    (and
       ("time interval1 is before time interval2" t2 t1)
       (not ("time interval1 overlaps time interval2" t1 t2)))
 ))

				
(cl:comment 'If a time interval1 is before a time interval2 and the time interval2 is before a time interval3 then the time interval1 is before the time interval3.')
(forall (t1 t2 t3)
  (if
    (and
      ("time interval1 is before time interval2" t1 t2)
      ("time interval1 is before time interval2" t2 t3))
    ("time interval1 is before time interval2" t1 t3)))

				
(cl:comment 'the time interval1 is before the time interval2 and the time interval1 is before a time interval3 and the time interval3 is before the time interval2')
(forall (t1 t2)
  (iff ("time interval1 is properly before time interval2" t1 t2)
    (and 
       ("time interval" t1)  ("time interval" t2)
       ("time interval1 is before time interval2" t1 t2)
       (exists (t3)
          (and ("time interval1 is before time interval2" t1 t3)
                  ("time interval1 is before time interval2" t3 t2))
) )))

				
(cl:comment 'the time interval1 is part of the time interval2 and the time interval2 is part of the time interval1')
(forall (t1 t2)
  (iff ("time interval1 equals time interval2" t1 t2)
    (and ("time interval1 is part of time interval2" t1 t2)
            ("time interval1 is part of time interval2" t2 t1)) ))

				
(cl:comment 'the time interval1 is before the time interval2 and the time interval1 is not before a time interval3 that is before the time interval2')
(forall (t1 t2)
  (iff ("time interval1 meets time interval2" t1 t2)
    (and 
      ("time interval1 is before time interval2" t1 t2)
      (not  (exists (t3)
        (and ("time interval1 is before time interval2" t1 t3)
                ("time interval1 is before time interval2" t3 t2)) 
)) )))

				
(cl:comment 'the time interval1 overlaps the time interval2 and a time interval3 is a proper part of the time interval1 and the time interval3 is before the time interval2')
(forall (t1 t2)
 (iff ("time interval1 properly overlaps time interval2" t1 t2)
  (and 
    ("time interval1 overlaps time interval2" t1 t2)
    (exists (t3)
      (and ("time interval1 is proper part of time interval2" t3 t1)
              ("time interval1 is before time interval2" t3 t2)) 
) )))

				
(cl:comment 'the time interval1 is a proper part of the time interval2 and a time interval3 is a proper part of the time interval2 and a time interval4 is a proper part of the time interval2 and the time interval3 is before the time interval1 and the time interval1 is before the time interval4')
(forall (t1 t2)
 (iff ("time interval1 is properly during time interval2" t1 t2)
  (and 
    ("time interval1 is proper part of time interval2" t1 t2)
    (not ("time interval1 starts time interval2" t1 t2))
    (not ("time interval1 finishes time interval2" t1 t2))
)))

				
(cl:comment 'time interval1 is a proper part of time interval2 and there exists no time interval3 that is a proper part of time interval2 and that is before time interval1')
(forall (t1 t2)
 (iff ("time interval1 starts time interval2" t1 t2)
  (and 
    ("time interval1 is proper part of time interval2" t1 t2)
    (not (exists (t3)
        (and ("time interval1 is proper part of time interval2" t3 t2)
                ("time interval1 is before time interval2" t3 t1)) )) 
)))

				
(cl:comment 'time interval1 is a proper part of time interval2 and there exists no time interval3 that is a proper part of time interval2 and that is after time interval1')
(forall (t1 t2)
 (iff ("time interval1 finishes time interval2" t1 t2)
  (and 
    ("time interval1 is proper part of time interval2" t1 t2)
    (not (exists (t3)
        (and ("time interval1 is proper part of time interval2" t3 t2)
                ("time interval1 is before time interval2" t1 t3)) )) 
)))

				
(cl:comment 'the time interval1 is properly before the time interval2 or the time interval1 meets the time interval2')
(forall (t1 t2)
 (iff ("time interval1 precedes time interval2" t1 t2)
  (or 
     ("time interval1 is properly before time interval2" t1 t2)
     ("time interval1 meets time interval2" t1 t2)) ))

				
(cl:comment 'the time interval1 equals the time interval2 or the time interval1 meets the time interval2 or the time interval1 properly overlaps the time interval2 or the time interval1 starts the time interval2')
(forall (t1 t2)
 (iff ("time interval1 begins time interval2" t1 t2)
  (or ("time interval1 equals time interval2" t1 t2)
        ("time interval1 meets time interval2" t1 t2)
        ("time interval1 properly overlaps time interval2" t1 t2)
        ("time interval1 starts time interval2" t1 t2)) ))

				
(cl:comment 'the time interval1 equals the time interval2 or the time interval2 meets the time interval1 or the time interval2 properly overlaps the time interval1 or the time interval1 finishes the time interval2')
(forall (t1 t2)
 (iff ("time interval1 ends time interval2" t1 t2)
  (or ("time interval1 equals time interval2" t1 t2)
        ("time interval1 meets time interval2" t2 t1)
        ("time interval1 properly overlaps time interval2" t2 t1)
        ("time interval1 finishes time interval2" t1 t2)) ))

				
(cl:comment 'time interval1 is before time interval2 or time interval1 meets time interval2 or time interval1 properly overlaps time interval2 or time interval2 is properly during time interval1')
(forall (t1 t2)
 (iff ("time interval1 starts before time interval2" t1 t2)
  (or 
     ("time interval1 is before time interval2" t1 t2)
     ("time interval1 meets time interval2" t1 t2)
     ("time interval1 properly overlaps time interval2" t1 t2)
     ("time interval1 is properly during time interval2" t2 t1)) ))

				
(cl:comment 'time interval2 is before time interval1 or time interval2 meets time interval1 or time interval2 properly overlaps time interval1 or time interval2 is properly during time interval1')
(forall (t1 t2)
 (iff ("time interval1 finishes after time interval2" t1 t2)
  (or 
     ("time interval1 is before time interval2" t2 t1)
     ("time interval1 meets time interval2" t2 t1)
     ("time interval1 properly overlaps time interval2" t2 t1)
     ("time interval1 is properly during time interval2" t2 t1)) ))

				
(cl:comment 'time interval1 is before time interval2 or time interval1 properly overlaps time interval2 or time interval1 starts time interval2 ')
(forall ((ti1 ti2))
 (iff ("time interval1 begins before time
        interval2" ti1 ti2)
      (and
        ("time interval" ti1)
        ("time interval" ti2)
        (or
         ("time interval1 is before time
           interval2" ti1 ti2)
         ("time interval1 properly overlaps
           time interval2" ti1 ti2)
         ("time interval1 starts time
           interval2" ti1 ti2)))))

				
(cl:comment 'Each time interval begins before the time interval.')
(forall (ti)
  (if ("time interval" ti)
      ("time interval1 begins before time
        interval2" ti ti)))

				
(cl:comment 'time interval1 is after time interval2 or time interval1 is properly overlapped by time interval2 or time interval1 ends time interval2')
(forall ((ti1 ti2))
 (iff ("time interval1 ends after time
        interval2" ti1 ti2)
      (and
        ("time interval" ti1)
        ("time interval" ti2)
        (or
         ("time interval1 is after time
           interval2" ti1 ti2)
         ("time interval1 properly overlaps
           time interval2" ti2 ti1)
         ("time interval1 ends time
           interval2" ti1 ti2)))))

				
(cl:comment 'Each time interval ends after the time interval.')
(forall (ti)
  (if ("time interval" ti)
      ("time interval1 ends after time
        interval2" ti ti)))

				
(cl:comment 'time interval1 follows time interval2 and  time interval1 precedes time interval3 ')
(forall (t1 t2 t3)
(iff ("time interval1 is between time 
    interval2 and time interval3" t1 t2 t3)
  (and
    ("time interval" t1)
    ("time interval" t2)
    ("time interval" t3)
    ("time interval1 precedes time 
      interval2" t2 t1)
    ("time interval1 precedes time 
      interval2" t1 t3))))

				
(cl:comment 'if the time interval1 includes the time interval2, then the time interval3 equals the time interval1')
(forall (t1 t2 t3)
    (if 
       (or
          ("time interval1 is before time interval2"  t1 t2)
           ("time interval1 properly overlaps  time interval2" t1 t2))
       (iff 
           ("time interval1 plus time interval2 is time interval3" 
                  t1 t2 t3)
           (and
             ("time interval1 starts time interval2"  t1 t3)
             ("time interval1 finishes time interval2"  t2 t3)) 
)))

				
(cl:comment 'if the time interval1 includes the time interval2, then the time interval3 equals the time interval1')
(forall (t1 t2 t3)
    (if 
       (or
          ("time interval1 is before time interval2"  t2 t1)
           ("time interval1 properly overlaps  time interval2" t2 t1))
       (iff 
           ("time interval1 plus time interval2 is time interval3" 
                  t1 t2 t3)
           (and
             ("time interval1 starts time interval2"  t2 t3)
             ("time interval1 finishes time interval2"  t1 t3)) 
)))

				
(cl:comment 'if the time interval1 includes the time interval2, then the time interval3 equals the time interval1')
(forall (t1 t2 t3)
    (if 
        ("time interval1 is part of time interval2"  t1 t2)
        (iff 
           ("time interval1 plus time interval2 is time interval3" 
                  t1 t2 t3)
           (= t3 t2) 
)))

				
(cl:comment 'if the time interval1 includes the time interval2, then the time interval3 equals the time interval1')
(forall (t1 t2 t3)
    (if 
        ("time interval1 is part of time interval2"   t2 t1)
        (iff 
           ("time interval1 plus time interval2 is time interval3" 
                  t1 t2 t3)
           (= t3 t1) 
)))

				
(cl:comment 'For each time interval1 and each time interval2, there is a time interval3 that is time interval1 plus time interval2.')
(forall ((t1 "time interval") (t2 "time interval"))
  (exists ((t3 "time interval"))
     ("time interval1 plus time interval2 is time interval3" t1 t2 t3) ))

				
(cl:comment 'Each time interval1 and each time interval2 is part of the time interval3 that is time interval1 plus time interval2.')
(forall (t1 t2 t3)
  (if ("time interval1 plus time interval2 is time interval3" 
            t1 t2 t3)
       ("time interval1 is part of time interval2" t1 t3)))

				
(cl:comment 'Each time interval1 and each time interval2 is part of the time interval3 that is time interval1 plus time interval2.')
(forall (t1 t2 t3)
  (if ("time interval1 plus time interval2 is time interval3" 
            t1 t2 t3)
       ("time interval1 is part of time interval2" t2 t3)))

				
(cl:comment 'If a time interval1 is part of a time interval3 and a time interval2 is part of the time interval3 then the time interval1 plus the time interval2 is part of the time interval3.')
(forall (t1 t2 t3 t4)
  (if 
    (and
      ("time interval1 is part of time interval2" t1 t3)
      ("time interval1 is part of time interval2" t2 t3))
    (and
      ("time interval1 plus time interval2 is time interval3" t1 t2 t4)
    ("time interval1 is part of time interval2" t4 t3))
   ))

				
(cl:comment 'A time interval1 plus a time interval2 is exactly one time interval3.')
(forall (t1 t2 t3)
  (if ("time interval1 plus time interval2 is time interval3" 
            t1 t2 t3)
      (forall (t4)
        (if 
          ("time interval1 plus time interval2 is time interval3" 
                 t1 t2 t4)
          (= t4 t3) )) ))

				
(cl:comment 'time interval1 meets time interval2 and time interval3 is time interval1')
(forall (t1 t2 t3)
  (iff 
    ("time interval1 to time interval2 specifies time interval3" 
         t1 t2 t3)
    (and
      ("time interval1 is before time interval2" t1 t2)
      (if  ("time interval1 meets time interval2" t1 t2)
            (= t1 t3))
      (if 
        ("time interval1 is properly before time interval2" t1 t2)
        (exists (t4)
          (and
             ("time interval1 meets time interval2" t1 t4)
             ("time interval1 meets time interval2" t4 t2)
             ("time interval1 plus time interval2 is time interval3"
                        t1 t4 t3)))) 
)))

				
(cl:comment 'if the time interval1 starts the time interval2 then the time interval3 finishes the time interval2 and the time interval1 meets the time interval3')
(forall (t1 t2 t3)
  (iff ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
        (and
           ("time interval1 starts time interval2" t1 t2)
           ("time interval1 finishes time interval2" t3 t2)
           ("time interval1 meets time interval2" t1 t3)) ))

				
(cl:comment 'if the time interval1 starts the time interval2 then the time interval3 finishes the time interval2 and the time interval1 meets the time interval3')
(forall (t1 t2)
  (if ("time interval1 starts time interval2" t1 t2)
       (exists (t3)
         ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) )))

				
(cl:comment 'If a time interval1 starts a time interval2 complementing a time interval3, then each time interval4 that is part of the time interval2 and that does not overlap the time interval1 is part of the time interval3.')
(forall (t1 t2 t3)
  (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
      (forall (t4)
        (if 
          (and
             ("time interval1 is part of time interval2" t4 t2)
             (not ("time interval1 overlaps time interval2" t4 t1)))
          ("time interval1 is part of time interval2" t4 t3)))))

				
(cl:comment 'If a time interval1 starts a time interval2 then the time interval1 starts the time interval2 complementing exactly one time interval3.')
(forall (t1 t2 t3)
  (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
      (forall (t4)
        (if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t4)
             (= t4 t3))) ))

				
(cl:comment 'if the time interval1 finishes the time interval2 then the time interval3 starts the time interval2 and the time interval1 is met by the time interval3')
(forall (t1 t2 t3)
  (iff ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
        (and
           ("time interval1 finishes time interval2" t1 t2)
           ("time interval1 starts time interval2" t3 t2)
           ("time interval1 meets time interval2" t3 t1)) ))

				
(cl:comment 'if the time interval1 finishes the time interval2 then the time interval3 starts the time interval2 and the time interval1 is met by the time interval3')
(forall (t1 t2)
  (if ("time interval1 finishes time interval2" t1 t2)
       (exists (t3)
         ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) )))

				
(cl:comment 'If a time interval1 finishes a time interval2 complementing a time interval3, then each time interval4 that is part of the time interval2 and that does not overlap the time interval1 is part of the time interval3.')
(forall (t1 t2 t3)
  (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
      (forall (t4)
        (if 
          (and
             ("time interval1 is part of time interval2" t4 t2)
             (not ("time interval1 overlaps time interval2" t4 t1)))
          ("time interval1 is part of time interval2" t4 t3)))))

				
(cl:comment 'If a time interval1 finishes a time interval2 then the time interval1 finishes the time interval2 complementing exactly one time interval3.')
(forall (t1 t2 t3)
  (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
      (forall (t4)
        (if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t4)
             (= t4 t3))) ))

				
(cl:comment 'For each time interval1 and each time interval2 that is properly during time interval1, there is a time interval4 that finishes time interval1 and is met by time interval2.')
(forall ((ti1 "time interval") 
         (ti2 "time interval"))
  (if ("time interval1 is properly during  
        time interval2" t2 t1)
   (exists (ti3 "time interval")
    (and
     ("time interval1 starts time 
       interval2" ti3 ti1)
     ("time interval1 meets time interval2" 
       ti3 ti2) )) ))

				
(cl:comment 'For each time interval1 and each time interval2 that is properly during time interval1, there is a time interval4 that finishes time interval1 and is met by time interval2.')
(forall ((ti1 "time interval") 
         (ti2 "time interval"))
  (if ("time interval1 is properly during 
        time interval2" t2 t1)
   (exists (ti4 "time interval")
    (and
     ("time interval1 finishes time 
       interval2" ti4 ti1)
     ("time interval1 meets time interval2" 
            ti2 ti4) )) ))

				
(cl:comment 'if the time interval1 overlaps the time interval2, then the time interval3 finishes the time interval1 and starts the time interval2')
(forall (t1 t2 t3)
  (iff 
    ("time interval1 intersects time interval2 with time interval3" 
             t1 t2 t3)
    (and
         ("time interval1 overlaps time interval2" t2 t3)
         ("time interval1 finishes time interval2" t1 t2)
         ("time interval1 starts time interval2" t1 t3)) ))

				
(cl:comment 'if the time interval1 overlaps the time interval2, then the time interval3 finishes the time interval1 and starts the time interval2')
(forall (t1 t2)
  (if 
    ("time interval1 overlaps time interval2" t1 t2)
      (exists (t3)
        ("time interval1 intersects time interval2 with time interval3"
               t3 t1 t2) )))

				
(cl:comment 'If a time interval1 intersects a time interval2 with a time interval3 and a time interval4 is part of the time interval1 and the time interval4 is part of the time interval2, then the time interval4 is part of the time interval3.')
(forall (t1 t2 t3 t4)
  (if 
    (and
       ("time interval1 intersects time interval2 with time interval3"
             t1 t2 t3)
       ("time interval1 is part of time interval2" t4 t2)
       ("time interval1 is part of time interval2" t4 t1))
    ("time interval1 is part of time interval2" t4 t3) ))

				
(cl:comment 'If a time interval1 overlaps a time inteval2, then the time interval1 intersects a time interval2 with exactly one time interval3.')
(forall (t1 t2 t3)
  (if
    ("time interval1 intersects time interval2 with time interval3"
                     t3 t1 t2)
    (forall (t4)
      (if 
        ("time interval1 intersects time interval2 with time interval3"
                     t4 t1 t2)
        (= t4 t3))) ))

				
(cl:comment 'If a time interval1 is properly before a time interval2 then the time interval1 meets a time interval3 and the time interval3 meets the time interval2 and the time interval1 plus the time interval2 is a time interval4 and the time interval1 starts the time interval4 complementing a time interval5 and the time interval2 finishes the time interval4 complementing a time interval6 and the time interval5 intersects the time interval6 with the time interval3.')
(forall (t1 t2)
  (if ("time interval1 is properly before time interval2" t1 t2)
      (exists (t3 t4 t5 t6)
        (and
          ("time interval1 meets time interval2" t1 t3)
          ("time interval1 meets time interval2" t3 t2)
          ("time interval1 plus time interval2 is time interval3"
                   t1 t2 t4)
          ("time interval1 finishes time interval2 complementing time interval3" t5 t4 t1)
          ("time interval1 starts time interval2 complementing time interval3" t6 t4 t2)
          ("time interval1 intersects time interval2 with time interval3" t3 t6 t5))) ))

				
(cl:comment 'Each duration <= the duration.')
(forall ((d1 duration))
  (<= d1 d1))

				
(cl:comment 'Each duration1 <= each duration2 or duration2 <= duration1.')
(forall ((d1 duration) (d2 duration))
  (or
    (<= d1 d2)
    (<= d2 d1)))

				
(cl:comment 'If some duration1 <= some duration2 and the duration2 <= the duration1, then the duration1 equals the duration2.')
(forall ((d1 duration) (d2 duration))
 (if (and
       (<= d1 d2)
       (<= d2 d1))
       (= d1 d2)))

				
(cl:comment 'If some duration1 <= some duration2 and the duration2 <= the duration3 then the duration1 <= the duration3.')
(forall ((d1 duration) (d2 duration) (d3 duration))
  (if (and
        (<= d1 d2)
        (<= d2 d3))
      (<= d1 d3)))

				
(cl:comment 'duration1 <= duration2 and duration1 does not equal duration2 ')
(forall ((d1 duration) (d2 duration))
  (iff (< d1 d2)
       (and
        (<= d1 d2)
        (not (= d2 d1)))))

				
(cl:comment 'duration3 equals duration1 plus duration2')
(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (+ d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 + duration2"
         d3 d1 d2) )))

				
(cl:comment 'For each duration1 and each duration2 there is some duration3, that equals duration1 plus duration2, ')
(forall ((d1 duration) (d2 duration))
         (exists (d3 duration) 
  
          (= d3 (+ d1 d2))))
     

				
(cl:comment 'If a duration4 equals a duration1 plus a duration2, and a duration5 equals duration4 plus duration3, and a duration6 equals duration2 plus duration3, then duration5 equals duration1 plus duration6.')
(forall ((d1 duration) (d2 duration) (d3 duration))
  (=  (+ (+ d1 d2) d3) (+ d1 (+ d2 d3))) )

				
(cl:comment 'Each duration1 plus duration2 equals duration2 plus duration1.')
(forall ((d1 duration))
   (exists ((d2 duration))
    (= D0 (+ d1 d2))))

				
(cl:comment 'duration that each duration1 equals duration1 plus D0')
(exists (D0) (and
(duration D0)
(forall (d duration)
(= (+ d D0_) d))))

				
(cl:comment 'duration1 equals duration3 plus duration2')
(forall ((d1 duration) (d2 duration) d3)
  (iff
    (= d3 (- d1 d2))
    (and
      (duration d3)
      ("duration3 = duration1 - duration2"
         d3 d1 d2) )))

				
(cl:comment 'D0 equals each duration1 plus some duration2.')
(forall ((d1 duration))
   (exists ((d2 duration))
    (= D0 (+ d1 d2))))

				
(cl:comment 'duration2 is the result of duration1 plus duration1, repeated number times')
(forall ((d1 duration) (n number) d2)
  (iff
    (= d2 (* n d1))
    (and
      (duration d2)
      ("duration2 = number * duration1"
         d2 n d1) )))

				
(cl:comment 'For each number and each duration1, there is a duration2 that is number times duration1.')
(forall ((n1 number) (d1 duration))
  (exists ((d2 duration)) 
     (= d2 (* n1 d1))))

				
(cl:comment 'If a duration3 equals a number1 times (a duration1 plus a duration2) then duration3 equals (number1 times duration1) plus (number1 times duration2).')
(forall ((d1 duration) (d2 duration) 
        (d3 duration) (n1 number))
(if (= d3 (* n1 (+ d1 d2)))
    (= d3 (+ (* n1 d1) (* n1 d2)))))

				
(cl:comment 'If a (number1 plus a number2) times a duration1 equals a duration2, then duration2 equals (number1 times duration1) plus (number2 times duration1).')
(forall  ((d1 duration) (n1 number) (n2 number))
    (= (* (+ n1 n2) d1)  (+ (* n1 d1) (* n2 d1))))

				
(cl:comment 'D0 equals 0 times each duration1.')
(forall ((d1 duration))
  (* 0 d1 D0))

				
(cl:comment 'D0 equals a number1 times a duration1 if and only if number1 equals 0 or duration1 equals D0.')
(forall ((n1 number) (d1 duration))
  (iff (= D0 (* n1 d1)) 
        (or
           (= n1 0)
           (= d1 D0)) ))

				
(cl:comment 'If a duration1 does not equal D0, then a duration2 equals a number1 times duration1.')
(forall ((d1 duration))
  (if (not (= d1 D0))
      (exists ((d2 duration) (n1 number))
           (* d1 n1 d2))))

				
(cl:comment 'the particular duration is the duration that is the amount of time in the time interval')
(forall (d ti) (iff 
 (= d ("duration of time interval" ti))
 (and 
   ("time interval" ti) (duration d)
   ("time interval has duration" ti d) )))

				
(cl:comment 'the particular duration is the duration that is the amount of time in the time interval')
(forall (t d)
  (if ("time interval has duration" t d)
       (and ("time interval" t) (duration d)) ))

				
(cl:comment 'the particular duration is the duration that is the amount of time in the time interval')
(forall (t d)
  (iff (= ("duration of" t) d)
        ("time interval has duration" t d)))

				
(cl:comment 'Each time interval has exactly one duration.')
(forall ((t "time interval") (d1 duration) (d2 duration))
 (if (and ("time interval has duration" t d1)
          ("time interval has duration" t d2))
     (= d1 d2)))

				
(cl:comment 'The duration of each time interval is greater than D0.')
(forall ((t "time interval"))
  (> ("duration of" t) D0))

				
(cl:comment 'The duration of no time interval equals D0.')
(forall ((t "time interval"))
  (not (= ("duration of" t) D0)))

				
(cl:comment 'For each time interval1 there is no time interval2 such that the duration of time interval1 plus the duration of time interval2 equals D0.')
(not (exists ((t1 t2)) 
 ("duration3 = duration1 plus duration2"
  D0 ("duration of time interval" t1)
     ("duration of time interval" t2)) ))

				
(cl:comment 'For each time interval1 and each time interval2 that is a part of time interval1, the duration of time interval2 is less than or equal to the duration of time interval1.')
(forall (t1 t2)
  (if ("time interval1 is part of time interval2" t1 t2)
      (<= ("duration of" t1) ("duration of" t2)) ))

				
(cl:comment 'For each time interval1 and each time interval2 that meets a time interval1, the duration of  time interval1 plus time interval2 is equal to the duration of time interval1 plus the duration of time interval2.')
(forall (t1 t2 t3)
  (if (and 
          ("time interval1 meets time interval2" t1 t2)
          ("time interval3 equals time interval1 plus  time interval2"
                           t3 t1 t2))
      (= (+  ("duration of" t1) ("duration of" t2))
          ("duration of" t3)) ))

				
(cl:comment 'For each time interval2 and each time interval3 that finishes time interval2, the duration of  the time interval1 that starts time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.')
(forall (t1 t2 t3)
  (if ("time interval1 starts time interval2 
        complementing time interval3" t1 t2 t3)
      (= ("duration of" t1)
         (- ("duration of" t2)
            ("duration of" t3)) ) ))

				
(cl:comment 'For each time interval2 and each time interval3 that starts time interval2, the duration of  the time interval1 that finishes time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.')
(forall (t1 t2 t3)
  (if ("time interval1 finishes time interval2  
        complementing time interval3" t1 t2 t3)
      (= ("duration of" t1)
         (- ("duration of" t2)
            ("duration of" t3)) ) ))

				
(cl:comment 'Duration >= D0.')
(forall (t1 t2 d)
 (iff ("time interval2 is duration before 
        time interval1" t1 d t2)
      (and
        ("time interval" t1)
        ("time interval" t2)
        (duration d)
        ("time interval1 is before time 
          interval2" t2 t1)
        (exists ("time interval" t3)
         (and
          ("time interval1 meets time 
            interval2" t2 t3)
          ("time interval1 meets time 
            interval2" t3 t1)
          ("duration1 equals duration2" d
            ("time interval has particular duration" 
              t3)))))))

				
(cl:comment 'Duration >= D0.')
(forall (t1 t2 d)
 (iff ("time interval2 is duration after 
        time interval1" t1 d t2)
      (and
        ("time interval" t1)
        ("time interval" t2)
        (duration d)
        ("time interval1 is after time 
          interval2" t2 self)
        (exists ("time interval" t3)
         (and
          ("time interval1 meets time 
            interval2" self t3)
          ("time interval1 meets time 
            interval2" t3 t2)
          ("duration1 equals duration2" d
            ("time interval has duration" 
              t3)))))))

				
(cl:comment 'the occurrence is a realization of the situation kind')
(forall (s occ)
   (if ("situation kind has occurrence" s occ)
        (and ("situation kind" s) (occurrence occ)) ))

				
(cl:comment 'the occurrence happens continuously, without interruption, in each time interval2 that is part of the time interval')
(forall (occ ti)
   (if  ("occurrence occurs throughout time interval" occ ti)
         (and (occurrence occ) ("time interval" ti)) ))

				
(cl:comment 'the occurrence occurs throughout some time interval2 that is part of the time interval')
(forall (occ t1)
  (iff ("occurrence occurs within time interval" occ t1)
     (and
         (occurrence occ) ("time interval" t1)
         (exists (t2)
            (and
               ("time interval1 is part of time interval2"  t2 t1)
               ("occurrence occurs throughout time interval"
                     occ t2))) )))

				
(cl:comment 'the occurrence occurs throughout the occurrence interval and the occurrence does not occur within some time interval2 that meets the occurrence interval and the occurrence does not occur within some time interval3 that is met by the occurrence interval')
(forall (occ t1)
  (iff ("occurrence occurs for occurrence interval" occ t1)
    (and
      ("occurrence occurs throughout time interval" occ t1)
      (exists (t2 t3)
        (and 
           ("time interval1 meets time interval2" t2 t1)
           (not ("occurrence occurs within time interval" occ t2))
           ("time interval1 meets time interval2" t1 t3)
           (not ("occurrence occurs within time interval" occ t3))
)) )))

				
(cl:comment 'Each occurrence occurs for exactly one occurrence interval.')
(forall (occ) (exists (t)
  (and
    ("occurrence occurs for occurrence interval" occ t)
    (forall (t2)
      (if (occurrence occurs for occurrence interval" occ t2)
           (= t2 t)))
)))

				
(cl:comment 'the occurrence occurs for some occurrence interval and the duration is the duration of the occurrence interval')
(forall (occ d)
  (iff ("occurrence lasts for duration" occ d)
    (and
      (occurrence occ) (duration d)
      (exists (t)
        (and
          ("occurrence occurs for time interval" occ t)
          ("time interval has duration" t d))))))

				
(cl:comment 'the occurrence interval of occurrence1 precedes the occurrence interval of occurrence2')
(forall (o1 o2)
  (iff ("occurrence1 precedes occurrence2" o1 o2)
      (and
        (occurrence o1)  (occurrence o2)
        (forall (t1 t2)
          (if
           (and
             ("occurrence occurs for time interval" o1 t1)
             ("occurrence occurs for time interval" o2 t2))
           ("time interval1 precedes time interval2" t1 t2)))
)))

				
(cl:comment 'If some occurrence1 precedes some occurrence2, and if the occurrence2 precedes some occurrence3, then occurrence1 precedes occurrence3.')
(forall (o1 o2 o3)
  (if (and
         ("occurrence1 precedes occurrence2" o1 o2)
         ("occurrence1 precedes occurrence2" o2 o3))
       ("occurrence1 precedes occurrence2"  o1 o3)))

				
(cl:comment 'the occurrence interval of occurrence1 starts before the occurrence interval of occurrence2')
(forall (o1 o2)
  (iff ("occurrence1 starts before occurrence2" o1 o2)
    (and
      (occurrence o1)  (occurrence o2)
      (forall (t1 t2)
        (if
          (and
            ("occurrence occurs for time interval" o1 t1)
            ("occurrence occurs for time interval" o2 t2))
          ("time interval1 starts before time interval2" t1 t2)))
)))

				
(cl:comment 'the occurrence interval of occurrence1 ends before the occurrence interval of occurrence2  ')
(forall (o1 o2)
  (iff ("occurrence1 ends before occurrence2" o1 o2)
    (and
      (occurrence o1)  (occurrence o2)
      (forall (t1 t2)
        (if
          (and
            ("occurrence occurs for time interval" o1 t1)
            ("occurrence occurs for time interval" o2 t2))
          ("time interval1 ends before time interval2" t1 t2)))
)))

				
(cl:comment 'the occurrence interval of occurrence1 overlaps the occurrence interval of occurrence2')
(forall (o1 o2)
 (if ("o1 overlaps o2")
     (and
        (occurrence o1)
        (occurrence o2)
        (forall ((t1 "time interval") 
                   (t2 "time interval"))
          (if (and
                ("occurrence occurs for time interval"
                  o1 t1) 
                ("occurrence occurs for time interval"
                  o2 t2))
               ("time interval1 overlaps time interval2"
                  t1 t2))))))

				
(cl:comment 'occurrence1 follows occurrence2 and occurrence1 precedes occurrence3')
(forall (o1 o2 o3)
  (iff ("occurrence1 is between occurrence2 and occurrence3" 
                  o1 o2 o3)
    (and 
      ("occurrence precedes occurrence" o2 o1)
      ("occurrence precedes occurrence" o1 o3)) ))

				
(cl:comment 'each occurrence of situation kind1 precedes each occurrence of situation kind2  ')
(forall (s1 s2)
  (iff ("situation kind1 precedes situation kind2" s1 s2)
       (forall (o1 o2)
         (if
           (and
              ("situation kind has occurrence" s1 o1)
              ("situation kind has occurrence" s2 o2))
           ("occurrence1 precedes occurrence2" o1 o2)) )))

				
(cl:comment 'each occurrence of situation kind1 starts before each occurrence of situation kind')
(forall (s1 s2)
  (iff ("situation kind1 starts before situation kind2" s1 s2)
     (and 
       ("situation kind" s1) ("situation kind" s2)
       (forall (o1 o2)
          (if
           (and
              ("situation kind has occurrence" s1 o1)
              ("situation kind has occurrence" s2 o2))
           ("occurrence1 starts before occurrence2" o1 o2)))
)))

				
(cl:comment 'each occurrence of situation kind1 ends before each occurrence of situation kind2 ')
(forall (s1 s2)
  (iff ("situation kind1 ends before situation kind2" s1 s2)
     (and 
       ("situation kind" s1) ("situation kind" s2)
       (forall (o1 o2)
          (if
           (and
              ("situation kind has occurrence" s1 o1)
              ("situation kind has occurrence" s2 o2))
           ("occurrence1 ends before occurrence2" o1 o2)))
)))

				
(cl:comment 'each occurrence of situation kind1 overlaps some occurrence of situation kind2')
(forall (s1 s2)
 (iff ("situation kind1 overlaps 
        situation kind2" s1 s2)
  (and
   ("situation kind" s1)
   ("situation kind" s2)
   (forall (o1 o2)
    (and
     (occurrence o1)
     (occurrence o2)
     (if (and 
          ("situation kind has occurrence"
           s1 o1)
         ("situation kind has occurrence"
          s2 o2))
        ("occurrence1 overlaps occurrence2"
         o1 o2)))))))

				
(cl:comment 'set of individual situation kinds that has a time table and that is for a general situation kind and each individual situation kind refines the general situation kind and each individual situation kind occurs for a table entry of the time table')
(forall (s)
  (iff ("schedule" s)
    (and
      (exists ((g "general situation kind")
               (tt "time table"))
        (and
          ("schedule is for general situation kind" s g)
          ("schedule has time table" s tt)
          (set s)
          (forall ((i thing))
            (if
              ("set has element" s i)
              (and
                ("individual situation kind" i)
                ("refinement refines situation kind" i g)
                (exists ((te "table entry"))
                  (and|
                    ("time table has table entry" tt te)
                    ("situation kind occurs for time 
                      interval" i te)))
             
 ))))))))


				
(cl:comment 'each table entry of the time table is the occurrence interval of some individual situation kind that is a member of the schedule')
(forall (s tt)
  (iff ("schedule has time table" s tt)
    (and
       (schedule s) ("time table" tt)
       (forall (ti)
          (if
             ("time table has table entry" tt ti)
             (exists (i)
                (and
                    ("set has member" s i)
      ("individual situation kind occurs over time interval" i ti))
))) )))

				
(cl:comment 'the time table period of the time table of the schedule.')
(forall (s span)
  (iff ("schedule has time span" s span)
   (and
     (schedule s) ("time interval" span)
     (forall (tt) 
       (if 
         ("schedule has time table" s tt)
         ("time table has time table period" tt span)))
)))

				
(cl:comment 'Each sequence position is of exactly one sequence.')
(forall (seq sp)
  (if ("sequence has sequence position" seq sp)
    (and
       (sequence seq)
       ("sequence position" sp)
       (forall (seq2)
         (if ("sequence has sequence position" seq2 sp)
              (= seq2 seq))) )))

				
(cl:comment 'If the index1 of some sequence position1 of some sequence equals the index2 of some sequence position2 of the sequence then sequence position1 is sequence position2.')
(forall (seq sp1 sp2 x1 x2)
  (if 
    (and
       ("sequence has sequence position" seq sp1)
       ("sequence has sequence position" seq sp2)
       ("sequence position has index" sp1 x1)
       ("sequence position has index" sp2 x2)
       (= x1 x2) )
   (= sp1 sp2) ))

				
(cl:comment 'If the index1 of some sequence position1 of some sequence equals the index2 of some sequence position2 of the sequence then sequence position1 is sequence position2.')
(forall ((sp "sequence position"))
  (exists ((x1 "integer"))
     (and
       ("sequence position has index" sp x1)
       (forall (x2)
         (if
           ("sequence position has index" sp x2)
           (= x1 x2)) ) )))

				
(cl:comment 'the index of sequence position1 is less than the index of sequence position2 .')
(forall (sp1 sp2 x1 x2)
  (if 
    (and
       ("sequence position has index" sp1 x1)
       ("sequence position has index" sp2 x2) )
    (iff ("sequence position1 precedes sequence position2"
                  sp1 sp2)
           (exists ((seq sequence))
              (and
                ("sequence has sequence position" seq sp1)
                ("sequence has sequence position" seq sp2)
                (< x1 x2) )) ))) 

				
(cl:comment 'Each sequence position has at most one next sequence position. ')
(forall (sp nsp)
  (iff ("next sequence position succeeds sequence position" 
                      nsp sp)
     (and
        ("sequence position1 precedes sequence position2" 
                      sp nsp)
        (not (exists (sp2)
          (and 
            ("sequence position1 precedes sequence position2" 
                      sp sp2)
            ("sequence position1 precedes sequence position2" 
                      sp2 nsp)) )) )))

				
(cl:comment 'the member is the member of a sequence position of the sequence')
(forall ((s sequence) (member thing))
  (iff ("sequence has member" s member)
       (exists ((sp "sequence position"))
        (and ("sequence has sequence position" s sp)
             ("sequence position has member" sp m)))))

				
(cl:comment 'The sequence has a sequence position that has an index that equals the index, and the sequence position has a member that is the member.')
(forall (member index s)
 (iff ("member has index in sequence" member index s)
   (and
      (sequence s) (integer index) 
      (exists (sp)
       (and
         ("sequence has sequence position" s sp)
         ("sequence position has index" sp index)
         ("sequence position has member" sp member)) ))))

				
(cl:comment 'The sequence has a sequence position that has an index that equals the index, and the sequence position has a member that is the member.')
(forall (member index s)
   (iff (= index ("index of member in sequence" member s))
         ("member has index in sequence" member index s) ))

				
(cl:comment 'The sequence has a sequence position that has an index that equals the index, and the sequence position has a member that is the member.')
(forall (member index s)
 (iff (= member ("member with index in sequence" index 
        s))
       ("member has index in sequence" member index s) ))

				
(cl:comment 'The concept corresponds to each member of the sequence.')
(forall (s c)
   (iff ("sequence is of concept" s c)
     (and
       (sequence s) (concept c)
       (forall (member)
         (if ("member participates in sequence" member s)
              ("meaning corresponds to thing" c member))) 
     )))

				
(cl:comment 'Each sequence has at most one index origin value.')
(forall (seq) (exists (iov)
  (if ("sequence has index origin value" seq iov)
       (and
          (integer iov)
          (forall (iv2)
             (if ("sequence has index origin value" 
                  seq iv2)
                  (= iov iv2)) )))))

				
(cl:comment 'The index of the index origin position equals the index origin value of the sequence.')
(forall (s p)
 (iff ("sequence has index origin position" s p)
    (exists (iov)
       (and
        ("sequence has index origin value" s iov)
        ("sequence position has index" p iov) ))))

				
(cl:comment 'sequence that each sequence position of the sequence that is not the first position of the sequence is next after a sequence position2, and the index of the sequence position equals 1 plus the index of the sequence position2')
(forall (s)  (iff ("consecutive sequence" s)
  (and
   (sequence s)
   (forall (sp1)
    (if 
      (and
        ("sequence has sequence position" s sp1)
        (exists (sp2)
          ("next sequence position succeeds sequence position" 
                    sp2 sp1)) )
      (forall (x1 x2)
        (if 
          (and
             ("sequence position has index" sp1 x1)
             ("sequence position has index" sp2 x2))
          (=  x2 (+ x1 1)) ))
)) )))

				
(cl:comment 'sequence that each member of the sequence is the member of at most one sequence position of the sequence')
(forall (s)
 (iff ("unique sequence" s)
   (forall (member x1 x2)
     (if 
      (and 
        ("member has index in sequence" member x1 s)
        ("member has index in sequence" member x2 s))
      (= x1 x2) ))))

				
(cl:comment 'consecutive sequence that is a unique sequence')
(forall (s)
 (iff ("regular sequence" s)
  (and
     ("consecutive sequence" s)
     ("unique sequence" s))))

				
(cl:comment 'member1 participates in the unique sequence and member2 participates in the unique sequence and each sequence position1 of member1 in the unique sequence precedes each sequence position2 of member2 in the unique sequence')
(forall ((s sequence)(m1 thing)(m2 thing))
 (iff ("member1 precedes member2 in unique sequence" 
       m1 m2 s)
      (and
        ("member participates in sequence" m1 s)
        ("member participates in sequence" m2 s)
        (forall ((sp1 "sequence position")
                 (sp2 "sequence position"))
          (if
            (and
              ("sequence position of member" sp1 m1)
              ("sequence position of member" sp2 m2))
           ("sequence position1 precedes 
             sequence position2" sp1 sp2))))))

				
(cl:comment 'the first member is the member of the first position of the sequence')
(forall (s m)
 (iff ("sequence has first member" s m)
  (exists (first)
   (and
    ("sequence has first position" s first)
    ("sequence position has member" first m)))))

				
(cl:comment 'the last member is the member of the last position of the sequence')
(forall (s m)
 (iff ("sequence has last member" s m)
  (exists (last)
   (and
    ("sequence has last position" s last)
    ("sequence position has member" last m)))))

				
(cl:comment 'thing is the member of exactly one sequence position in the unique sequence and next member is the member of some sequence position of the unique sequence that succeeds the sequence position of the thing')
(forall (s nm m)
  (iff
   ("next member is next after thing in unique sequence"
                  nm m s)
   (and
     ("unique sequence" s)
     (exists (sp nsp)
      (and
        ("sequence has sequence position" s sp)
        ("sequence position has member" sp m)
        ("next sequence position succeeds sequence position" 
                  nsp sp)
        ("sequence position has member" nsp nm) )))))

				
(cl:comment 'The last member of each sequence has no next member.')
(forall (s last)
 (if 
   ("sequence has last member" s last)
   (not (exists (m)
     ("member is next after thing in sequence" m last s) ))))

				
(cl:comment 'Each member that participates in a unique sequence and that has no next member in the unique sequence is the last member of the unique sequence.')
(forall (s m)
 (if
   (and 
     ("sequence has member" s m)
     (not (exists (nm)
       ("next member is next after thing in sequence" nm m s) )))
   ("sequence has last member" s m)))

				
(cl:comment 'thing is the member of exactly one sequence position in the unique sequence and previous member is the member of some sequence position of the unique sequence that is just before the sequence position of the thing')
(forall (s pm m)
  (iff
   ("previous member is just before thing in unique sequence"
                  pm m s)
   (and
     ("unique sequence" s)
     (exists (sp psp)
      (and
        ("sequence has sequence position" s sp)
        ("sequence position has member" sp m)
        ("next sequence position succeeds sequence position" 
                  sp psp)
        ("sequence position has member" psp pm) )))))

				
(cl:comment 'The first member of each sequence has no previous member.')
(forall (s first)
 (if 
   ("sequence has first member" s first)
   (not (exists (m)
     ("previous member is just before thing in sequence" m first s) ))))


(cl:comment 'Each member that participates in a unique sequence and that has no previous member in the unique sequence is the first member of the unique sequence.')
(forall (s m)
 (if
   (and 
     ("sequence has member" s m)
     (not (exists (nm)
       ("previous member is just before thing in sequence" nm m s)
    )))
   ("sequence has first member" s m)))

				
(cl:comment 'Each quantity has exactly one quantity kind.')
(forall ((q quantity))
 (exists ((qk "quantity kind"))
  (and
    ("quantity has quantity kind" q qk)
    (forall (qk2)
     (if
      ("quantity has quantity kind" q qk2)
      (= qk2 qk) )) )))

				
(cl:comment 'Each system of units is for exactly one system of quantities.')
(forall (("system of units" "system of units"))
        (= (count 
            ("system of units is for system of quantities"
              "system of units"))
           1))

				
(cl:comment 'Each part is part of the part.')
(forall (part)
 ("part of" part part))

				
(cl:comment 'If the part is part of the whole and the whole is part of the part then the part is the whole.')
(forall ((part thing) (whole thing))
 (if (and ("part of" part whole)
          ("part of" whole part))
     (= part whole))) 

				
(cl:comment 'If the part is part of some whole and the whole is part of some part3 then the part is part of part3.')
(forall ((part thing) (whole thing) (part3 thing))
  (if (and ("part of" part whole) 
           ("part of" whole part3))
      ("part of" part part3)))

				
(cl:comment 'There exists a part3 that is part of the part1 and the part3 is part of the part2.')
(forall ((part1 thing) (part2 thing))
 (iff (overlaps part1 part2)
      (exists ((part3 thing))
       (and
        ("part of" part3 part1)
        ("part of" part3 part2)))))

				
(cl:comment 'the part is part of the whole and the whole is not part of the part')
(forall ((whole thing) (part thing))
 (iff ("proper part " part whole)
      (and
       ("part of" part whole)
       (not ("part of" whole part)))))

				
(cl:comment 'If a part1 is a proper part of a whole then there exists a part2 that is a proper part of the whole and part2 does not overlap part1.')
(forall (part1 whole)
 (if ("proper part" part1 whole)
     (exists (part2)
      (and
       ("proper part" part2 whole)
       (not (overlaps part2 part1)) ))))