occupies spatial region at some time located-at-r_st (forall (x y r_1 t) (if (and (occupiesSpatialRegionAt x r_1 t) (continuantPartOfAt y x t)) (exists (r_2) (and (continuantPartOfAt r_2 r_1 t) (occupiesSpatialRegionAt y r_2 t))))) // axiom label in BFO2 CLIF: [043-001] BFO2 Reference: independent continuant Alan Ruttenberg: This is a binary version of a ternary time-indexed, instance level, relation. The BFO reading of the binary relation 'occupies spatial region at some time@en' is: exists t, exists_at(x,t) & exists_at(y,t) & 'occupies spatial region@en'(x,y,t) (forall (x r t) (if (occupiesSpatialRegionAt x r t) (and (SpatialRegion r) (IndependentContinuant x)))) // axiom label in BFO2 CLIF: [041-002] BFO2 Reference: spatial region (forall (r t) (if (Region r) (occupiesSpatialRegionAt r r t))) // axiom label in BFO2 CLIF: [042-002] b occupies_spatial_region r at t means that r is a spatial region in which independent continuant b is exactly located (axiom label in BFO2 Reference: [041-002]) every region r is occupies_spatial_region r at all times. (axiom label in BFO2 Reference: [042-002]) if b occupies_spatial_region r at t & b continuant_part_of b at t, then there is some r which is continuant_part_of r at t such that b occupies_spatial_region r at t. (axiom label in BFO2 Reference: [043-001]) occupiesSpatialRegionAt has spatial occupant at some time independent continuant spatial region