The cat does not visit the rabbit. The rabbit chases the cat. If the cat is kind then the cat is blue. If the rabbit chases the cat then the rabbit is cold. If the cat is big and the cat is green then the cat does not chase the rabbit. If the cat is cold then the cat chases the rabbit. If someone is blue then they visit the rabbit. If someone chases the cat then they do not like the cat. If the rabbit is cold and the cat does not like the rabbit then the rabbit visits the cat. If someone is blue then they are green.
The cat does not visit the rabbit.
("cat" "visits" "rabbit" "-")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
If the cat is kind then the cat is blue.
((("cat" "is" "kind" "+")) -> ("cat" "is" "blue" "+"))
If the rabbit chases the cat then the rabbit is cold.
((("rabbit" "chases" "cat" "+")) -> ("rabbit" "is" "cold" "+"))
If the cat is big and the cat is green then the cat does not chase the rabbit.
((("cat" "is" "big" "+") ("cat" "is" "green" "+")) -> ("cat" "chases" "rabbit" "-"))
If the cat is cold then the cat chases the rabbit.
((("cat" "is" "cold" "+")) -> ("cat" "chases" "rabbit" "+"))
If someone is blue then they visit the rabbit.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone chases the cat then they do not like the cat.
((("someone" "chases" "cat" "+")) -> ("someone" "likes" "cat" "-"))
If the rabbit is cold and the cat does not like the rabbit then the rabbit visits the cat.
((("rabbit" "is" "cold" "+") ("cat" "likes" "rabbit" "~")) -> ("rabbit" "visits" "cat" "+"))
If someone is blue then they are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
The cat does not visit the rabbit.
True
1
proof
[(triple1)]
("cat" "visits" "rabbit" "-")
triple1
The cat visits the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "visits" "rabbit" "+")
triple1
The rabbit does not like the cat.
True
2
proof
[(((triple2) -> rule6))]
("rabbit" "likes" "cat" "-")
((triple2) -> (rule6 % int1))
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
int1
The rabbit is not cold.
False
2
inv-proof
[(((triple2) -> rule2))]
("rabbit" "is" "cold" "-")
((triple2) -> (rule2 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "blue" "-")
The cat is green.
Unknown
rconc
[@2: The cat is green.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("cat" "is" "green" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The cat does not visit the rabbit.[(triple1)] The rabbit chases the cat.[(triple2)] @1: The rabbit does not like the cat.[(((triple2) -> rule6))] The rabbit is cold.[(((triple2) -> rule2))]
The cat does not visit the rabbit.
("cat" "visits" "rabbit" "-")
triple1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple2
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
((triple2) -> (rule6 % int1))
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple2) -> (rule2 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1