The bear likes the mouse. The bear does not visit the mouse. The mouse does not like the bear. The rabbit chases the mouse. The rabbit likes the bear. The rabbit likes the mouse. The rabbit visits the mouse. If someone is kind then they visit the rabbit. If someone visits the mouse then they are rough. If someone likes the mouse and the mouse visits the bear then the bear does not chase the mouse. If someone is cold then they chase the bear. If someone visits the rabbit then the rabbit does not chase the mouse. If someone likes the rabbit and they do not chase the bear then the bear visits the rabbit.
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone is kind then they visit the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the mouse then they are rough.
((("someone" "visits" "mouse" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the mouse and the mouse visits the bear then the bear does not chase the mouse.
((("someone" "likes" "mouse" "+") ("mouse" "visits" "bear" "+")) -> ("bear" "chases" "mouse" "-"))
If someone is cold then they chase the bear.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "bear" "+"))
If someone visits the rabbit then the rabbit does not chase the mouse.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "-"))
If someone likes the rabbit and they do not chase the bear then the bear visits the rabbit.
((("someone" "likes" "rabbit" "+") ("someone" "chases" "bear" "~")) -> ("bear" "visits" "rabbit" "+"))
The rabbit likes the mouse.
True
1
proof
[(triple6)]
("rabbit" "likes" "mouse" "+")
triple6
The rabbit does not like the bear.
False
1
inv-proof
[(triple5)]
("rabbit" "likes" "bear" "-")
triple5
The rabbit is rough.
True
2
proof
[(((triple7) -> rule2))]
("rabbit" "is" "rough" "+")
((triple7) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is not rough.
False
2
inv-proof
[(((triple7) -> rule2))]
("rabbit" "is" "rough" "-")
((triple7) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The mouse visits the rabbit.
Unknown
rconc
[@1: The mouse visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "rabbit" "+")
The bear does not chase the mouse.
Unknown
inv-random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The bear does not visit the mouse.[(triple2)] The bear likes the mouse.[(triple1)] The mouse does not like the bear.[(triple3)] The rabbit chases the mouse.[(triple4)] The rabbit likes the bear.[(triple5)] The rabbit likes the mouse.[(triple6)] The rabbit visits the mouse.[(triple7)] @1: The rabbit is rough.[(((triple7) -> rule2))]
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
triple2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple1
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
triple3
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple4
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple5
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple6
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple7) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1