The cat chases the mouse. The dog chases the rabbit. The dog is not green. The dog does not like the mouse. The dog likes the rabbit. The dog sees the cat. The mouse chases the cat. The mouse does not chase the rabbit. The mouse does not like the dog. The rabbit does not chase the cat. The rabbit is not green. The rabbit likes the dog. The rabbit likes the mouse. The rabbit sees the cat. The rabbit does not see the mouse. If someone chases the rabbit and they do not see the dog then they are not kind. If the dog is blue then the dog chases the mouse. If the mouse chases the cat then the cat likes the rabbit. If the dog does not see the rabbit and the rabbit does not like the cat then the cat likes the rabbit. If someone sees the dog then the dog does not like the cat. If someone chases the cat and the cat chases the rabbit then the cat sees the mouse. If the cat chases the rabbit and the cat is not kind then the cat likes the mouse. If someone likes the cat then the cat likes the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is not green.
("dog" "is" "green" "-")
The dog does not like the mouse.
("dog" "likes" "mouse" "-")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit is not green.
("rabbit" "is" "green" "-")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
If someone chases the rabbit and they do not see the dog then they are not kind.
((("someone" "chases" "rabbit" "+") ("someone" "sees" "dog" "~")) -> ("someone" "is" "kind" "-"))
If the dog is blue then the dog chases the mouse.
((("dog" "is" "blue" "+")) -> ("dog" "chases" "mouse" "+"))
If the mouse chases the cat then the cat likes the rabbit.
((("mouse" "chases" "cat" "+")) -> ("cat" "likes" "rabbit" "+"))
If the dog does not see the rabbit and the rabbit does not like the cat then the cat likes the rabbit.
((("dog" "sees" "rabbit" "~") ("rabbit" "likes" "cat" "~")) -> ("cat" "likes" "rabbit" "+"))
If someone sees the dog then the dog does not like the cat.
((("someone" "sees" "dog" "+")) -> ("dog" "likes" "cat" "-"))
If someone chases the cat and the cat chases the rabbit then the cat sees the mouse.
((("someone" "chases" "cat" "+") ("cat" "chases" "rabbit" "+")) -> ("cat" "sees" "mouse" "+"))
If the cat chases the rabbit and the cat is not kind then the cat likes the mouse.
((("cat" "chases" "rabbit" "+") ("cat" "is" "kind" "~")) -> ("cat" "likes" "mouse" "+"))
If someone likes the cat then the cat likes the mouse.
((("someone" "likes" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
The mouse does not chase the rabbit.
True
1
proof
[(triple8)]
("mouse" "chases" "rabbit" "-")
triple8
The dog is green.
False
1
inv-proof
[(triple3)]
("dog" "is" "green" "+")
triple3
The cat does not see the mouse.
Unknown
inv-rconc
[@1: The cat sees the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "mouse" "-")
The dog sees the rabbit.
Unknown
random
[@0: The dog sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "rabbit" "+")
@0: The cat chases the mouse.[(triple1)] The dog chases the rabbit.[(triple2)] The dog does not like the mouse.[(triple4)] The dog is not green.[(triple3)] The dog likes the rabbit.[(triple5)] The dog sees the cat.[(triple6)] The mouse chases the cat.[(triple7)] The mouse does not chase the rabbit.[(triple8)] The mouse does not like the dog.[(triple9)] The rabbit does not chase the cat.[(triple10)] The rabbit does not see the mouse.[(triple15)] The rabbit is not green.[(triple11)] The rabbit likes the dog.[(triple12)] The rabbit likes the mouse.[(triple13)] The rabbit sees the cat.[(triple14)] @1: The cat likes the rabbit.[(((triple7) -> rule3))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple2
The dog does not like the mouse.
("dog" "likes" "mouse" "-")
triple4
The dog is not green.
("dog" "is" "green" "-")
triple3
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple5
The dog sees the cat.
("dog" "sees" "cat" "+")
triple6
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple7
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
triple8
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
triple9
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple10
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
triple15
The rabbit is not green.
("rabbit" "is" "green" "-")
triple11
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple12
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple13
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple14
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
((triple7) -> (rule3 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1