The bear is kind. The bear needs the rabbit. The bear visits the rabbit. The cat is big. The cat likes the bear. The cat likes the rabbit. The cat needs the bear. The rabbit is kind. The rabbit needs the bear. The rabbit visits the cat. If someone is blue then they visit the cat. If the bear needs the rabbit and the bear visits the cat then the rabbit is rough. All kind people are blue. If someone likes the rabbit then the rabbit likes the cat. If someone needs the rabbit and the rabbit is cold then they are rough. If someone likes the rabbit then the rabbit needs the bear. If someone likes the rabbit and they visit the cat then the rabbit visits the bear. If the rabbit is kind then the rabbit likes the cat.
The bear is kind.
("bear" "is" "kind" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The cat is big.
("cat" "is" "big" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If someone is blue then they visit the cat.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "cat" "+"))
If the bear needs the rabbit and the bear visits the cat then the rabbit is rough.
((("bear" "needs" "rabbit" "+") ("bear" "visits" "cat" "+")) -> ("rabbit" "is" "rough" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone likes the rabbit then the rabbit likes the cat.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "likes" "cat" "+"))
If someone needs the rabbit and the rabbit is cold then they are rough.
((("someone" "needs" "rabbit" "+") ("rabbit" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the rabbit then the rabbit needs the bear.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "needs" "bear" "+"))
If someone likes the rabbit and they visit the cat then the rabbit visits the bear.
((("someone" "likes" "rabbit" "+") ("someone" "visits" "cat" "+")) -> ("rabbit" "visits" "bear" "+"))
If the rabbit is kind then the rabbit likes the cat.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "likes" "cat" "+"))
The rabbit needs the bear.
True
1
proof
[(triple9 OR ((triple6) -> rule6))]
("rabbit" "needs" "bear" "+")
triple9
((triple6) -> (rule6 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The cat does not like the rabbit.
False
1
inv-proof
[(triple6)]
("cat" "likes" "rabbit" "-")
triple6
The rabbit is blue.
True
2
proof
[(((triple8) -> rule3))]
("rabbit" "is" "blue" "+")
((triple8) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit does not like the cat.
False
2
inv-proof
[(((triple6) -> rule4) OR ((triple8) -> rule8))]
("rabbit" "likes" "cat" "-")
((triple6) -> (rule4 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
((triple8) -> (rule8 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The bear visits the cat.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("bear" "visits" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear does not visit the cat.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("bear" "visits" "cat" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The rabbit is rough.
True
5
proof
[(((triple2 ((((triple1) -> rule3)) -> rule1)) -> rule2))]
("rabbit" "is" "rough" "+")
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The rabbit is not rough.
False
5
inv-proof
[(((triple2 ((((triple1) -> rule3)) -> rule1)) -> rule2))]
("rabbit" "is" "rough" "-")
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "rough" "-")
The cat is blue.
Unknown
rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "blue" "+")
The rabbit does not visit the bear.
Unknown
inv-rconc
[@3: The rabbit visits the bear.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule3 <- FAIL)]]
("rabbit" "visits" "bear" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "rough" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The rabbit likes the bear.
Unknown
random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "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 bear is kind.[(triple1)] The bear needs the rabbit.[(triple2)] The bear visits the rabbit.[(triple3)] The cat is big.[(triple4)] The cat likes the bear.[(triple5)] The cat likes the rabbit.[(triple6)] The cat needs the bear.[(triple7)] The rabbit is kind.[(triple8)] The rabbit needs the bear.[(triple9 OR ((triple6) -> rule6))] The rabbit visits the cat.[(triple10 OR ((((triple8) -> rule3)) -> rule1))] @1: The bear is blue.[(((triple1) -> rule3))] The rabbit is blue.[(((triple8) -> rule3))] The rabbit likes the cat.[(((triple6) -> rule4) OR ((triple8) -> rule8))] @2: The bear visits the cat.[(((((triple1) -> rule3)) -> rule1))] @3: The rabbit is rough.[(((triple2 ((((triple1) -> rule3)) -> rule1)) -> rule2))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple2
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple3
The cat is big.
("cat" "is" "big" "+")
triple4
The cat likes the bear.
("cat" "likes" "bear" "+")
triple5
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple6
The cat needs the bear.
("cat" "needs" "bear" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple8
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple9
((triple6) -> (rule6 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple10
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple8) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((triple6) -> (rule4 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
((triple8) -> (rule8 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3