The bear is young. The bear needs the mouse. The mouse is green. The mouse is kind. The mouse is young. The mouse likes the bear. The mouse visits the bear. If something is round and it likes the bear then the bear is kind. If something is kind then it likes the mouse.
The bear is young.
("bear" "is" "young" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If something is round and it likes the bear then the bear is kind.
((("something" "is" "round" "+") ("something" "likes" "bear" "+")) -> ("bear" "is" "kind" "+"))
If something is kind then it likes the mouse.
((("something" "is" "kind" "+")) -> ("something" "likes" "mouse" "+"))
The mouse is kind.
True
1
proof
[(triple4)]
("mouse" "is" "kind" "+")
triple4
The mouse does not like the bear.
False
1
inv-proof
[(triple6)]
("mouse" "likes" "bear" "-")
triple6
The mouse likes the mouse.
True
2
proof
[(((triple4) -> rule2))]
("mouse" "likes" "mouse" "+")
((triple4) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple4) -> rule2))]
("mouse" "likes" "mouse" "-")
((triple4) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The bear does not like the mouse.
Unknown
inv-rconc
[@2: The bear likes the mouse.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("bear" "likes" "mouse" "-")
The bear is kind.
Unknown
rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "kind" "+")
The mouse does not need the bear.
Unknown
inv-random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The bear is young.[(triple1)] The bear needs the mouse.[(triple2)] The mouse is green.[(triple3)] The mouse is kind.[(triple4)] The mouse is young.[(triple5)] The mouse likes the bear.[(triple6)] The mouse visits the bear.[(triple7)] @1: The mouse likes the mouse.[(((triple4) -> rule2))]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple6
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple7
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple4) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1