The cat visits the rabbit. The mouse chases the rabbit. The mouse is green. The rabbit chases the cat. The rabbit does not chase the mouse. The rabbit is not big. The rabbit visits the mouse. If something is nice and it visits the rabbit then the rabbit is green. If the rabbit chases the cat and the rabbit visits the mouse then the rabbit likes the cat. If the rabbit chases the cat and the rabbit is not green then the rabbit likes the cat.
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is green.
("mouse" "is" "green" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
The rabbit is not big.
("rabbit" "is" "big" "-")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something is nice and it visits the rabbit then the rabbit is green.
((("something" "is" "nice" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If the rabbit chases the cat and the rabbit visits the mouse then the rabbit likes the cat.
((("rabbit" "chases" "cat" "+") ("rabbit" "visits" "mouse" "+")) -> ("rabbit" "likes" "cat" "+"))
If the rabbit chases the cat and the rabbit is not green then the rabbit likes the cat.
((("rabbit" "chases" "cat" "+") ("rabbit" "is" "green" "~")) -> ("rabbit" "likes" "cat" "+"))
The cat visits the rabbit.
True
1
proof
[(triple1)]
("cat" "visits" "rabbit" "+")
triple1
The rabbit chases the mouse.
False
1
inv-proof
[(triple5)]
("rabbit" "chases" "mouse" "+")
triple5
The rabbit likes the cat.
True
3
proof
[(((triple4 triple7) -> rule2))]
("rabbit" "likes" "cat" "+")
((triple4 triple7) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit does not like the cat.
False
3
inv-proof
[(((triple4 triple7) -> rule2))]
("rabbit" "likes" "cat" "-")
((triple4 triple7) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "green" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The cat does not chase the mouse.
Unknown
inv-random
[@0: The cat chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The cat visits the rabbit.[(triple1)] The mouse chases the rabbit.[(triple2)] The mouse is green.[(triple3)] The rabbit chases the cat.[(triple4)] The rabbit does not chase the mouse.[(triple5)] The rabbit is not big.[(triple6)] The rabbit visits the mouse.[(triple7)] @1: The rabbit likes the cat.[(((triple4 triple7) -> rule2))]
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple4
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
triple5
The rabbit is not big.
("rabbit" "is" "big" "-")
triple6
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple7
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((triple4 triple7) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1