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