The bear chases the mouse. The dog is cold. The mouse visits the bear. If the mouse visits the dog then the mouse likes the bear. If someone visits the mouse then the mouse visits the bear. If the dog chases the bear and the dog likes the mouse then the bear is cold. If someone likes the mouse and the mouse is kind then they visit the mouse. If the mouse chases the bear then the bear visits the dog. If someone visits the dog then the dog visits the bear. If the dog likes the mouse and the dog chases the bear then the mouse visits the bear. If someone visits the bear then the bear is kind.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The dog is cold.
("dog" "is" "cold" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If the mouse visits the dog then the mouse likes the bear.
((("mouse" "visits" "dog" "+")) -> ("mouse" "likes" "bear" "+"))
If someone visits the mouse then the mouse visits the bear.
((("someone" "visits" "mouse" "+")) -> ("mouse" "visits" "bear" "+"))
If the dog chases the bear and the dog likes the mouse then the bear is cold.
((("dog" "chases" "bear" "+") ("dog" "likes" "mouse" "+")) -> ("bear" "is" "cold" "+"))
If someone likes the mouse and the mouse is kind then they visit the mouse.
((("someone" "likes" "mouse" "+") ("mouse" "is" "kind" "+")) -> ("someone" "visits" "mouse" "+"))
If the mouse chases the bear then the bear visits the dog.
((("mouse" "chases" "bear" "+")) -> ("bear" "visits" "dog" "+"))
If someone visits the dog then the dog visits the bear.
((("someone" "visits" "dog" "+")) -> ("dog" "visits" "bear" "+"))
If the dog likes the mouse and the dog chases the bear then the mouse visits the bear.
((("dog" "likes" "mouse" "+") ("dog" "chases" "bear" "+")) -> ("mouse" "visits" "bear" "+"))
If someone visits the bear then the bear is kind.
((("someone" "visits" "bear" "+")) -> ("bear" "is" "kind" "+"))
The bear chases the mouse.
True
1
proof
[(triple1)]
("bear" "chases" "mouse" "+")
triple1
The mouse does not visit the bear.
False
1
inv-proof
[(triple3)]
("mouse" "visits" "bear" "-")
triple3
The bear is kind.
True
2
proof
[(((triple3) -> rule8))]
("bear" "is" "kind" "+")
((triple3) -> (rule8 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is not kind.
False
2
inv-proof
[(((triple3) -> rule8))]
("bear" "is" "kind" "-")
((triple3) -> (rule8 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The mouse does not like the bear.
Unknown
inv-rconc
[@1: The mouse likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "bear" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The dog likes the bear.
Unknown
random
[@0: The dog likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "bear" "+")
@0: The bear chases the mouse.[(triple1)] The dog is cold.[(triple2)] The mouse visits the bear.[(triple3)] @1: The bear is kind.[(((triple3) -> rule8))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple3
The bear is kind.
("bear" "is" "kind" "+")
((triple3) -> (rule8 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1