|
1. |
(forall (?VAR1)
(=>
(instance ?VAR1 Collection)
(exists (?VAR2)
(and
(instance ?VAR2 Object)
(member ?VAR2 ?VAR1))))) | [ kb_SUMO_12977] | |
|
2. |
(instance PuertoRico Christian) | [ conj1] | |
|
3. |
(instance Christianity Collection) | [ kb_SUMO_31811] | |
|
4. |
(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))))) | 5 [distribute] | |
|
5. |
(forall (?VAR1)
(and
(or
(instance
(?VAR1) Object)
(not
(instance ?VAR1 Collection)))
(or
(member
(?VAR1) ?VAR1)
(not
(instance ?VAR1 Collection))))) | 1 [distribute] | |
|
6. |
(not
(instance PuertoRico Christian)) | [Negated Query] | |
|
7. |
(or
(instance ?VAR1 Christian)
(not
(instance ?VAR2 Object))
(not
(member ?VAR2 Christianity))) | 4 [split_conjunct] | |
|
8. |
(or
(member
(?VAR1) ?VAR1)
(not
(instance ?VAR1 Collection))) | 5 [split_conjunct] | |
|
9. |
(or
(instance ?VAR1 Christian)
(not
(instance
(Christianity) Object))) | 7 8 3 [cn] | |
|
10. |
(or
(instance
(?VAR1) Object)
(not
(instance ?VAR1 Collection))) | 5 [split_conjunct] | |
|
11. |
(not
(instance PuertoRico Christian)) | [split_conjunct] | |
|
12. |
(instance ?VAR1 Christian) | 9 10 3 [cn] | |
|
13. |
QED | 11 12 [cn] | |
