The cat is not red. The cat likes the rabbit. The cat likes the tiger. The cat needs the rabbit. The cat visits the mouse. The mouse is cold. The mouse is kind. The mouse is red. The mouse does not like the tiger. The rabbit likes the tiger. The rabbit needs the cat. The rabbit needs the mouse. The rabbit visits the cat. The tiger is red. The tiger likes the rabbit. The tiger does not need the cat. If someone likes the mouse and they are not kind then they need the mouse. If someone visits the rabbit and they do not like the mouse then the mouse needs the rabbit. If someone needs the cat then they are red.
The cat is not red.
("cat" "is" "red" "-")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
If someone likes the mouse and they are not kind then they need the mouse.
((("someone" "likes" "mouse" "+") ("someone" "is" "kind" "~")) -> ("someone" "needs" "mouse" "+"))
If someone visits the rabbit and they do not like the mouse then the mouse needs the rabbit.
((("someone" "visits" "rabbit" "+") ("someone" "likes" "mouse" "~")) -> ("mouse" "needs" "rabbit" "+"))
If someone needs the cat then they are red.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "red" "+"))
The rabbit likes the tiger.
True
1
proof
[(triple10)]
("rabbit" "likes" "tiger" "+")
triple10
The mouse likes the tiger.
False
1
inv-proof
[(triple9)]
("mouse" "likes" "tiger" "+")
triple9
The rabbit is red.
True
2
proof
[(((triple11) -> rule3))]
("rabbit" "is" "red" "+")
((triple11) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple11) -> rule3))]
("rabbit" "is" "red" "-")
((triple11) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The cat does not need the mouse.
Unknown
inv-rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "mouse" "-")
The mouse needs the rabbit.
Unknown
rconc
[@1: The mouse needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "rabbit" "+")
The tiger does not need the rabbit.
Unknown
inv-random
[@0: The tiger needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "rabbit" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cat is not red.[(triple1)] The cat likes the rabbit.[(triple2)] The cat likes the tiger.[(triple3)] The cat needs the rabbit.[(triple4)] The cat visits the mouse.[(triple5)] The mouse does not like the tiger.[(triple9)] The mouse is cold.[(triple6)] The mouse is kind.[(triple7)] The mouse is red.[(triple8)] The rabbit likes the tiger.[(triple10)] The rabbit needs the cat.[(triple11)] The rabbit needs the mouse.[(triple12)] The rabbit visits the cat.[(triple13)] The tiger does not need the cat.[(triple16)] The tiger is red.[(triple14)] The tiger likes the rabbit.[(triple15)] @1: The rabbit is red.[(((triple11) -> rule3))]
The cat is not red.
("cat" "is" "red" "-")
triple1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple4
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple5
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple6
The mouse is kind.
("mouse" "is" "kind" "+")
triple7
The mouse is red.
("mouse" "is" "red" "+")
triple8
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple10
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple11
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple12
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple13
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
triple16
The tiger is red.
("tiger" "is" "red" "+")
triple14
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple15
The rabbit is red.
("rabbit" "is" "red" "+")
((triple11) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1