The bear is young. The bear likes the rabbit. The bear needs the mouse. The mouse eats the rabbit. The mouse is kind. The mouse is young. The rabbit is big. The rabbit is red. The rabbit is young. The rabbit likes the mouse. If something is young and kind then it needs the bear. If the mouse needs the bear then the bear is young. If something needs the rabbit and it likes the bear then it needs the mouse. If something eats the bear then the bear likes the mouse. If something likes the bear then the bear needs the rabbit. If something is red and kind then it needs the rabbit.
The bear is young.
("bear" "is" "young" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
If something is young and kind then it needs the bear.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "needs" "bear" "+"))
If the mouse needs the bear then the bear is young.
((("mouse" "needs" "bear" "+")) -> ("bear" "is" "young" "+"))
If something needs the rabbit and it likes the bear then it needs the mouse.
((("something" "needs" "rabbit" "+") ("something" "likes" "bear" "+")) -> ("something" "needs" "mouse" "+"))
If something eats the bear then the bear likes the mouse.
((("something" "eats" "bear" "+")) -> ("bear" "likes" "mouse" "+"))
If something likes the bear then the bear needs the rabbit.
((("something" "likes" "bear" "+")) -> ("bear" "needs" "rabbit" "+"))
If something is red and kind then it needs the rabbit.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "needs" "rabbit" "+"))
The bear likes the rabbit.
True
1
proof
[(triple2)]
("bear" "likes" "rabbit" "+")
triple2
The bear does not need the mouse.
False
1
inv-proof
[(triple3)]
("bear" "needs" "mouse" "-")
triple3
The mouse needs the bear.
True
3
proof
[(((triple6 triple5) -> rule1))]
("mouse" "needs" "bear" "+")
((triple6 triple5) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse does not need the bear.
False
3
inv-proof
[(((triple6 triple5) -> rule1))]
("mouse" "needs" "bear" "-")
((triple6 triple5) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "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 mouse needs the rabbit.
Unknown
rconc
[@1: The mouse needs the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "needs" "rabbit" "+")
The rabbit does not like the bear.
Unknown
inv-random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear is young.[(triple1 OR ((((triple6 triple5) -> rule1)) -> rule2))] The bear likes the rabbit.[(triple2)] The bear needs the mouse.[(triple3)] The mouse eats the rabbit.[(triple4)] The mouse is kind.[(triple5)] The mouse is young.[(triple6)] The rabbit is big.[(triple7)] The rabbit is red.[(triple8)] The rabbit is young.[(triple9)] The rabbit likes the mouse.[(triple10)] @1: The mouse needs the bear.[(((triple6 triple5) -> rule1))]
The bear is young.
("bear" "is" "young" "+")
triple1
((((triple6 triple5) -> (rule1 % int2))) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The rabbit is big.
("rabbit" "is" "big" "+")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple8
The rabbit is young.
("rabbit" "is" "young" "+")
triple9
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple10
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple6 triple5) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1