The cat likes the rabbit. The cat needs the rabbit. The lion is round. The lion likes the rabbit. The rabbit chases the cat. The rabbit is young. The rabbit likes the lion. If the lion likes the cat and the lion is big then the lion is kind. If the cat needs the lion and the cat chases the rabbit then the rabbit is kind. If something needs the cat and the cat is young then it is young. If something chases the rabbit then it needs the lion. If something needs the rabbit then the rabbit is young. If the rabbit is round and the rabbit chases the lion then the lion is kind.
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
If the lion likes the cat and the lion is big then the lion is kind.
((("lion" "likes" "cat" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "kind" "+"))
If the cat needs the lion and the cat chases the rabbit then the rabbit is kind.
((("cat" "needs" "lion" "+") ("cat" "chases" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
If something needs the cat and the cat is young then it is young.
((("something" "needs" "cat" "+") ("cat" "is" "young" "+")) -> ("something" "is" "young" "+"))
If something chases the rabbit then it needs the lion.
((("something" "chases" "rabbit" "+")) -> ("something" "needs" "lion" "+"))
If something needs the rabbit then the rabbit is young.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If the rabbit is round and the rabbit chases the lion then the lion is kind.
((("rabbit" "is" "round" "+") ("rabbit" "chases" "lion" "+")) -> ("lion" "is" "kind" "+"))
The cat likes the rabbit.
True
1
proof
[(triple1)]
("cat" "likes" "rabbit" "+")
triple1
The rabbit does not chase the cat.
False
1
inv-proof
[(triple5)]
("rabbit" "chases" "cat" "-")
triple5
The cat does not need the lion.
Unknown
inv-rconc
[@1: The cat needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "lion" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat likes the rabbit.[(triple1)] The cat needs the rabbit.[(triple2)] The lion is round.[(triple3)] The lion likes the rabbit.[(triple4)] The rabbit chases the cat.[(triple5)] The rabbit is young.[(triple6 OR ((triple2) -> rule5))] The rabbit likes the lion.[(triple7)]
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple4
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple5
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
((triple2) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple7