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