The bear does not like the lion. The bear needs the mouse. The bear sees the cow. The cow needs the bear. The cow sees the bear. The lion does not need the bear. The lion does not see the mouse. The mouse is rough. The mouse is not young. The mouse sees the cow. If someone sees the cow and they need the cow then they like the mouse. If someone is blue then they are cold. If the cow needs the bear then the bear needs the lion.
The bear does not like the lion.
("bear" "likes" "lion" "-")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The lion does not need the bear.
("lion" "needs" "bear" "-")
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If someone sees the cow and they need the cow then they like the mouse.
((("someone" "sees" "cow" "+") ("someone" "needs" "cow" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is blue then they are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If the cow needs the bear then the bear needs the lion.
((("cow" "needs" "bear" "+")) -> ("bear" "needs" "lion" "+"))
The mouse is rough.
True
1
proof
[(triple8)]
("mouse" "is" "rough" "+")
triple8
The mouse is young.
False
1
inv-proof
[(triple9)]
("mouse" "is" "young" "+")
triple9
The bear needs the lion.
True
2
proof
[(((triple4) -> rule3))]
("bear" "needs" "lion" "+")
((triple4) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear does not need the lion.
False
2
inv-proof
[(((triple4) -> rule3))]
("bear" "needs" "lion" "-")
((triple4) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "cold" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The lion does not see the cow.
Unknown
inv-random
[@0: The lion sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cow" "-")
The bear needs the cow.
Unknown
random
[@0: The bear needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cow" "+")
@0: The bear does not like the lion.[(triple1)] The bear needs the mouse.[(triple2)] The bear sees the cow.[(triple3)] The cow needs the bear.[(triple4)] The cow sees the bear.[(triple5)] The lion does not need the bear.[(triple6)] The lion does not see the mouse.[(triple7)] The mouse is not young.[(triple9)] The mouse is rough.[(triple8)] The mouse sees the cow.[(triple10)] @1: The bear needs the lion.[(((triple4) -> rule3))]
The bear does not like the lion.
("bear" "likes" "lion" "-")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The bear sees the cow.
("bear" "sees" "cow" "+")
triple3
The cow needs the bear.
("cow" "needs" "bear" "+")
triple4
The cow sees the bear.
("cow" "sees" "bear" "+")
triple5
The lion does not need the bear.
("lion" "needs" "bear" "-")
triple6
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
triple7
The mouse is not young.
("mouse" "is" "young" "-")
triple9
The mouse is rough.
("mouse" "is" "rough" "+")
triple8
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple10
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple4) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1