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