The dog visits the lion. The lion is cold. The lion is kind. The lion is young. The lion likes the rabbit. The lion needs the dog. The lion needs the rabbit. The rabbit is cold. The rabbit is kind. The rabbit is red. The rabbit likes the dog. The rabbit likes the lion. If someone is red then they need the rabbit. If someone is red and nice then they need the rabbit. If the dog is nice then the dog visits the rabbit. If someone likes the rabbit and the rabbit visits the dog then they visit the dog. If someone is red and they visit the lion then they are kind. If someone visits the rabbit and they are cold then the rabbit likes the dog. If someone is kind and they visit the rabbit then the rabbit needs the lion. If someone is cold and they like the dog then the dog likes the lion.
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
If someone is red then they need the rabbit.
((("someone" "is" "red" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone is red and nice then they need the rabbit.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "needs" "rabbit" "+"))
If the dog is nice then the dog visits the rabbit.
((("dog" "is" "nice" "+")) -> ("dog" "visits" "rabbit" "+"))
If someone likes the rabbit and the rabbit visits the dog then they visit the dog.
((("someone" "likes" "rabbit" "+") ("rabbit" "visits" "dog" "+")) -> ("someone" "visits" "dog" "+"))
If someone is red and they visit the lion then they are kind.
((("someone" "is" "red" "+") ("someone" "visits" "lion" "+")) -> ("someone" "is" "kind" "+"))
If someone visits the rabbit and they are cold then the rabbit likes the dog.
((("someone" "visits" "rabbit" "+") ("someone" "is" "cold" "+")) -> ("rabbit" "likes" "dog" "+"))
If someone is kind and they visit the rabbit then the rabbit needs the lion.
((("someone" "is" "kind" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "needs" "lion" "+"))
If someone is cold and they like the dog then the dog likes the lion.
((("someone" "is" "cold" "+") ("someone" "likes" "dog" "+")) -> ("dog" "likes" "lion" "+"))
The lion needs the rabbit.
True
1
proof
[(triple7)]
("lion" "needs" "rabbit" "+")
triple7
The lion does not like the rabbit.
False
1
inv-proof
[(triple5)]
("lion" "likes" "rabbit" "-")
triple5
The dog likes the lion.
True
3
proof
[(((triple8 triple11) -> rule8))]
("dog" "likes" "lion" "+")
((triple8 triple11) -> (rule8 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple10) -> rule1))]
("rabbit" "needs" "rabbit" "-")
((triple10) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The dog does not visit the rabbit.
Unknown
inv-rconc
[@1: The dog visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "rabbit" "-")
The rabbit needs the lion.
Unknown
rconc
[@2: The rabbit needs the lion.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("rabbit" "needs" "lion" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The dog visits the lion.[(triple1)] The lion is cold.[(triple2)] The lion is kind.[(triple3)] The lion is young.[(triple4)] The lion likes the rabbit.[(triple5)] The lion needs the dog.[(triple6)] The lion needs the rabbit.[(triple7)] The rabbit is cold.[(triple8)] The rabbit is kind.[(triple9)] The rabbit is red.[(triple10)] The rabbit likes the dog.[(triple11)] The rabbit likes the lion.[(triple12)] @1: The dog likes the lion.[(((triple8 triple11) -> rule8))] The rabbit needs the rabbit.[(((triple10) -> rule1))]
The dog visits the lion.
("dog" "visits" "lion" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
triple4
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple5
The lion needs the dog.
("lion" "needs" "dog" "+")
triple6
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple10
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple11
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple12
The dog likes the lion.
("dog" "likes" "lion" "+")
((triple8 triple11) -> (rule8 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple10) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1