The bear is young. The bear likes the cat. The bear likes the lion. The bear likes the tiger. The bear sees the cat. The bear sees the lion. The bear visits the lion. The cat is blue. The cat sees the lion. The lion likes the bear. The lion visits the cat. The tiger is blue. The tiger likes the lion. The tiger sees the bear. The tiger visits the bear. If someone visits the cat and they like the bear then the bear is kind. If someone is rough then they see the tiger. If someone sees the cat then they visit the bear. If someone is blue then they see the bear. If the lion sees the cat and the lion is blue then the lion is round. If someone visits the bear then they are rough.
The bear is young.
("bear" "is" "young" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone visits the cat and they like the bear then the bear is kind.
((("someone" "visits" "cat" "+") ("someone" "likes" "bear" "+")) -> ("bear" "is" "kind" "+"))
If someone is rough then they see the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "tiger" "+"))
If someone sees the cat then they visit the bear.
((("someone" "sees" "cat" "+")) -> ("someone" "visits" "bear" "+"))
If someone is blue then they see the bear.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "bear" "+"))
If the lion sees the cat and the lion is blue then the lion is round.
((("lion" "sees" "cat" "+") ("lion" "is" "blue" "+")) -> ("lion" "is" "round" "+"))
If someone visits the bear then they are rough.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "rough" "+"))
The tiger likes the lion.
True
1
proof
[(triple13)]
("tiger" "likes" "lion" "+")
triple13
The bear is not young.
False
1
inv-proof
[(triple1)]
("bear" "is" "young" "-")
triple1
The cat sees the bear.
True
2
proof
[(((triple8) -> rule4))]
("cat" "sees" "bear" "+")
((triple8) -> (rule4 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The bear is not kind.
False
3
inv-proof
[(((triple11 triple10) -> rule1))]
("bear" "is" "kind" "-")
((triple11 triple10) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
True
3
proof
[(((((triple5) -> rule3)) -> rule6))]
("bear" "is" "rough" "+")
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple15) -> rule6)) -> rule2))]
("tiger" "sees" "tiger" "-")
((((triple15) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The bear sees the tiger.
True
4
proof
[(((((((triple5) -> rule3)) -> rule6)) -> rule2))]
("bear" "sees" "tiger" "+")
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The bear does not see the tiger.
False
4
inv-proof
[(((((((triple5) -> rule3)) -> rule6)) -> rule2))]
("bear" "sees" "tiger" "-")
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The lion does not see the bear.
Unknown
inv-rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "bear" "-")
The cat sees the tiger.
Unknown
rconc
[@3: The cat sees the tiger.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule3 <- FAIL)]]
("cat" "sees" "tiger" "+")
The lion does not visit the bear.
Unknown
inv-rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "bear" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "round" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The cat visits the tiger.
Unknown
random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The bear is young.[(triple1)] The bear likes the cat.[(triple2)] The bear likes the lion.[(triple3)] The bear likes the tiger.[(triple4)] The bear sees the cat.[(triple5)] The bear sees the lion.[(triple6)] The bear visits the lion.[(triple7)] The cat is blue.[(triple8)] The cat sees the lion.[(triple9)] The lion likes the bear.[(triple10)] The lion visits the cat.[(triple11)] The tiger is blue.[(triple12)] The tiger likes the lion.[(triple13)] The tiger sees the bear.[(triple14 OR ((triple12) -> rule4))] The tiger visits the bear.[(triple15)] @1: The bear is kind.[(((triple11 triple10) -> rule1))] The bear visits the bear.[(((triple5) -> rule3))] The cat sees the bear.[(((triple8) -> rule4))] The tiger is rough.[(((triple15) -> rule6))] @2: The bear is rough.[(((((triple5) -> rule3)) -> rule6))] The tiger sees the tiger.[(((((triple15) -> rule6)) -> rule2))] @3: The bear sees the tiger.[(((((((triple5) -> rule3)) -> rule6)) -> rule2))]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
The bear likes the lion.
("bear" "likes" "lion" "+")
triple3
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple4
The bear sees the cat.
("bear" "sees" "cat" "+")
triple5
The bear sees the lion.
("bear" "sees" "lion" "+")
triple6
The bear visits the lion.
("bear" "visits" "lion" "+")
triple7
The cat is blue.
("cat" "is" "blue" "+")
triple8
The cat sees the lion.
("cat" "sees" "lion" "+")
triple9
The lion likes the bear.
("lion" "likes" "bear" "+")
triple10
The lion visits the cat.
("lion" "visits" "cat" "+")
triple11
The tiger is blue.
("tiger" "is" "blue" "+")
triple12
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple13
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple14
((triple12) -> (rule4 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple15
The bear is kind.
("bear" "is" "kind" "+")
((triple11 triple10) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple5) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
((triple8) -> (rule4 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple15) -> (rule6 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple15) -> (rule6 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3