The cow eats the dog. The cow is cold. The cow sees the mouse. The cow sees the squirrel. The dog eats the squirrel. The dog likes the squirrel. The mouse eats the dog. The mouse is big. The squirrel likes the dog. The squirrel likes the mouse. If someone likes the dog then they see the dog. If someone likes the squirrel then they eat the squirrel.
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If someone likes the dog then they see the dog.
((("someone" "likes" "dog" "+")) -> ("someone" "sees" "dog" "+"))
If someone likes the squirrel then they eat the squirrel.
((("someone" "likes" "squirrel" "+")) -> ("someone" "eats" "squirrel" "+"))
The dog likes the squirrel.
True
1
proof
[(triple6)]
("dog" "likes" "squirrel" "+")
triple6
The dog does not like the squirrel.
False
1
inv-proof
[(triple6)]
("dog" "likes" "squirrel" "-")
triple6
The squirrel sees the dog.
True
2
proof
[(((triple9) -> rule1))]
("squirrel" "sees" "dog" "+")
((triple9) -> (rule1 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The squirrel does not see the dog.
False
2
inv-proof
[(((triple9) -> rule1))]
("squirrel" "sees" "dog" "-")
((triple9) -> (rule1 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "dog" "-")
The cow sees the dog.
Unknown
rconc
[@1: The cow sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "dog" "+")
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 mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cow eats the dog.[(triple1)] The cow is cold.[(triple2)] The cow sees the mouse.[(triple3)] The cow sees the squirrel.[(triple4)] The dog eats the squirrel.[(triple5 OR ((triple6) -> rule2))] The dog likes the squirrel.[(triple6)] The mouse eats the dog.[(triple7)] The mouse is big.[(triple8)] The squirrel likes the dog.[(triple9)] The squirrel likes the mouse.[(triple10)] @1: The squirrel sees the dog.[(((triple9) -> rule1))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple3
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple4
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple5
((triple6) -> (rule2 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple6
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple8
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple9
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple10
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
((triple9) -> (rule1 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1