The bear is green. The bear is nice. The bear is rough. The bear likes the rabbit. The bear sees the tiger. The rabbit chases the bear. The rabbit chases the tiger. The rabbit is nice. The rabbit likes the bear. The rabbit sees the bear. The tiger chases the rabbit. The tiger is cold. The tiger is green. The tiger is nice. The tiger likes the bear. The tiger sees the bear. If someone sees the bear and the bear chases the tiger then they like the bear. If the rabbit likes the tiger then the tiger likes the rabbit. If the bear chases the rabbit then the bear sees the rabbit. If the bear is rough then the bear sees the tiger. If someone is nice then they see the bear. If the rabbit sees the bear then the bear chases the tiger. If the rabbit sees the bear and the bear is round then the rabbit chases the tiger. If someone is rough and they see the tiger then they see the rabbit.
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If someone sees the bear and the bear chases the tiger then they like the bear.
((("someone" "sees" "bear" "+") ("bear" "chases" "tiger" "+")) -> ("someone" "likes" "bear" "+"))
If the rabbit likes the tiger then the tiger likes the rabbit.
((("rabbit" "likes" "tiger" "+")) -> ("tiger" "likes" "rabbit" "+"))
If the bear chases the rabbit then the bear sees the rabbit.
((("bear" "chases" "rabbit" "+")) -> ("bear" "sees" "rabbit" "+"))
If the bear is rough then the bear sees the tiger.
((("bear" "is" "rough" "+")) -> ("bear" "sees" "tiger" "+"))
If someone is nice then they see the bear.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "bear" "+"))
If the rabbit sees the bear then the bear chases the tiger.
((("rabbit" "sees" "bear" "+")) -> ("bear" "chases" "tiger" "+"))
If the rabbit sees the bear and the bear is round then the rabbit chases the tiger.
((("rabbit" "sees" "bear" "+") ("bear" "is" "round" "+")) -> ("rabbit" "chases" "tiger" "+"))
If someone is rough and they see the tiger then they see the rabbit.
((("someone" "is" "rough" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "sees" "rabbit" "+"))
The tiger is green.
True
1
proof
[(triple13)]
("tiger" "is" "green" "+")
triple13
The rabbit does not see the bear.
False
1
inv-proof
[(triple10 OR ((triple8) -> rule5))]
("rabbit" "sees" "bear" "-")
triple10
((triple8) -> (rule5 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The bear sees the rabbit.
True
3
proof
[(((triple3 triple5) -> rule8) OR ((triple3 ((triple3) -> rule4)) -> rule8))]
("bear" "sees" "rabbit" "+")
((triple3 triple5) -> (rule8 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
((triple3 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear does not chase the tiger.
False
2
inv-proof
[(((triple10) -> rule6) OR ((((triple8) -> rule5)) -> rule6))]
("bear" "chases" "tiger" "-")
((triple10) -> (rule6 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule6 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int2
The bear likes the bear.
True
5
proof
[(((((triple2) -> rule5) ((triple10) -> rule6)) -> rule1) OR ((((triple2) -> rule5) ((((triple8) -> rule5)) -> rule6)) -> rule1))]
("bear" "likes" "bear" "+")
((((triple2) -> (rule5 % int3)) ((triple10) -> (rule6 % int2))) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((triple2) -> (rule5 % int4)) ((((triple8) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4
The bear does not like the bear.
False
5
inv-proof
[(((((triple2) -> rule5) ((triple10) -> rule6)) -> rule1) OR ((((triple2) -> rule5) ((((triple8) -> rule5)) -> rule6)) -> rule1))]
("bear" "likes" "bear" "-")
((((triple2) -> (rule5 % int3)) ((triple10) -> (rule6 % int2))) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((triple2) -> (rule5 % int4)) ((((triple8) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4
The tiger does not like the rabbit.
Unknown
inv-rconc
[@1: The tiger likes the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "sees" "rabbit" "+")
The tiger does not see the rabbit.
Unknown
inv-rconc
[@1: The tiger sees the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "sees" "rabbit" "-")
The rabbit sees the tiger.
Unknown
random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The bear is green.[(triple1)] The bear is nice.[(triple2)] The bear is rough.[(triple3)] The bear likes the rabbit.[(triple4)] The bear sees the tiger.[(triple5 OR ((triple3) -> rule4))] The rabbit chases the bear.[(triple6)] The rabbit chases the tiger.[(triple7)] The rabbit is nice.[(triple8)] The rabbit likes the bear.[(triple9 OR ((triple10 ((triple10) -> rule6)) -> rule1) OR ((((triple8) -> rule5) ((triple10) -> rule6)) -> rule1) OR ((triple10 ((((triple8) -> rule5)) -> rule6)) -> rule1) OR ((((triple8) -> rule5) ((((triple8) -> rule5)) -> rule6)) -> rule1))] The rabbit sees the bear.[(triple10 OR ((triple8) -> rule5))] The tiger chases the rabbit.[(triple11)] The tiger is cold.[(triple12)] The tiger is green.[(triple13)] The tiger is nice.[(triple14)] The tiger likes the bear.[(triple15 OR ((triple16 ((triple10) -> rule6)) -> rule1) OR ((((triple14) -> rule5) ((triple10) -> rule6)) -> rule1) OR ((triple16 ((((triple8) -> rule5)) -> rule6)) -> rule1) OR ((((triple14) -> rule5) ((((triple8) -> rule5)) -> rule6)) -> rule1))] The tiger sees the bear.[(triple16 OR ((triple14) -> rule5))] @1: The bear chases the tiger.[(((triple10) -> rule6) OR ((((triple8) -> rule5)) -> rule6))] The bear sees the bear.[(((triple2) -> rule5))] The bear sees the rabbit.[(((triple3 triple5) -> rule8) OR ((triple3 ((triple3) -> rule4)) -> rule8))] @2: The bear likes the bear.[(((((triple2) -> rule5) ((triple10) -> rule6)) -> rule1) OR ((((triple2) -> rule5) ((((triple8) -> rule5)) -> rule6)) -> rule1))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple4
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple5
((triple3) -> (rule4 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple6
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple9
((triple10 ((triple10) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
((((triple8) -> (rule5 % int3)) ((triple10) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int3
((triple10 ((((triple8) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int3
((((triple8) -> (rule5 % int3)) ((((triple8) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int3
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple10
((triple8) -> (rule5 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is green.
("tiger" "is" "green" "+")
triple13
The tiger is nice.
("tiger" "is" "nice" "+")
triple14
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple15
((triple16 ((triple10) -> (rule6 % int2))) -> (rule1 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
((((triple14) -> (rule5 % int3)) ((triple10) -> (rule6 % int2))) -> (rule1 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int3
((triple16 ((((triple8) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int3
((((triple14) -> (rule5 % int4)) ((((triple8) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int3
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int4
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple16
((triple14) -> (rule5 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((triple10) -> (rule6 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule6 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple2) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
((triple3 triple5) -> (rule8 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
((triple3 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
((((triple2) -> (rule5 % int3)) ((triple10) -> (rule6 % int2))) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
((((triple2) -> (rule5 % int4)) ((((triple8) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4