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