The bear is kind. The rabbit likes the bear. The squirrel likes the bear. If someone likes the bear and they like the squirrel then the squirrel needs the bear. If the rabbit needs the bear then the rabbit does not chase the squirrel. If the rabbit likes the squirrel and the rabbit is rough then the rabbit likes the bear.
The bear is kind.
("bear" "is" "kind" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
If someone likes the bear and they like the squirrel then the squirrel needs the bear.
((("someone" "likes" "bear" "+") ("someone" "likes" "squirrel" "+")) -> ("squirrel" "needs" "bear" "+"))
If the rabbit needs the bear then the rabbit does not chase the squirrel.
((("rabbit" "needs" "bear" "+")) -> ("rabbit" "chases" "squirrel" "-"))
If the rabbit likes the squirrel and the rabbit is rough then the rabbit likes the bear.
((("rabbit" "likes" "squirrel" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "likes" "bear" "+"))
The squirrel likes the bear.
True
1
proof
[(triple3)]
("squirrel" "likes" "bear" "+")
triple3
The squirrel does not like the bear.
False
1
inv-proof
[(triple3)]
("squirrel" "likes" "bear" "-")
triple3
The squirrel does not need the bear.
Unknown
inv-rconc
[@1: The squirrel needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "bear" "-")
The squirrel chases the bear.
Unknown
random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "+")
@0: The bear is kind.[(triple1)] The rabbit likes the bear.[(triple2)] The squirrel likes the bear.[(triple3)]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple3