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