The bear chases the mouse. The bear is blue. The bear is cold. The bear is green. The bear is nice. The bear is round. The bear needs the mouse. The mouse chases the bear. The mouse is blue. The mouse is cold. The mouse is green. The mouse is nice. The mouse is round. The mouse does not like the bear. The mouse needs the bear. If someone is green and they do not need the mouse then the mouse needs the bear. If the bear chases the mouse then the mouse needs the bear. If someone is blue and not cold then they do not need the bear. If someone needs the bear and the bear does not chase the mouse then they like the mouse. If someone needs the bear then they are green. If someone is cold then they chase the bear.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is round.
("bear" "is" "round" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
If someone is green and they do not need the mouse then the mouse needs the bear.
((("someone" "is" "green" "+") ("someone" "needs" "mouse" "~")) -> ("mouse" "needs" "bear" "+"))
If the bear chases the mouse then the mouse needs the bear.
((("bear" "chases" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
If someone is blue and not cold then they do not need the bear.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "~")) -> ("someone" "needs" "bear" "-"))
If someone needs the bear and the bear does not chase the mouse then they like the mouse.
((("someone" "needs" "bear" "+") ("bear" "chases" "mouse" "~")) -> ("someone" "likes" "mouse" "+"))
If someone needs the bear then they are green.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "green" "+"))
If someone is cold then they chase the bear.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "bear" "+"))
The mouse needs the bear.
True
1
proof
[(triple15 OR ((triple1) -> rule2))]
("mouse" "needs" "bear" "+")
triple15
((triple1) -> (rule2 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is not green.
False
1
inv-proof
[(triple11 OR ((triple15) -> rule5) OR ((((triple1) -> rule2)) -> rule5))]
("mouse" "is" "green" "-")
triple11
((triple15) -> (rule5 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear chases the bear.
True
2
proof
[(((triple3) -> rule6))]
("bear" "chases" "bear" "+")
((triple3) -> (rule6 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear does not chase the bear.
False
2
inv-proof
[(((triple3) -> rule6))]
("bear" "chases" "bear" "-")
((triple3) -> (rule6 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear does not like the mouse.
Unknown
inv-rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear chases the mouse.[(triple1)] The bear is blue.[(triple2)] The bear is cold.[(triple3)] The bear is green.[(triple4)] The bear is nice.[(triple5)] The bear is round.[(triple6)] The bear needs the mouse.[(triple7)] The mouse chases the bear.[(triple8 OR ((triple10) -> rule6))] The mouse does not like the bear.[(triple14)] The mouse is blue.[(triple9)] The mouse is cold.[(triple10)] The mouse is green.[(triple11 OR ((triple15) -> rule5) OR ((((triple1) -> rule2)) -> rule5))] The mouse is nice.[(triple12)] The mouse is round.[(triple13)] The mouse needs the bear.[(triple15 OR ((triple1) -> rule2))] @1: The bear chases the bear.[(((triple3) -> rule6))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple4
The bear is nice.
("bear" "is" "nice" "+")
triple5
The bear is round.
("bear" "is" "round" "+")
triple6
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple7
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple8
((triple10) -> (rule6 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
triple14
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
((triple15) -> (rule5 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
triple12
The mouse is round.
("mouse" "is" "round" "+")
triple13
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple15
((triple1) -> (rule2 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple3) -> (rule6 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1