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