;; Auto-generated by suo-kif-to-metta.sh

;; Self-contained SUO-KIF file extracted from
;;
;; https://github.com/ontologyportal/sumo/blob/master/Merge.kif
;;
;; containing knowledge about `located` and related symbols.

(subclass TransitiveRelation BinaryRelation)
(disjoint TransitiveRelation IntransitiveRelation)

(documentation TransitiveRelation EnglishLanguage "A &%BinaryRelation $REL is transitive
if ($REL $INST1 $INST2) and ($REL $INST2 $INST3) imply ($REL $INST1 $INST3),
for all $INST1, $INST2, and $INST3.")

;; TODO: re-enable when ($REL $INST1 $INST2) does not lead to an
;; infinite recursion.
;;
;; (⟹
;;    (instance $REL TransitiveRelation)
;;    (∀ ($INST1 $INST2 $INST3)
;;       (⟹
;;          (∧
;;             ($REL $INST1 $INST2)
;;             ($REL $INST2 $INST3))
;;          ($REL $INST1 $INST3))))

;; In the meantime we manually instantiate the relation located.  We
;; remove the ∀ in the process to avoid ($INST1 $INST2 $INST3) which
;; also leads to an infinite recursion, and is not actually mandatory
;; anymore.
(⟹
   (∧
      (located $INST1 $INST2)
      (located $INST2 $INST3))
   (located $INST1 $INST3))

(instance located TransitiveRelation)

(⟹
   (orientation $OBJ1 $OBJ2 Inside)
   (located $OBJ1 $OBJ2))

;; Add instances of `located`, extracted from
;;
;; https://github.com/ontologyportal/sumo/blob/master/tests/SP03.kif.tq
;;
;; to test it.

(instance JohnsHouse Building)
(instance John Human)
(instance SanJose City)
(orientation John JohnsHouse Inside)
(located JohnsHouse SanJose)

;; An example of query would be
;;
;; (located John SanJose)