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