The lion likes the rabbit. The rabbit visits the lion. If the rabbit likes the lion and the rabbit chases the lion then the lion visits the rabbit. If someone likes the lion then they are cold. If the rabbit is big then the rabbit is cold. If the rabbit visits the lion and the rabbit is blue then the lion likes the rabbit. If the rabbit visits the lion then the lion is blue. If someone visits the rabbit then the rabbit is green. If someone visits the rabbit and the rabbit visits the lion then the rabbit is not green. If someone likes the rabbit and they are blue then they visit the lion.
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If the rabbit likes the lion and the rabbit chases the lion then the lion visits the rabbit.
((("rabbit" "likes" "lion" "+") ("rabbit" "chases" "lion" "+")) -> ("lion" "visits" "rabbit" "+"))
If someone likes the lion then they are cold.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "cold" "+"))
If the rabbit is big then the rabbit is cold.
((("rabbit" "is" "big" "+")) -> ("rabbit" "is" "cold" "+"))
If the rabbit visits the lion and the rabbit is blue then the lion likes the rabbit.
((("rabbit" "visits" "lion" "+") ("rabbit" "is" "blue" "+")) -> ("lion" "likes" "rabbit" "+"))
If the rabbit visits the lion then the lion is blue.
((("rabbit" "visits" "lion" "+")) -> ("lion" "is" "blue" "+"))
If someone visits the rabbit then the rabbit is green.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If someone visits the rabbit and the rabbit visits the lion then the rabbit is not green.
((("someone" "visits" "rabbit" "+") ("rabbit" "visits" "lion" "+")) -> ("rabbit" "is" "green" "-"))
If someone likes the rabbit and they are blue then they visit the lion.
((("someone" "likes" "rabbit" "+") ("someone" "is" "blue" "+")) -> ("someone" "visits" "lion" "+"))
The lion likes the rabbit.
True
1
proof
[(triple1)]
("lion" "likes" "rabbit" "+")
triple1
The lion does not like the rabbit.
False
1
inv-proof
[(triple1)]
("lion" "likes" "rabbit" "-")
triple1
The lion is blue.
True
2
proof
[(((triple2) -> rule5))]
("lion" "is" "blue" "+")
((triple2) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple2) -> rule5))]
("lion" "is" "blue" "-")
((triple2) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion visits the lion.
True
4
proof
[(((triple1 ((triple2) -> rule5)) -> rule8))]
("lion" "visits" "lion" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion does not visit the lion.
False
4
inv-proof
[(((triple1 ((triple2) -> rule5)) -> rule8))]
("lion" "visits" "lion" "-")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion does not visit the rabbit.
Unknown
inv-rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "rabbit" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "cold" "+")
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "cold" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
The rabbit does not chase the lion.
Unknown
inv-random
[@0: The rabbit chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "lion" "-")
The lion chases the rabbit.
Unknown
random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "+")
@0: The lion likes the rabbit.[(triple1)] The rabbit visits the lion.[(triple2)] @1: The lion is blue.[(((triple2) -> rule5))] @2: The lion visits the lion.[(((triple1 ((triple2) -> rule5)) -> rule8))]
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
((triple2) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2