The bear is big. The bear is cold. The bear is green. The bear is red. The bear likes the mouse. The bear needs the mouse. The bear sees the mouse. The mouse is cold. The mouse is red. The mouse likes the bear. The mouse needs the bear. The mouse sees the bear. If someone sees the bear then the bear is cold. If someone sees the bear then the bear needs the mouse. If someone needs the mouse then they are rough. If someone sees the mouse and they are rough then they need the mouse. If someone sees the bear then the bear needs the mouse. If the bear needs the mouse and the mouse sees the bear then the mouse likes the bear.
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is red.
("bear" "is" "red" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
If someone sees the bear then the bear is cold.
((("someone" "sees" "bear" "+")) -> ("bear" "is" "cold" "+"))
If someone sees the bear then the bear needs the mouse.
((("someone" "sees" "bear" "+")) -> ("bear" "needs" "mouse" "+"))
If someone needs the mouse then they are rough.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the mouse and they are rough then they need the mouse.
((("someone" "sees" "mouse" "+") ("someone" "is" "rough" "+")) -> ("someone" "needs" "mouse" "+"))
If someone sees the bear then the bear needs the mouse.
((("someone" "sees" "bear" "+")) -> ("bear" "needs" "mouse" "+"))
If the bear needs the mouse and the mouse sees the bear then the mouse likes the bear.
((("bear" "needs" "mouse" "+") ("mouse" "sees" "bear" "+")) -> ("mouse" "likes" "bear" "+"))
The mouse likes the bear.
True
1
proof
[(triple10 OR ((triple6 triple12) -> rule6) OR ((((triple12) -> rule2) triple12) -> rule6) OR ((((triple12) -> rule5) triple12) -> rule6))]
("mouse" "likes" "bear" "+")
triple10
((triple6 triple12) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
((((triple12) -> (rule2 % int2)) triple12) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
((((triple12) -> (rule5 % int2)) triple12) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The mouse does not like the bear.
False
1
inv-proof
[(triple10 OR ((triple6 triple12) -> rule6) OR ((((triple12) -> rule2) triple12) -> rule6) OR ((((triple12) -> rule5) triple12) -> rule6))]
("mouse" "likes" "bear" "-")
triple10
((triple6 triple12) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
((((triple12) -> (rule2 % int2)) triple12) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
((((triple12) -> (rule5 % int2)) triple12) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is big.[(triple1)] The bear is cold.[(triple2 OR ((triple12) -> rule1))] The bear is green.[(triple3)] The bear is red.[(triple4)] The bear likes the mouse.[(triple5)] The bear needs the mouse.[(triple6 OR ((triple12) -> rule2) OR ((triple12) -> rule5))] The bear sees the mouse.[(triple7)] The mouse is cold.[(triple8)] The mouse is red.[(triple9)] The mouse likes the bear.[(triple10 OR ((triple6 triple12) -> rule6) OR ((((triple12) -> rule2) triple12) -> rule6) OR ((((triple12) -> rule5) triple12) -> rule6))] The mouse needs the bear.[(triple11)] The mouse sees the bear.[(triple12)] @1: The bear is rough.[(((triple6) -> rule3) OR ((((triple12) -> rule2)) -> rule3) OR ((((triple12) -> rule5)) -> rule3))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
((triple12) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
triple3
The bear is red.
("bear" "is" "red" "+")
triple4
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple5
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple6
((triple12) -> (rule2 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
((triple12) -> (rule5 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse is red.
("mouse" "is" "red" "+")
triple9
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple10
((triple6 triple12) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
((((triple12) -> (rule2 % int2)) triple12) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
((((triple12) -> (rule5 % int2)) triple12) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple11
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple12
The bear is rough.
("bear" "is" "rough" "+")
((triple6) -> (rule3 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
((((triple12) -> (rule5 % int2))) -> (rule3 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2