The bear likes the mouse. The cow sees the mouse. The mouse likes the bear. If something sees the mouse and the mouse sees the cow then the mouse likes the bear. If something likes the mouse then it needs the bear.
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If something sees the mouse and the mouse sees the cow then the mouse likes the bear.
((("something" "sees" "mouse" "+") ("mouse" "sees" "cow" "+")) -> ("mouse" "likes" "bear" "+"))
If something likes the mouse then it needs the bear.
((("something" "likes" "mouse" "+")) -> ("something" "needs" "bear" "+"))
The bear likes the mouse.
True
1
proof
[(triple1)]
("bear" "likes" "mouse" "+")
triple1
The mouse does not like the bear.
False
1
inv-proof
[(triple3)]
("mouse" "likes" "bear" "-")
triple3
The bear needs the bear.
True
2
proof
[(((triple1) -> rule2))]
("bear" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "needs" "bear" "-")
((triple1) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The cow does not need the bear.
Unknown
inv-rconc
[@1: The cow needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "bear" "-")
The mouse needs the bear.
Unknown
rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "bear" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear likes the mouse.[(triple1)] The cow sees the mouse.[(triple2)] The mouse likes the bear.[(triple3)] @1: The bear needs the bear.[(((triple1) -> rule2))]
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple3
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1