The cat visits the rabbit. The rabbit is kind. The rabbit needs the cat. If something needs the cat and it does not like the cat then the cat needs the rabbit. If the cat likes the rabbit then the cat is round. If something is blue then it does not visit the cat. If something visits the rabbit then it likes the rabbit. If something likes the cat then it is blue. If the cat needs the rabbit and the cat likes the rabbit then the cat is big. If something visits the rabbit and it needs the cat then the cat visits the rabbit. If something visits the rabbit then it is young.
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something needs the cat and it does not like the cat then the cat needs the rabbit.
((("something" "needs" "cat" "+") ("something" "likes" "cat" "~")) -> ("cat" "needs" "rabbit" "+"))
If the cat likes the rabbit then the cat is round.
((("cat" "likes" "rabbit" "+")) -> ("cat" "is" "round" "+"))
If something is blue then it does not visit the cat.
((("something" "is" "blue" "+")) -> ("something" "visits" "cat" "-"))
If something visits the rabbit then it likes the rabbit.
((("something" "visits" "rabbit" "+")) -> ("something" "likes" "rabbit" "+"))
If something likes the cat then it is blue.
((("something" "likes" "cat" "+")) -> ("something" "is" "blue" "+"))
If the cat needs the rabbit and the cat likes the rabbit then the cat is big.
((("cat" "needs" "rabbit" "+") ("cat" "likes" "rabbit" "+")) -> ("cat" "is" "big" "+"))
If something visits the rabbit and it needs the cat then the cat visits the rabbit.
((("something" "visits" "rabbit" "+") ("something" "needs" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If something visits the rabbit then it is young.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "young" "+"))
The cat visits the rabbit.
True
1
proof
[(triple1)]
("cat" "visits" "rabbit" "+")
triple1
The rabbit is not kind.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "kind" "-")
triple2
The cat likes the rabbit.
True
2
proof
[(((triple1) -> rule4))]
("cat" "likes" "rabbit" "+")
((triple1) -> (rule4 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat does not like the rabbit.
False
2
inv-proof
[(((triple1) -> rule4))]
("cat" "likes" "rabbit" "-")
((triple1) -> (rule4 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat is round.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("cat" "is" "round" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The cat is not round.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("cat" "is" "round" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit is young.
Unknown
rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "young" "+")
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "blue" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The rabbit does not visit the cat.
Unknown
inv-random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The cat visits the rabbit.[(triple1)] The rabbit is kind.[(triple2)] The rabbit needs the cat.[(triple3)] @1: The cat is young.[(((triple1) -> rule8))] The cat likes the rabbit.[(((triple1) -> rule4))] @2: The cat is round.[(((((triple1) -> rule4)) -> rule2))]
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
((triple1) -> (rule8 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
((triple1) -> (rule4 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2