The bear is cold. The bear is not green. The bear is kind. The bear is rough. The bear is young. The bear needs the mouse. The bear sees the mouse. The bear visits the mouse. The mouse is cold. The mouse is green. The mouse is kind. The mouse is not rough. The mouse is young. The mouse needs the bear. The mouse sees the bear. The mouse does not visit the bear. If someone sees the bear and they need the mouse then the mouse sees the bear. If someone is cold and rough then they visit the bear. If someone needs the mouse and the mouse visits the bear then the bear sees the mouse.
The bear is cold.
("bear" "is" "cold" "+")
The bear is not green.
("bear" "is" "green" "-")
The bear is kind.
("bear" "is" "kind" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
If someone sees the bear and they need the mouse then the mouse sees the bear.
((("someone" "sees" "bear" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "bear" "+"))
If someone is cold and rough then they visit the bear.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "visits" "bear" "+"))
If someone needs the mouse and the mouse visits the bear then the bear sees the mouse.
((("someone" "needs" "mouse" "+") ("mouse" "visits" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
The bear is young.
True
1
proof
[(triple5)]
("bear" "is" "young" "+")
triple5
The mouse does not need the bear.
False
1
inv-proof
[(triple14)]
("mouse" "needs" "bear" "-")
triple14
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
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 cold.[(triple1)] The bear is kind.[(triple3)] The bear is not green.[(triple2)] The bear is rough.[(triple4)] The bear is young.[(triple5)] The bear needs the mouse.[(triple6)] The bear sees the mouse.[(triple7)] The bear visits the mouse.[(triple8)] The mouse does not visit the bear.[(triple16)] The mouse is cold.[(triple9)] The mouse is green.[(triple10)] The mouse is kind.[(triple11)] The mouse is not rough.[(triple12)] The mouse is young.[(triple13)] The mouse needs the bear.[(triple14)] The mouse sees the bear.[(triple15)] @1: The bear visits the bear.[(((triple1 triple4) -> rule2))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple3
The bear is not green.
("bear" "is" "green" "-")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple4
The bear is young.
("bear" "is" "young" "+")
triple5
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple6
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple7
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple8
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
triple16
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse is green.
("mouse" "is" "green" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse is not rough.
("mouse" "is" "rough" "-")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple13
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple14
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple15
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1 triple4) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1