The cow is big. The lion likes the rabbit. The rabbit likes the cow. If the cow chases the lion then the cow is not green. If the cow visits the lion then the cow is not green. If someone likes the rabbit then they are round. If someone chases the rabbit and the rabbit does not chase the cow then the rabbit visits the lion. If someone likes the cow and they do not chase the rabbit then the cow does not chase the lion. If someone visits the lion then the lion visits the cow. If someone is round then they do not visit the rabbit. If someone likes the rabbit and the rabbit is not round then the rabbit chases the lion.
The cow is big.
("cow" "is" "big" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
If the cow chases the lion then the cow is not green.
((("cow" "chases" "lion" "+")) -> ("cow" "is" "green" "-"))
If the cow visits the lion then the cow is not green.
((("cow" "visits" "lion" "+")) -> ("cow" "is" "green" "-"))
If someone likes the rabbit then they are round.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "round" "+"))
If someone chases the rabbit and the rabbit does not chase the cow then the rabbit visits the lion.
((("someone" "chases" "rabbit" "+") ("rabbit" "chases" "cow" "~")) -> ("rabbit" "visits" "lion" "+"))
If someone likes the cow and they do not chase the rabbit then the cow does not chase the lion.
((("someone" "likes" "cow" "+") ("someone" "chases" "rabbit" "~")) -> ("cow" "chases" "lion" "-"))
If someone visits the lion then the lion visits the cow.
((("someone" "visits" "lion" "+")) -> ("lion" "visits" "cow" "+"))
If someone is round then they do not visit the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "visits" "rabbit" "-"))
If someone likes the rabbit and the rabbit is not round then the rabbit chases the lion.
((("someone" "likes" "rabbit" "+") ("rabbit" "is" "round" "~")) -> ("rabbit" "chases" "lion" "+"))
The rabbit likes the cow.
True
1
proof
[(triple3)]
("rabbit" "likes" "cow" "+")
triple3
The rabbit does not like the cow.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "cow" "-")
triple3
The lion is round.
True
2
proof
[(((triple2) -> rule3))]
("lion" "is" "round" "+")
((triple2) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("lion" "is" "round" "-")
((triple2) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion does not visit the rabbit.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("lion" "visits" "rabbit" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion visits the rabbit.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("lion" "visits" "rabbit" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The rabbit does not visit the lion.
Unknown
inv-rconc
[@1: The rabbit visits the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "visits" "lion" "-")
The lion visits the cow.
Unknown
rconc
[@2: The lion visits the cow.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("lion" "visits" "cow" "+")
The rabbit is not round.
Unknown
inv-rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "round" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The cow is big.[(triple1)] The lion likes the rabbit.[(triple2)] The rabbit likes the cow.[(triple3)] @1: The lion is round.[(((triple2) -> rule3))] @2: The lion does not visit the rabbit.[(((((triple2) -> rule3)) -> rule7))]
The cow is big.
("cow" "is" "big" "+")
triple1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple2
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
((triple2) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
int1
The lion is round.
("lion" "is" "round" "+")
int2