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