The bear does not need the mouse. The mouse visits the bear. If something visits the bear and it chases the bear then it visits the mouse. If something needs the bear and the bear needs the mouse then the bear is kind. If something needs the bear and it does not chase the bear then it is not green. If something chases the mouse and it does not need the mouse then the mouse is kind. If something visits the mouse and the mouse chases the bear then the bear chases the mouse. If something visits the mouse then the mouse does not visit the bear. If the mouse visits the bear then the mouse is not cold. All round things are cold.
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If something visits the bear and it chases the bear then it visits the mouse.
((("something" "visits" "bear" "+") ("something" "chases" "bear" "+")) -> ("something" "visits" "mouse" "+"))
If something needs the bear and the bear needs the mouse then the bear is kind.
((("something" "needs" "bear" "+") ("bear" "needs" "mouse" "+")) -> ("bear" "is" "kind" "+"))
If something needs the bear and it does not chase the bear then it is not green.
((("something" "needs" "bear" "+") ("something" "chases" "bear" "~")) -> ("something" "is" "green" "-"))
If something chases the mouse and it does not need the mouse then the mouse is kind.
((("something" "chases" "mouse" "+") ("something" "needs" "mouse" "~")) -> ("mouse" "is" "kind" "+"))
If something visits the mouse and the mouse chases the bear then the bear chases the mouse.
((("something" "visits" "mouse" "+") ("mouse" "chases" "bear" "+")) -> ("bear" "chases" "mouse" "+"))
If something visits the mouse then the mouse does not visit the bear.
((("something" "visits" "mouse" "+")) -> ("mouse" "visits" "bear" "-"))
If the mouse visits the bear then the mouse is not cold.
((("mouse" "visits" "bear" "+")) -> ("mouse" "is" "cold" "-"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
The bear does not need the mouse.
True
1
proof
[(triple1)]
("bear" "needs" "mouse" "-")
triple1
The bear needs the mouse.
False
1
inv-proof
[(triple1)]
("bear" "needs" "mouse" "+")
triple1
The mouse is not cold.
True
2
proof
[(((triple2) -> rule7))]
("mouse" "is" "cold" "-")
((triple2) -> (rule7 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
The mouse is cold.
False
2
inv-proof
[(((triple2) -> rule7))]
("mouse" "is" "cold" "+")
((triple2) -> (rule7 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
The bear does not visit the mouse.
Unknown
inv-rconc
[@1: The bear visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "mouse" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The bear does not need the mouse.[(triple1)] The mouse visits the bear.[(triple2)] @1: The mouse is not cold.[(((triple2) -> rule7))]
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
triple1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple2
The mouse is not cold.
("mouse" "is" "cold" "-")
((triple2) -> (rule7 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1