The bear likes the rabbit. The bear visits the lion. The cat is nice. The lion is rough. The rabbit is kind. The rabbit likes the cat. The rabbit visits the cat. If someone chases the rabbit then they are kind. If someone chases the rabbit then they visit the rabbit. If someone is rough then they visit the rabbit. If someone likes the bear then the bear chases the lion. If someone visits the cat and the cat chases the bear then the cat is kind. If someone visits the rabbit and they are rough then the rabbit is rough.
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cat is nice.
("cat" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If someone chases the rabbit then they are kind.
((("someone" "chases" "rabbit" "+")) -> ("someone" "is" "kind" "+"))
If someone chases the rabbit then they visit the rabbit.
((("someone" "chases" "rabbit" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is rough then they visit the rabbit.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone likes the bear then the bear chases the lion.
((("someone" "likes" "bear" "+")) -> ("bear" "chases" "lion" "+"))
If someone visits the cat and the cat chases the bear then the cat is kind.
((("someone" "visits" "cat" "+") ("cat" "chases" "bear" "+")) -> ("cat" "is" "kind" "+"))
If someone visits the rabbit and they are rough then the rabbit is rough.
((("someone" "visits" "rabbit" "+") ("someone" "is" "rough" "+")) -> ("rabbit" "is" "rough" "+"))
The cat is nice.
True
1
proof
[(triple3)]
("cat" "is" "nice" "+")
triple3
The rabbit is not kind.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "kind" "-")
triple5
The lion visits the rabbit.
True
2
proof
[(((triple4) -> rule3))]
("lion" "visits" "rabbit" "+")
((triple4) -> (rule3 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion does not visit the rabbit.
False
2
inv-proof
[(((triple4) -> rule3))]
("lion" "visits" "rabbit" "-")
((triple4) -> (rule3 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The rabbit is rough.
True
4
proof
[(((((triple4) -> rule3) triple4) -> rule6))]
("rabbit" "is" "rough" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The rabbit is not rough.
False
4
inv-proof
[(((((triple4) -> rule3) triple4) -> rule6))]
("rabbit" "is" "rough" "-")
((((triple4) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The rabbit visits the rabbit.
True
5
proof
[(((((((triple4) -> rule3) triple4) -> rule6)) -> rule3))]
("rabbit" "visits" "rabbit" "+")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int3
The rabbit does not visit the rabbit.
False
5
inv-proof
[(((((((triple4) -> rule3) triple4) -> rule6)) -> rule3))]
("rabbit" "visits" "rabbit" "-")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int3
The cat is not kind.
Unknown
inv-rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "kind" "-")
The bear chases the lion.
Unknown
rconc
[@1: The bear chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "chases" "lion" "+")
The cat does not visit the rabbit.
Unknown
inv-rconc
[@1: The cat visits the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "rabbit" "-")
The lion is kind.
Unknown
rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "kind" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The cat chases the bear.
Unknown
random
[@0: The cat chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bear" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The rabbit likes the bear.
Unknown
random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "+")
@0: The bear likes the rabbit.[(triple1)] The bear visits the lion.[(triple2)] The cat is nice.[(triple3)] The lion is rough.[(triple4)] The rabbit is kind.[(triple5)] The rabbit likes the cat.[(triple6)] The rabbit visits the cat.[(triple7)] @1: The lion visits the rabbit.[(((triple4) -> rule3))] @2: The rabbit is rough.[(((((triple4) -> rule3) triple4) -> rule6))] @3: The rabbit visits the rabbit.[(((((((triple4) -> rule3) triple4) -> rule6)) -> rule3))]
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple1
The bear visits the lion.
("bear" "visits" "lion" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple7
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
((triple4) -> (rule3 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int3