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