The bear is red. The bear likes the rabbit. The bear visits the tiger. The rabbit eats the bear. The rabbit eats the tiger. The rabbit is cold. The rabbit is green. The rabbit is red. The rabbit is rough. The rabbit likes the bear. The rabbit likes the tiger. The rabbit visits the bear. The rabbit visits the tiger. The tiger is rough. The tiger likes the rabbit. The tiger visits the bear. If someone is green then they visit the bear. If someone visits the bear and they are red then the bear is rough. If someone likes the tiger then they like the bear.
The bear is red.
("bear" "is" "red" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone is green then they visit the bear.
((("someone" "is" "green" "+")) -> ("someone" "visits" "bear" "+"))
If someone visits the bear and they are red then the bear is rough.
((("someone" "visits" "bear" "+") ("someone" "is" "red" "+")) -> ("bear" "is" "rough" "+"))
If someone likes the tiger then they like the bear.
((("someone" "likes" "tiger" "+")) -> ("someone" "likes" "bear" "+"))
The bear visits the tiger.
True
1
proof
[(triple3)]
("bear" "visits" "tiger" "+")
triple3
The bear does not like the rabbit.
False
1
inv-proof
[(triple2)]
("bear" "likes" "rabbit" "-")
triple2
The bear is rough.
True
3
proof
[(((triple12 triple8) -> rule2) OR ((((triple7) -> rule1) triple8) -> rule2))]
("bear" "is" "rough" "+")
((triple12 triple8) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
((((triple7) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The bear is not rough.
False
3
inv-proof
[(((triple12 triple8) -> rule2) OR ((((triple7) -> rule1) triple8) -> rule2))]
("bear" "is" "rough" "-")
((triple12 triple8) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
((((triple7) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The tiger does not like the bear.
Unknown
inv-rconc
[@1: The tiger likes the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "bear" "-")
The bear visits the bear.
Unknown
rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "bear" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
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 red.[(triple1)] The bear likes the rabbit.[(triple2)] The bear visits the tiger.[(triple3)] The rabbit eats the bear.[(triple4)] The rabbit eats the tiger.[(triple5)] The rabbit is cold.[(triple6)] The rabbit is green.[(triple7)] The rabbit is red.[(triple8)] The rabbit is rough.[(triple9)] The rabbit likes the bear.[(triple10 OR ((triple11) -> rule3))] The rabbit likes the tiger.[(triple11)] The rabbit visits the bear.[(triple12 OR ((triple7) -> rule1))] The rabbit visits the tiger.[(triple13)] The tiger is rough.[(triple14)] The tiger likes the rabbit.[(triple15)] The tiger visits the bear.[(triple16)] @1: The bear is rough.[(((triple12 triple8) -> rule2) OR ((((triple7) -> rule1) triple8) -> rule2))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple3
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple4
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple8
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple9
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple10
((triple11) -> (rule3 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple11
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple12
((triple7) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple13
The tiger is rough.
("tiger" "is" "rough" "+")
triple14
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple15
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple16
The bear is rough.
("bear" "is" "rough" "+")
((triple12 triple8) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
((((triple7) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2