The bear chases the mouse. The bear is cold. The bear needs the mouse. The mouse chases the bear. The mouse is cold. The mouse needs the bear. The mouse sees the bear. If someone is green and they need the mouse then they chase the mouse. If someone needs the mouse then they see the mouse.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
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 sees the bear.
("mouse" "sees" "bear" "+")
If someone is green and they need the mouse then they chase the mouse.
((("someone" "is" "green" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "chases" "mouse" "+"))
If someone needs the mouse then they see the mouse.
((("someone" "needs" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
The bear needs the mouse.
True
1
proof
[(triple3)]
("bear" "needs" "mouse" "+")
triple3
The bear is not cold.
False
1
inv-proof
[(triple2)]
("bear" "is" "cold" "-")
triple2
The bear sees the mouse.
True
2
proof
[(((triple3) -> rule2))]
("bear" "sees" "mouse" "+")
((triple3) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear does not see the mouse.
False
2
inv-proof
[(((triple3) -> rule2))]
("bear" "sees" "mouse" "-")
((triple3) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- 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 bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear chases the mouse.[(triple1)] The bear is cold.[(triple2)] The bear needs the mouse.[(triple3)] The mouse chases the bear.[(triple4)] The mouse is cold.[(triple5)] The mouse needs the bear.[(triple6)] The mouse sees the bear.[(triple7)] @1: The bear sees the mouse.[(((triple3) -> rule2))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple4
The mouse is cold.
("mouse" "is" "cold" "+")
triple5
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple6
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple7
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((triple3) -> (rule2 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1