The bear needs the rabbit. The rabbit likes the bear. If someone needs the bear and they visit the rabbit then the rabbit needs the bear. If someone likes the bear and the bear needs the rabbit then they do not visit the bear. If someone is big and they like the rabbit then the rabbit is kind. If someone is big then they do not need the rabbit. If the rabbit needs the bear then the bear needs the rabbit. If someone visits the bear and the bear is not nice then they are not round.
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
If someone needs the bear and they visit the rabbit then the rabbit needs the bear.
((("someone" "needs" "bear" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "needs" "bear" "+"))
If someone likes the bear and the bear needs the rabbit then they do not visit the bear.
((("someone" "likes" "bear" "+") ("bear" "needs" "rabbit" "+")) -> ("someone" "visits" "bear" "-"))
If someone is big and they like the rabbit then the rabbit is kind.
((("someone" "is" "big" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
If someone is big then they do not need the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "needs" "rabbit" "-"))
If the rabbit needs the bear then the bear needs the rabbit.
((("rabbit" "needs" "bear" "+")) -> ("bear" "needs" "rabbit" "+"))
If someone visits the bear and the bear is not nice then they are not round.
((("someone" "visits" "bear" "+") ("bear" "is" "nice" "~")) -> ("someone" "is" "round" "-"))
The rabbit likes the bear.
True
1
proof
[(triple2)]
("rabbit" "likes" "bear" "+")
triple2
The bear does not need the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "needs" "rabbit" "-")
triple1
The rabbit does not visit the bear.
True
3
proof
[(((triple2 triple1) -> rule2))]
("rabbit" "visits" "bear" "-")
((triple2 triple1) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The rabbit visits the bear.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("rabbit" "visits" "bear" "+")
((triple2 triple1) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The rabbit does not need the bear.
Unknown
inv-rconc
[@1: The rabbit needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "bear" "-")
The rabbit is kind.
Unknown
rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "kind" "+")
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 bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear needs the rabbit.[(triple1)] The rabbit likes the bear.[(triple2)] @1: The rabbit does not visit the bear.[(((triple2 triple1) -> rule2))]
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple2
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
((triple2 triple1) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1