The cow visits the mouse. The dog sees the mouse. The mouse visits the dog. The squirrel is rough. If someone sees the mouse then the mouse chases the dog. All kind people are red. If someone sees the cow and they visit the mouse then they are big. If the mouse chases the cow then the mouse is kind. If someone is rough and they chase the cow then the cow sees the mouse. If someone sees the squirrel and the squirrel chases the mouse then the mouse chases the squirrel.
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If someone sees the mouse then the mouse chases the dog.
((("someone" "sees" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone sees the cow and they visit the mouse then they are big.
((("someone" "sees" "cow" "+") ("someone" "visits" "mouse" "+")) -> ("someone" "is" "big" "+"))
If the mouse chases the cow then the mouse is kind.
((("mouse" "chases" "cow" "+")) -> ("mouse" "is" "kind" "+"))
If someone is rough and they chase the cow then the cow sees the mouse.
((("someone" "is" "rough" "+") ("someone" "chases" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If someone sees the squirrel and the squirrel chases the mouse then the mouse chases the squirrel.
((("someone" "sees" "squirrel" "+") ("squirrel" "chases" "mouse" "+")) -> ("mouse" "chases" "squirrel" "+"))
The cow visits the mouse.
True
1
proof
[(triple1)]
("cow" "visits" "mouse" "+")
triple1
The dog does not see the mouse.
False
1
inv-proof
[(triple2)]
("dog" "sees" "mouse" "-")
triple2
The mouse chases the dog.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "chases" "dog" "+")
((triple2) -> (rule1 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse does not chase the dog.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "chases" "dog" "-")
((triple2) -> (rule1 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "red" "-")
The cow is red.
Unknown
rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "red" "+")
The mouse does not see the squirrel.
Unknown
inv-random
[@0: The mouse sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "squirrel" "-")
The mouse visits the cow.
Unknown
random
[@0: The mouse visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cow" "+")
@0: The cow visits the mouse.[(triple1)] The dog sees the mouse.[(triple2)] The mouse visits the dog.[(triple3)] The squirrel is rough.[(triple4)] @1: The mouse chases the dog.[(((triple2) -> rule1))]
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple3
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple4
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((triple2) -> (rule1 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1