The cat needs the squirrel. The cat sees the cow. The cow likes the dog. The dog likes the squirrel. The dog needs the squirrel. The squirrel is blue. The squirrel is rough. If something sees the squirrel then the squirrel sees the dog. If something is rough then it sees the dog. If something likes the squirrel then the squirrel likes the cat.
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If something sees the squirrel then the squirrel sees the dog.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "dog" "+"))
If something is rough then it sees the dog.
((("something" "is" "rough" "+")) -> ("something" "sees" "dog" "+"))
If something likes the squirrel then the squirrel likes the cat.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "cat" "+"))
The squirrel is rough.
True
1
proof
[(triple7)]
("squirrel" "is" "rough" "+")
triple7
The cow does not like the dog.
False
1
inv-proof
[(triple3)]
("cow" "likes" "dog" "-")
triple3
The squirrel likes the cat.
True
2
proof
[(((triple4) -> rule3))]
("squirrel" "likes" "cat" "+")
((triple4) -> (rule3 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel does not see the dog.
False
2
inv-proof
[(((triple7) -> rule2))]
("squirrel" "sees" "dog" "-")
((triple7) -> (rule2 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The cat does not see the dog.
Unknown
inv-rconc
[@1: The cat sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "dog" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "dog" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cow sees the squirrel.
Unknown
random
[@0: The cow sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "squirrel" "+")
@0: The cat needs the squirrel.[(triple1)] The cat sees the cow.[(triple2)] The cow likes the dog.[(triple3)] The dog likes the squirrel.[(triple4)] The dog needs the squirrel.[(triple5)] The squirrel is blue.[(triple6)] The squirrel is rough.[(triple7)] @1: The squirrel likes the cat.[(((triple4) -> rule3))] The squirrel sees the dog.[(((triple7) -> rule2))]
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple2
The cow likes the dog.
("cow" "likes" "dog" "+")
triple3
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple4
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple5
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple6
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple7
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
((triple4) -> (rule3 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
((triple7) -> (rule2 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1