The bear chases the mouse. The bear chases the tiger. The bear is blue. The bear likes the tiger. The mouse chases the bear. The mouse chases the tiger. The mouse is blue. The mouse is cold. The mouse is kind. The mouse sees the tiger. The tiger is blue. The tiger likes the mouse. If someone is kind and they see the tiger then they see the bear. If someone chases the bear then the bear sees the tiger. If the tiger sees the bear then the bear is red. If someone likes the mouse and the mouse chases the bear then the mouse likes the tiger. If someone chases the tiger and they are blue then they like the tiger. If someone sees the bear then the bear is blue.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If someone is kind and they see the tiger then they see the bear.
((("someone" "is" "kind" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "sees" "bear" "+"))
If someone chases the bear then the bear sees the tiger.
((("someone" "chases" "bear" "+")) -> ("bear" "sees" "tiger" "+"))
If the tiger sees the bear then the bear is red.
((("tiger" "sees" "bear" "+")) -> ("bear" "is" "red" "+"))
If someone likes the mouse and the mouse chases the bear then the mouse likes the tiger.
((("someone" "likes" "mouse" "+") ("mouse" "chases" "bear" "+")) -> ("mouse" "likes" "tiger" "+"))
If someone chases the tiger and they are blue then they like the tiger.
((("someone" "chases" "tiger" "+") ("someone" "is" "blue" "+")) -> ("someone" "likes" "tiger" "+"))
If someone sees the bear then the bear is blue.
((("someone" "sees" "bear" "+")) -> ("bear" "is" "blue" "+"))
The mouse is cold.
True
1
proof
[(triple8)]
("mouse" "is" "cold" "+")
triple8
The bear does not like the tiger.
False
1
inv-proof
[(triple4 OR ((triple2 triple3) -> rule5) OR ((triple2 ((((triple9 triple10) -> rule1)) -> rule6)) -> rule5))]
("bear" "likes" "tiger" "-")
triple4
((triple2 triple3) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
((triple2 ((((triple9 triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int3
The bear does not see the bear.
Unknown
inv-rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "bear" "-")
The tiger likes the bear.
Unknown
random
[@0: The tiger likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "bear" "+")
@0: The bear chases the mouse.[(triple1)] The bear chases the tiger.[(triple2)] The bear is blue.[(triple3 OR ((((triple9 triple10) -> rule1)) -> rule6))] The bear likes the tiger.[(triple4 OR ((triple2 triple3) -> rule5) OR ((triple2 ((((triple9 triple10) -> rule1)) -> rule6)) -> rule5))] The mouse chases the bear.[(triple5)] The mouse chases the tiger.[(triple6)] The mouse is blue.[(triple7)] The mouse is cold.[(triple8)] The mouse is kind.[(triple9)] The mouse sees the tiger.[(triple10)] The tiger is blue.[(triple11)] The tiger likes the mouse.[(triple12)] @1: The bear sees the tiger.[(((triple5) -> rule2))] The mouse likes the tiger.[(((triple12 triple5) -> rule4) OR ((triple6 triple7) -> rule5))] The mouse sees the bear.[(((triple9 triple10) -> rule1))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
((((triple9 triple10) -> (rule1 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple4
((triple2 triple3) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
((triple2 ((((triple9 triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple5
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse is kind.
("mouse" "is" "kind" "+")
triple9
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple12
The bear sees the tiger.
("bear" "sees" "tiger" "+")
((triple5) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((triple12 triple5) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
((triple6 triple7) -> (rule5 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
((triple9 triple10) -> (rule1 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1