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