The bear is cold. The cow sees the mouse. The mouse is not young. All nice people are not young. If someone sees the mouse then the mouse does not chase the cow. If someone chases the mouse then the mouse does not see the cow. If the cow is nice then the cow does not chase the mouse. If the cow sees the mouse and the mouse is young then the cow is not cold. If someone visits the mouse then the mouse is green.
The bear is cold.
("bear" "is" "cold" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse is not young.
("mouse" "is" "young" "-")
All nice people are not young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "-"))
If someone sees the mouse then the mouse does not chase the cow.
((("someone" "sees" "mouse" "+")) -> ("mouse" "chases" "cow" "-"))
If someone chases the mouse then the mouse does not see the cow.
((("someone" "chases" "mouse" "+")) -> ("mouse" "sees" "cow" "-"))
If the cow is nice then the cow does not chase the mouse.
((("cow" "is" "nice" "+")) -> ("cow" "chases" "mouse" "-"))
If the cow sees the mouse and the mouse is young then the cow is not cold.
((("cow" "sees" "mouse" "+") ("mouse" "is" "young" "+")) -> ("cow" "is" "cold" "-"))
If someone visits the mouse then the mouse is green.
((("someone" "visits" "mouse" "+")) -> ("mouse" "is" "green" "+"))
The cow sees the mouse.
True
1
proof
[(triple2)]
("cow" "sees" "mouse" "+")
triple2
The mouse is young.
False
1
inv-proof
[(triple3)]
("mouse" "is" "young" "+")
triple3
The mouse is not green.
Unknown
inv-rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "green" "-")
The cow visits the mouse.
Unknown
random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "+")
@0: The bear is cold.[(triple1)] The cow sees the mouse.[(triple2)] The mouse is not young.[(triple3)] @1: The mouse does not chase the cow.[(((triple2) -> rule2))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple2
The mouse is not young.
("mouse" "is" "young" "-")
triple3
The mouse does not chase the cow.
("mouse" "chases" "cow" "-")
((triple2) -> (rule2 % int1))
The mouse does not chase the cow.
("mouse" "chases" "cow" "-")
int1