The bear is red. The lion eats the bear. The rabbit chases the bear. If someone chases the bear then they are blue. If someone likes the lion and they like the bear then they are young. If someone chases the rabbit then the rabbit chases the lion. If someone eats the lion then they eat the bear. If the bear eats the lion then the lion chases the bear. If someone likes the rabbit and they chase the rabbit then the rabbit eats the bear.
The bear is red.
("bear" "is" "red" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
If someone chases the bear then they are blue.
((("someone" "chases" "bear" "+")) -> ("someone" "is" "blue" "+"))
If someone likes the lion and they like the bear then they are young.
((("someone" "likes" "lion" "+") ("someone" "likes" "bear" "+")) -> ("someone" "is" "young" "+"))
If someone chases the rabbit then the rabbit chases the lion.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "lion" "+"))
If someone eats the lion then they eat the bear.
((("someone" "eats" "lion" "+")) -> ("someone" "eats" "bear" "+"))
If the bear eats the lion then the lion chases the bear.
((("bear" "eats" "lion" "+")) -> ("lion" "chases" "bear" "+"))
If someone likes the rabbit and they chase the rabbit then the rabbit eats the bear.
((("someone" "likes" "rabbit" "+") ("someone" "chases" "rabbit" "+")) -> ("rabbit" "eats" "bear" "+"))
The rabbit chases the bear.
True
1
proof
[(triple3)]
("rabbit" "chases" "bear" "+")
triple3
The bear is not red.
False
1
inv-proof
[(triple1)]
("bear" "is" "red" "-")
triple1
The rabbit is blue.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "is" "blue" "-")
((triple3) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The lion is not blue.
Unknown
inv-rconc
[@2: The lion is blue.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("lion" "is" "blue" "-")
The lion chases the bear.
Unknown
rconc
[@1: The lion chases the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "chases" "bear" "+")
The lion does not chase the rabbit.
Unknown
inv-random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The bear is red.[(triple1)] The lion eats the bear.[(triple2)] The rabbit chases the bear.[(triple3)] @1: The rabbit is blue.[(((triple3) -> rule1))]
The bear is red.
("bear" "is" "red" "+")
triple1
The lion eats the bear.
("lion" "eats" "bear" "+")
triple2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1