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