The cow chases the lion. The lion visits the rabbit. The rabbit is blue. The squirrel is young. If someone visits the lion then they eat the cow. If someone eats the lion then they do not chase the squirrel. If someone visits the lion and they do not eat the rabbit then the rabbit is not blue. If someone visits the lion then the lion is young. If someone visits the lion and the lion visits the rabbit then they visit the squirrel. If someone chases the lion then they visit the cow. If someone is blue then they do not visit the rabbit. If someone is green and not young then they do not chase the rabbit.
The cow chases the lion.
("cow" "chases" "lion" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If someone visits the lion then they eat the cow.
((("someone" "visits" "lion" "+")) -> ("someone" "eats" "cow" "+"))
If someone eats the lion then they do not chase the squirrel.
((("someone" "eats" "lion" "+")) -> ("someone" "chases" "squirrel" "-"))
If someone visits the lion and they do not eat the rabbit then the rabbit is not blue.
((("someone" "visits" "lion" "+") ("someone" "eats" "rabbit" "~")) -> ("rabbit" "is" "blue" "-"))
If someone visits the lion then the lion is young.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "young" "+"))
If someone visits the lion and the lion visits the rabbit then they visit the squirrel.
((("someone" "visits" "lion" "+") ("lion" "visits" "rabbit" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone chases the lion then they visit the cow.
((("someone" "chases" "lion" "+")) -> ("someone" "visits" "cow" "+"))
If someone is blue then they do not visit the rabbit.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "rabbit" "-"))
If someone is green and not young then they do not chase the rabbit.
((("someone" "is" "green" "+") ("someone" "is" "young" "~")) -> ("someone" "chases" "rabbit" "-"))
The squirrel is young.
True
1
proof
[(triple4)]
("squirrel" "is" "young" "+")
triple4
The cow does not chase the lion.
False
1
inv-proof
[(triple1)]
("cow" "chases" "lion" "-")
triple1
The rabbit does not visit the rabbit.
True
2
proof
[(((triple3) -> rule7))]
("rabbit" "visits" "rabbit" "-")
((triple3) -> (rule7 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The rabbit visits the rabbit.
False
2
inv-proof
[(((triple3) -> rule7))]
("rabbit" "visits" "rabbit" "+")
((triple3) -> (rule7 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "cow" "-")
The rabbit visits the squirrel.
Unknown
rconc
[@1: The rabbit visits the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "visits" "squirrel" "+")
The rabbit does not chase the cow.
Unknown
inv-random
[@0: The rabbit chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cow" "-")
The cow visits the lion.
Unknown
random
[@0: The cow visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "lion" "+")
@0: The cow chases the lion.[(triple1)] The lion visits the rabbit.[(triple2)] The rabbit is blue.[(triple3)] The squirrel is young.[(triple4)] @1: The cow visits the cow.[(((triple1) -> rule6))] The rabbit does not visit the rabbit.[(((triple3) -> rule7))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
triple4
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
((triple3) -> (rule7 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1