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