The dog likes the rabbit. The lion is kind. The rabbit sees the lion. If someone is red and big then they see the dog. If the rabbit is rough then the rabbit does not like the lion. If the dog eats the rabbit then the rabbit sees the dog. If someone is big and they do not eat the rabbit then the rabbit eats the dog. If someone likes the rabbit then the rabbit is rough. If someone sees the lion and they are rough then the lion does not eat the dog. If someone is rough and they eat the lion then the lion is kind. If the dog is big and the dog sees the rabbit then the rabbit does not like the dog.
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The lion is kind.
("lion" "is" "kind" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone is red and big then they see the dog.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "sees" "dog" "+"))
If the rabbit is rough then the rabbit does not like the lion.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "likes" "lion" "-"))
If the dog eats the rabbit then the rabbit sees the dog.
((("dog" "eats" "rabbit" "+")) -> ("rabbit" "sees" "dog" "+"))
If someone is big and they do not eat the rabbit then the rabbit eats the dog.
((("someone" "is" "big" "+") ("someone" "eats" "rabbit" "~")) -> ("rabbit" "eats" "dog" "+"))
If someone likes the rabbit then the rabbit is rough.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If someone sees the lion and they are rough then the lion does not eat the dog.
((("someone" "sees" "lion" "+") ("someone" "is" "rough" "+")) -> ("lion" "eats" "dog" "-"))
If someone is rough and they eat the lion then the lion is kind.
((("someone" "is" "rough" "+") ("someone" "eats" "lion" "+")) -> ("lion" "is" "kind" "+"))
If the dog is big and the dog sees the rabbit then the rabbit does not like the dog.
((("dog" "is" "big" "+") ("dog" "sees" "rabbit" "+")) -> ("rabbit" "likes" "dog" "-"))
The dog likes the rabbit.
True
1
proof
[(triple1)]
("dog" "likes" "rabbit" "+")
triple1
The rabbit does not see the lion.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "lion" "-")
triple3
The rabbit is rough.
True
2
proof
[(((triple1) -> rule5))]
("rabbit" "is" "rough" "+")
((triple1) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is not rough.
False
2
inv-proof
[(((triple1) -> rule5))]
("rabbit" "is" "rough" "-")
((triple1) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit does not like the lion.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("rabbit" "likes" "lion" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit likes the lion.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("rabbit" "likes" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit does not eat the dog.
Unknown
inv-rconc
[@1: The rabbit eats the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "eats" "dog" "-")
The lion sees the dog.
Unknown
rconc
[@1: The lion sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "dog" "+")
The rabbit does not see the dog.
Unknown
inv-rconc
[@1: The rabbit sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "dog" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The dog likes the rabbit.[(triple1)] The lion is kind.[(triple2)] The rabbit sees the lion.[(triple3)] @1: The rabbit is rough.[(((triple1) -> rule5))] @2: The lion does not eat the dog.[(((triple3 ((triple1) -> rule5)) -> rule6))] The rabbit does not like the lion.[(((((triple1) -> rule5)) -> rule2))]
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple3
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple1) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The lion does not eat the dog.
("lion" "eats" "dog" "-")
((triple3 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The lion does not eat the dog.
("lion" "eats" "dog" "-")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2