The cow sees the rabbit. The cow does not visit the rabbit. The mouse is green. The mouse is kind. The mouse visits the cow. The mouse does not visit the rabbit. The rabbit visits the mouse. If the cow is blue then the cow is rough. If the cow is green then the cow does not see the mouse. If someone visits the cow and they are green then they see the mouse. If someone likes the mouse and they do not like the rabbit then they visit the rabbit. If someone sees the cow and they are not big then they visit the rabbit. If someone visits the rabbit and they do not visit the mouse then they do not like the cow. If someone visits the cow then the cow does not visit the rabbit. If someone likes the mouse and they do not visit the rabbit then they are rough.
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If the cow is blue then the cow is rough.
((("cow" "is" "blue" "+")) -> ("cow" "is" "rough" "+"))
If the cow is green then the cow does not see the mouse.
((("cow" "is" "green" "+")) -> ("cow" "sees" "mouse" "-"))
If someone visits the cow and they are green then they see the mouse.
((("someone" "visits" "cow" "+") ("someone" "is" "green" "+")) -> ("someone" "sees" "mouse" "+"))
If someone likes the mouse and they do not like the rabbit then they visit the rabbit.
((("someone" "likes" "mouse" "+") ("someone" "likes" "rabbit" "~")) -> ("someone" "visits" "rabbit" "+"))
If someone sees the cow and they are not big then they visit the rabbit.
((("someone" "sees" "cow" "+") ("someone" "is" "big" "~")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the rabbit and they do not visit the mouse then they do not like the cow.
((("someone" "visits" "rabbit" "+") ("someone" "visits" "mouse" "~")) -> ("someone" "likes" "cow" "-"))
If someone visits the cow then the cow does not visit the rabbit.
((("someone" "visits" "cow" "+")) -> ("cow" "visits" "rabbit" "-"))
If someone likes the mouse and they do not visit the rabbit then they are rough.
((("someone" "likes" "mouse" "+") ("someone" "visits" "rabbit" "~")) -> ("someone" "is" "rough" "+"))
The rabbit visits the mouse.
True
1
proof
[(triple7)]
("rabbit" "visits" "mouse" "+")
triple7
The mouse visits the rabbit.
False
1
inv-proof
[(triple6)]
("mouse" "visits" "rabbit" "+")
triple6
The rabbit does not see the mouse.
Unknown
inv-rconc
[@1: The rabbit sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "mouse" "-")
The mouse likes the cow.
Unknown
random
[@0: The mouse likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cow" "+")
@0: The cow does not visit the rabbit.[(triple2 OR ((triple5) -> rule7))] The cow sees the rabbit.[(triple1)] The mouse does not visit the rabbit.[(triple6)] The mouse is green.[(triple3)] The mouse is kind.[(triple4)] The mouse visits the cow.[(triple5)] The rabbit visits the mouse.[(triple7)] @1: The mouse sees the mouse.[(((triple5 triple3) -> rule3))]
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
triple2
((triple5) -> (rule7 % int1))
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple1
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple5
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple7
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple5 triple3) -> (rule3 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1