The bear visits the mouse. The cow is blue. The mouse does not visit the cow. If something is blue then it visits the bear. If something visits the mouse then it is nice. If something chases the bear then the bear is red. If the cow needs the mouse and the mouse is nice then the mouse visits the bear. If something visits the cow and the cow chases the bear then the bear is not nice. If something is red and it chases the cow then the cow does not visit the bear.
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cow is blue.
("cow" "is" "blue" "+")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
If something is blue then it visits the bear.
((("something" "is" "blue" "+")) -> ("something" "visits" "bear" "+"))
If something visits the mouse then it is nice.
((("something" "visits" "mouse" "+")) -> ("something" "is" "nice" "+"))
If something chases the bear then the bear is red.
((("something" "chases" "bear" "+")) -> ("bear" "is" "red" "+"))
If the cow needs the mouse and the mouse is nice then the mouse visits the bear.
((("cow" "needs" "mouse" "+") ("mouse" "is" "nice" "+")) -> ("mouse" "visits" "bear" "+"))
If something visits the cow and the cow chases the bear then the bear is not nice.
((("something" "visits" "cow" "+") ("cow" "chases" "bear" "+")) -> ("bear" "is" "nice" "-"))
If something is red and it chases the cow then the cow does not visit the bear.
((("something" "is" "red" "+") ("something" "chases" "cow" "+")) -> ("cow" "visits" "bear" "-"))
The mouse does not visit the cow.
True
1
proof
[(triple3)]
("mouse" "visits" "cow" "-")
triple3
The mouse visits the cow.
False
1
inv-proof
[(triple3)]
("mouse" "visits" "cow" "+")
triple3
The bear is nice.
True
2
proof
[(((triple1) -> rule2))]
("bear" "is" "nice" "+")
((triple1) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The cow does not visit the bear.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "visits" "bear" "-")
((triple2) -> (rule1 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The bear is not red.
Unknown
inv-rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "red" "-")
The bear visits the bear.
Unknown
rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "bear" "+")
The mouse does not need the bear.
Unknown
inv-random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
@0: The bear visits the mouse.[(triple1)] The cow is blue.[(triple2)] The mouse does not visit the cow.[(triple3)] @1: The bear is nice.[(((triple1) -> rule2))] The cow visits the bear.[(((triple2) -> rule1))]
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple3
The bear is nice.
("bear" "is" "nice" "+")
((triple1) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
((triple2) -> (rule1 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1