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