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