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