The bear likes the lion. The lion likes the rabbit. The rabbit is big. If someone likes the rabbit then the rabbit likes the bear. If someone likes the bear and the bear likes the lion then the lion likes the bear. If someone eats the rabbit and the rabbit is red then the rabbit eats the bear. If someone is red and round then they do not eat the lion. If someone likes the bear then they eat the lion. If someone is kind and they chase the rabbit then they eat the rabbit. If someone is red and round then they like the rabbit. If the lion is rough and the lion likes the rabbit then the lion is red.
The bear likes the lion.
("bear" "likes" "lion" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
If someone likes the rabbit then the rabbit likes the bear.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "likes" "bear" "+"))
If someone likes the bear and the bear likes the lion then the lion likes the bear.
((("someone" "likes" "bear" "+") ("bear" "likes" "lion" "+")) -> ("lion" "likes" "bear" "+"))
If someone eats the rabbit and the rabbit is red then the rabbit eats the bear.
((("someone" "eats" "rabbit" "+") ("rabbit" "is" "red" "+")) -> ("rabbit" "eats" "bear" "+"))
If someone is red and round then they do not eat the lion.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "eats" "lion" "-"))
If someone likes the bear then they eat the lion.
((("someone" "likes" "bear" "+")) -> ("someone" "eats" "lion" "+"))
If someone is kind and they chase the rabbit then they eat the rabbit.
((("someone" "is" "kind" "+") ("someone" "chases" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is red and round then they like the rabbit.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "likes" "rabbit" "+"))
If the lion is rough and the lion likes the rabbit then the lion is red.
((("lion" "is" "rough" "+") ("lion" "likes" "rabbit" "+")) -> ("lion" "is" "red" "+"))
The rabbit is big.
True
1
proof
[(triple3)]
("rabbit" "is" "big" "+")
triple3
The lion does not like the rabbit.
False
1
inv-proof
[(triple2)]
("lion" "likes" "rabbit" "-")
triple2
The rabbit likes the bear.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "likes" "bear" "+")
((triple2) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The rabbit does not like the bear.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "likes" "bear" "-")
((triple2) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The lion likes the bear.
True
4
proof
[(((((triple2) -> rule1) triple1) -> rule2))]
("lion" "likes" "bear" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The lion does not like the bear.
False
4
inv-proof
[(((((triple2) -> rule1) triple1) -> rule2))]
("lion" "likes" "bear" "-")
((((triple2) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The lion eats the lion.
True
5
proof
[(((((((triple2) -> rule1) triple1) -> rule2)) -> rule5))]
("lion" "eats" "lion" "+")
((((((triple2) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3
The lion does not eat the lion.
False
5
inv-proof
[(((((((triple2) -> rule1) triple1) -> rule2)) -> rule5))]
("lion" "eats" "lion" "-")
((((((triple2) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3
The rabbit does not eat the bear.
Unknown
inv-rconc
[@1: The rabbit eats the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "eats" "bear" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The bear does not eat the rabbit.
Unknown
inv-rconc
[@1: The bear eats the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "rabbit" "-")
The bear eats the lion.
Unknown
rconc
[@1: The bear eats the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "lion" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The lion chases the bear.
Unknown
random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "+")
@0: The bear likes the lion.[(triple1)] The lion likes the rabbit.[(triple2)] The rabbit is big.[(triple3)] @1: The rabbit likes the bear.[(((triple2) -> rule1))] @2: The lion likes the bear.[(((((triple2) -> rule1) triple1) -> rule2))] The rabbit eats the lion.[(((((triple2) -> rule1)) -> rule5))] @3: The lion eats the lion.[(((((((triple2) -> rule1) triple1) -> rule2)) -> rule5))]
The bear likes the lion.
("bear" "likes" "lion" "+")
triple1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
((triple2) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
((((((triple2) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3