The cow chases the rabbit. The lion is cold. The rabbit chases the cow. All round people are big. If someone likes the rabbit then they are cold. If someone chases the cow then the cow chases the lion. If the lion chases the rabbit and the lion sees the cow then the rabbit chases the lion. If someone is big and they see the rabbit then they like the rabbit. If someone likes the cow then the cow sees the lion. If someone likes the lion then the lion is red. If the rabbit is green then the rabbit chases the cow.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone likes the rabbit then they are cold.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "cold" "+"))
If someone chases the cow then the cow chases the lion.
((("someone" "chases" "cow" "+")) -> ("cow" "chases" "lion" "+"))
If the lion chases the rabbit and the lion sees the cow then the rabbit chases the lion.
((("lion" "chases" "rabbit" "+") ("lion" "sees" "cow" "+")) -> ("rabbit" "chases" "lion" "+"))
If someone is big and they see the rabbit then they like the rabbit.
((("someone" "is" "big" "+") ("someone" "sees" "rabbit" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone likes the cow then the cow sees the lion.
((("someone" "likes" "cow" "+")) -> ("cow" "sees" "lion" "+"))
If someone likes the lion then the lion is red.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "red" "+"))
If the rabbit is green then the rabbit chases the cow.
((("rabbit" "is" "green" "+")) -> ("rabbit" "chases" "cow" "+"))
The rabbit chases the cow.
True
1
proof
[(triple3)]
("rabbit" "chases" "cow" "+")
triple3
The cow does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("cow" "chases" "rabbit" "-")
triple1
The cow chases the lion.
True
2
proof
[(((triple3) -> rule3))]
("cow" "chases" "lion" "+")
((triple3) -> (rule3 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow does not chase the lion.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "chases" "lion" "-")
((triple3) -> (rule3 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The rabbit is not cold.
Unknown
inv-rconc
[@2: The rabbit is cold.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit does not see the cow.
Unknown
inv-random
[@0: The rabbit sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cow" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The cow chases the rabbit.[(triple1)] The lion is cold.[(triple2)] The rabbit chases the cow.[(triple3)] @1: The cow chases the lion.[(((triple3) -> rule3))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple3
The cow chases the lion.
("cow" "chases" "lion" "+")
((triple3) -> (rule3 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1