The dog sees the squirrel. The lion chases the dog. The lion does not chase the squirrel. The lion is blue. The lion does not like the squirrel. The squirrel chases the lion. The squirrel does not like the lion. If the squirrel sees the lion and the squirrel chases the lion then the lion is blue. If something is blue then it chases the lion. If something likes the dog then it sees the lion. If something chases the dog then the dog is red. If the squirrel chases the dog and the dog is young then the squirrel chases the lion. If something sees the lion then it chases the dog. If something is kind and not blue then it likes the squirrel. If something likes the dog then it likes the squirrel.
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
If the squirrel sees the lion and the squirrel chases the lion then the lion is blue.
((("squirrel" "sees" "lion" "+") ("squirrel" "chases" "lion" "+")) -> ("lion" "is" "blue" "+"))
If something is blue then it chases the lion.
((("something" "is" "blue" "+")) -> ("something" "chases" "lion" "+"))
If something likes the dog then it sees the lion.
((("something" "likes" "dog" "+")) -> ("something" "sees" "lion" "+"))
If something chases the dog then the dog is red.
((("something" "chases" "dog" "+")) -> ("dog" "is" "red" "+"))
If the squirrel chases the dog and the dog is young then the squirrel chases the lion.
((("squirrel" "chases" "dog" "+") ("dog" "is" "young" "+")) -> ("squirrel" "chases" "lion" "+"))
If something sees the lion then it chases the dog.
((("something" "sees" "lion" "+")) -> ("something" "chases" "dog" "+"))
If something is kind and not blue then it likes the squirrel.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "likes" "squirrel" "+"))
If something likes the dog then it likes the squirrel.
((("something" "likes" "dog" "+")) -> ("something" "likes" "squirrel" "+"))
The squirrel chases the lion.
True
1
proof
[(triple6)]
("squirrel" "chases" "lion" "+")
triple6
The lion is not blue.
False
1
inv-proof
[(triple4)]
("lion" "is" "blue" "-")
triple4
The dog does not chase the dog.
Unknown
inv-rconc
[@2: The dog chases the dog.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("dog" "chases" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog sees the squirrel.[(triple1)] The lion chases the dog.[(triple2)] The lion does not chase the squirrel.[(triple3)] The lion does not like the squirrel.[(triple5)] The lion is blue.[(triple4)] The squirrel chases the lion.[(triple6)] The squirrel does not like the lion.[(triple7)] @1: The dog is red.[(((triple2) -> rule4))] The lion chases the lion.[(((triple4) -> rule2))]
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple1
The lion chases the dog.
("lion" "chases" "dog" "+")
triple2
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
triple3
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple4
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple6
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
triple7
The dog is red.
("dog" "is" "red" "+")
((triple2) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple4) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1