|
1. |
(forall (?VAR1 ?VAR2)
(=>
(instance ?VAR2 Object)
(and
(=>
(and
(attribute ?VAR2 ?VAR1)
(instance ?VAR1 Christian))
(member ?VAR2 Christianity))
(=>
(member ?VAR2 Christianity)
(and
(attribute ?VAR2 ?VAR1)
(instance ?VAR1 Christian)))))) | [ kb_SUMO_5] | For all an attribute and an object |
|
2. |
(forall (?VAR1)
(=>
(instance ?VAR1 Collection)
(exists (?VAR2)
(and
(instance ?VAR2 Object)
(member ?VAR2 ?VAR1))))) | [ kb_SUMO_12977] | For all a collection |
|
3. |
(instance immediateInstance IrreflexiveRelation) | [ kb_SUMO_74086] | immediate instance is an instance of irreflexive relation |
|
4. |
(forall (?VAR1 ?VAR2)
(=>
(instance ?VAR2 SetOrClass)
(=>
(instance ?VAR1 ?VAR2)
(immediateInstance ?VAR1 ?VAR2)))) | [ kb_SUMO_4447] | For all an entity and a set or class |
|
5. |
(instance Christianity Collection) | [ kb_SUMO_31811] | Christianity is an instance of collection |
|
6. |
(instance Christian SetOrClass) | [ kb_SUMO_24195] | Christian is an instance of set or class |
|
7. |
(forall (?VAR1)
(or
(not
(instance immediateInstance IrreflexiveRelation))
(not
(immediateInstance ?VAR1 ?VAR1)))) | 8 [shift_quantors] | For all an entity immediate instance is not an instance of irreflexive relation or the entity is not an immediate instance of the entity |
|
8. |
(forall (?VAR1 ?VAR2)
(and
(or
(or
(or
(not
(attribute ?VAR2 ?VAR1))
(not
(instance ?VAR1 Christian)))
(member ?VAR2 Christianity))
(not
(instance ?VAR2 Object)))
(or
(or
(attribute ?VAR2 ?VAR1)
(not
(member ?VAR2 Christianity)))
(not
(instance ?VAR2 Object)))
(or
(or
(instance ?VAR1 Christian)
(not
(member ?VAR2 Christianity)))
(not
(instance ?VAR2 Object))))) | 1 [distribute] | For all an attribute and an object the attribute is not an attribute of the object or the attribute is not an instance of christian or the object is a member of christianity or the object is not an instance of object and the attribute is an attribute of the object or the object is not a member of christianity or the object is not an instance of object and the attribute is an instance of christian or the object is not a member of christianity or the object is not an instance of object |
|
9. |
(forall (?VAR1)
(and
(or
(instance
(?VAR1) Object)
(not
(instance ?VAR1 Collection)))
(or
(member
(?VAR1) ?VAR1)
(not
(instance ?VAR1 Collection))))) | 2 [distribute] | For all a collection the collection is an instance of object or the collection is not an instance of collection and the collection is a member of the collection or the collection is not an instance of collection |
|
10. |
(or
(not
(immediateInstance ?VAR1 ?VAR1))
(not
(instance immediateInstance IrreflexiveRelation))) | 7 [split_conjunct] | An entity is not an immediate instance of the entity or immediate instance is not an instance of irreflexive relation |
|
11. |
(forall (?VAR1 ?VAR2)
(or
(not
(instance ?VAR2 SetOrClass))
(not
(instance ?VAR1 ?VAR2))
(immediateInstance ?VAR1 ?VAR2))) | 4 [variable_rename] | For all an entity and a set or class the set or class is not an instance of set or class or the entity is not an instance of the set or class or the entity is an immediate instance of the set or class |
|
12. |
(or
(instance ?VAR1 Christian)
(not
(instance ?VAR2 Object))
(not
(member ?VAR2 Christianity))) | 8 [split_conjunct] | An entity is an instance of christian or an object is not an instance of object or the object is not a member of christianity |
|
13. |
(or
(member
(?VAR1) ?VAR1)
(not
(instance ?VAR1 Collection))) | 9 [split_conjunct] | A collection is a member of the collection or the collection is not an instance of collection |
|
14. |
(not
(immediateInstance ?VAR1 ?VAR1)) | 10 3 [cn] | An entity is not an immediate instance of the entity |
|
15. |
(or
(immediateInstance ?VAR1 ?VAR2)
(not
(instance ?VAR1 ?VAR2))
(not
(instance ?VAR2 SetOrClass))) | 11 [split_conjunct] | An entity is an immediate instance of a set or class or the entity is not an instance of the set or class or the set or class is not an instance of set or class |
|
16. |
(or
(instance ?VAR1 Christian)
(not
(instance
(Christianity) Object))) | 12 13 5 [cn] | An entity is an instance of christian or christianity is not an instance of object |
|
17. |
(or
(instance
(?VAR1) Object)
(not
(instance ?VAR1 Collection))) | 9 [split_conjunct] | An entity is an instance of object or the entity is not an instance of collection |
|
18. |
(or
(not
(instance ?VAR1 SetOrClass))
(not
(instance ?VAR1 ?VAR1))) | 14 15 [spm] | A set or class is not an instance of set or class or the set or class is not an instance of the set or class |
|
19. |
(instance ?VAR1 Christian) | 16 17 5 [cn] | An entity is an instance of christian |
|
20. |
QED | 18 6 19 [cn] | true |
