The cow sees the dog. The dog sees the squirrel. The mouse sees the dog. The squirrel likes the cow. If the cow is green and the cow likes the mouse then the cow likes the squirrel. If the mouse chases the dog and the mouse likes the squirrel then the dog chases the cow. If someone likes the mouse and the mouse chases the squirrel then the mouse sees the squirrel. If someone is green then they like the dog. If someone sees the squirrel then they see the mouse. If someone sees the mouse then the mouse is round.
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
If the cow is green and the cow likes the mouse then the cow likes the squirrel.
((("cow" "is" "green" "+") ("cow" "likes" "mouse" "+")) -> ("cow" "likes" "squirrel" "+"))
If the mouse chases the dog and the mouse likes the squirrel then the dog chases the cow.
((("mouse" "chases" "dog" "+") ("mouse" "likes" "squirrel" "+")) -> ("dog" "chases" "cow" "+"))
If someone likes the mouse and the mouse chases the squirrel then the mouse sees the squirrel.
((("someone" "likes" "mouse" "+") ("mouse" "chases" "squirrel" "+")) -> ("mouse" "sees" "squirrel" "+"))
If someone is green then they like the dog.
((("someone" "is" "green" "+")) -> ("someone" "likes" "dog" "+"))
If someone sees the squirrel then they see the mouse.
((("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the mouse then the mouse is round.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "round" "+"))
The mouse sees the dog.
True
1
proof
[(triple3)]
("mouse" "sees" "dog" "+")
triple3
The mouse does not see the dog.
False
1
inv-proof
[(triple3)]
("mouse" "sees" "dog" "-")
triple3
The dog sees the mouse.
True
2
proof
[(((triple2) -> rule5))]
("dog" "sees" "mouse" "+")
((triple2) -> (rule5 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog does not see the mouse.
False
2
inv-proof
[(((triple2) -> rule5))]
("dog" "sees" "mouse" "-")
((triple2) -> (rule5 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The mouse is round.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("mouse" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The mouse is not round.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("mouse" "is" "round" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The mouse does not see the mouse.
Unknown
inv-rconc
[@2: The mouse sees the mouse.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse likes the dog.
Unknown
rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "dog" "+")
The squirrel does not see the mouse.
Unknown
inv-rconc
[@1: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "mouse" "-")
The dog likes the squirrel.
Unknown
random
[@0: The dog likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "squirrel" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The cow sees the dog.[(triple1)] The dog sees the squirrel.[(triple2)] The mouse sees the dog.[(triple3)] The squirrel likes the cow.[(triple4)] @1: The dog sees the mouse.[(((triple2) -> rule5))] @2: The mouse is round.[(((((triple2) -> rule5)) -> rule6))]
The cow sees the dog.
("cow" "sees" "dog" "+")
triple1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple3
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((triple2) -> (rule5 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2