The bear chases the mouse. The bear is big. The bear is blue. The bear is green. The bear is young. The bear needs the mouse. The bear visits the mouse. The mouse chases the bear. The mouse is blue. The mouse is green. The mouse is young. The mouse visits the bear. If the mouse is green and the mouse visits the bear then the mouse needs the bear. If someone needs the bear then the bear needs the mouse. If the mouse chases the bear and the bear is big then the mouse visits the bear.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If the mouse is green and the mouse visits the bear then the mouse needs the bear.
((("mouse" "is" "green" "+") ("mouse" "visits" "bear" "+")) -> ("mouse" "needs" "bear" "+"))
If someone needs the bear then the bear needs the mouse.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "mouse" "+"))
If the mouse chases the bear and the bear is big then the mouse visits the bear.
((("mouse" "chases" "bear" "+") ("bear" "is" "big" "+")) -> ("mouse" "visits" "bear" "+"))
The mouse is young.
True
1
proof
[(triple11)]
("mouse" "is" "young" "+")
triple11
The bear does not visit the mouse.
False
1
inv-proof
[(triple7)]
("bear" "visits" "mouse" "-")
triple7
The mouse needs the bear.
True
3
proof
[(((triple10 triple12) -> rule1) OR ((triple10 ((triple8 triple2) -> rule3)) -> rule1))]
("mouse" "needs" "bear" "+")
((triple10 triple12) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
((triple10 ((triple8 triple2) -> (rule3 % int2))) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The mouse does not need the bear.
False
3
inv-proof
[(((triple10 triple12) -> rule1) OR ((triple10 ((triple8 triple2) -> rule3)) -> rule1))]
("mouse" "needs" "bear" "-")
((triple10 triple12) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
((triple10 ((triple8 triple2) -> (rule3 % int2))) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The bear chases the mouse.[(triple1)] The bear is big.[(triple2)] The bear is blue.[(triple3)] The bear is green.[(triple4)] The bear is young.[(triple5)] The bear needs the mouse.[(triple6 OR ((((triple10 triple12) -> rule1)) -> rule2) OR ((((triple10 ((triple8 triple2) -> rule3)) -> rule1)) -> rule2))] The bear visits the mouse.[(triple7)] The mouse chases the bear.[(triple8)] The mouse is blue.[(triple9)] The mouse is green.[(triple10)] The mouse is young.[(triple11)] The mouse visits the bear.[(triple12 OR ((triple8 triple2) -> rule3))] @1: The mouse needs the bear.[(((triple10 triple12) -> rule1) OR ((triple10 ((triple8 triple2) -> rule3)) -> rule1))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple4
The bear is young.
("bear" "is" "young" "+")
triple5
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple6
((((triple10 triple12) -> (rule1 % int2))) -> (rule2 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
((((triple10 ((triple8 triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple7
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse is green.
("mouse" "is" "green" "+")
triple10
The mouse is young.
("mouse" "is" "young" "+")
triple11
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple12
((triple8 triple2) -> (rule3 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple10 triple12) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
((triple10 ((triple8 triple2) -> (rule3 % int2))) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2