The dog likes the lion. The lion is round. The lion sees the dog. If someone is big then they are round. If someone likes the lion and the lion is young then they see the lion.
The dog likes the lion.
("dog" "likes" "lion" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone likes the lion and the lion is young then they see the lion.
((("someone" "likes" "lion" "+") ("lion" "is" "young" "+")) -> ("someone" "sees" "lion" "+"))
The lion sees the dog.
True
1
proof
[(triple3)]
("lion" "sees" "dog" "+")
triple3
The dog does not like the lion.
False
1
inv-proof
[(triple1)]
("dog" "likes" "lion" "-")
triple1
The dog does not see the lion.
Unknown
inv-rconc
[@1: The dog sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "lion" "-")
The lion likes the dog.
Unknown
random
[@0: The lion likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "dog" "+")
@0: The dog likes the lion.[(triple1)] The lion is round.[(triple2)] The lion sees the dog.[(triple3)]
The dog likes the lion.
("dog" "likes" "lion" "+")
triple1
The lion is round.
("lion" "is" "round" "+")
triple2
The lion sees the dog.
("lion" "sees" "dog" "+")
triple3