The mouse is cold. The mouse is red. The rabbit chases the mouse. The rabbit is blue. The rabbit is red. The rabbit likes the mouse. The rabbit sees the mouse. If something likes the mouse and the mouse chases the rabbit then the rabbit chases the mouse. If something likes the mouse then it is kind.
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something likes the mouse and the mouse chases the rabbit then the rabbit chases the mouse.
((("something" "likes" "mouse" "+") ("mouse" "chases" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "+"))
If something likes the mouse then it is kind.
((("something" "likes" "mouse" "+")) -> ("something" "is" "kind" "+"))
The mouse is cold.
True
1
proof
[(triple1)]
("mouse" "is" "cold" "+")
triple1
The rabbit does not chase the mouse.
False
1
inv-proof
[(triple3)]
("rabbit" "chases" "mouse" "-")
triple3
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "kind" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The mouse is cold.[(triple1)] The mouse is red.[(triple2)] The rabbit chases the mouse.[(triple3)] The rabbit is blue.[(triple4)] The rabbit is red.[(triple5)] The rabbit likes the mouse.[(triple6)] The rabbit sees the mouse.[(triple7)] @1: The rabbit is kind.[(((triple6) -> rule2))]
The mouse is cold.
("mouse" "is" "cold" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple6
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple6) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1