The cow is kind. The cow likes the mouse. The cow likes the squirrel. The cow sees the dog. The dog sees the cow. The mouse is red. The mouse likes the cow. The mouse sees the squirrel. The mouse visits the squirrel. The squirrel visits the cow. If something visits the cow and the cow sees the squirrel then the cow is red. If something visits the dog and it sees the mouse then the mouse likes the dog. If something sees the cow then the cow likes the dog.
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If something visits the cow and the cow sees the squirrel then the cow is red.
((("something" "visits" "cow" "+") ("cow" "sees" "squirrel" "+")) -> ("cow" "is" "red" "+"))
If something visits the dog and it sees the mouse then the mouse likes the dog.
((("something" "visits" "dog" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "likes" "dog" "+"))
If something sees the cow then the cow likes the dog.
((("something" "sees" "cow" "+")) -> ("cow" "likes" "dog" "+"))
The mouse likes the cow.
True
1
proof
[(triple7)]
("mouse" "likes" "cow" "+")
triple7
The cow does not see the dog.
False
1
inv-proof
[(triple4)]
("cow" "sees" "dog" "-")
triple4
The mouse does not like the dog.
Unknown
inv-rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "dog" "-")
The cow sees the squirrel.
Unknown
random
[@0: The cow sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "squirrel" "+")
@0: The cow is kind.[(triple1)] The cow likes the mouse.[(triple2)] The cow likes the squirrel.[(triple3)] The cow sees the dog.[(triple4)] The dog sees the cow.[(triple5)] The mouse is red.[(triple6)] The mouse likes the cow.[(triple7)] The mouse sees the squirrel.[(triple8)] The mouse visits the squirrel.[(triple9)] The squirrel visits the cow.[(triple10)] @1: The cow likes the dog.[(((triple5) -> rule3))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple2
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple3
The cow sees the dog.
("cow" "sees" "dog" "+")
triple4
The dog sees the cow.
("dog" "sees" "cow" "+")
triple5
The mouse is red.
("mouse" "is" "red" "+")
triple6
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple7
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple8
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple9
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple10
The cow likes the dog.
("cow" "likes" "dog" "+")
((triple5) -> (rule3 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1