The bear is blue. The bear is round. The bear likes the mouse. The bear needs the cow. The bear needs the mouse. The bear visits the cow. The cow needs the mouse. The mouse is green. The mouse likes the cow. The mouse does not need the bear. The mouse needs the cow. The mouse visits the cow. If someone is blue then they do not need the bear.
The bear is blue.
("bear" "is" "blue" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If someone is blue then they do not need the bear.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "bear" "-"))
The bear needs the cow.
True
1
proof
[(triple4)]
("bear" "needs" "cow" "+")
triple4
The bear does not need the mouse.
False
1
inv-proof
[(triple5)]
("bear" "needs" "mouse" "-")
triple5
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 cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The bear is blue.[(triple1)] The bear is round.[(triple2)] The bear likes the mouse.[(triple3)] The bear needs the cow.[(triple4)] The bear needs the mouse.[(triple5)] The bear visits the cow.[(triple6)] The cow needs the mouse.[(triple7)] The mouse does not need the bear.[(triple10)] The mouse is green.[(triple8)] The mouse likes the cow.[(triple9)] The mouse needs the cow.[(triple11)] The mouse visits the cow.[(triple12)] @1: The bear does not need the bear.[(((triple1) -> rule1))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple3
The bear needs the cow.
("bear" "needs" "cow" "+")
triple4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple5
The bear visits the cow.
("bear" "visits" "cow" "+")
triple6
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple7
The mouse does not need the bear.
("mouse" "needs" "bear" "-")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple9
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple11
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple12
The bear does not need the bear.
("bear" "needs" "bear" "-")
((triple1) -> (rule1 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1