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