The dog sees the squirrel. The squirrel is red. If something eats the squirrel and it chases the dog then the squirrel is big. If something chases the squirrel then the squirrel chases the dog. If something is red and it eats the squirrel then the squirrel is cold.
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
If something eats the squirrel and it chases the dog then the squirrel is big.
((("something" "eats" "squirrel" "+") ("something" "chases" "dog" "+")) -> ("squirrel" "is" "big" "+"))
If something chases the squirrel then the squirrel chases the dog.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "chases" "dog" "+"))
If something is red and it eats the squirrel then the squirrel is cold.
((("something" "is" "red" "+") ("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
The dog sees the squirrel.
True
1
proof
[(triple1)]
("dog" "sees" "squirrel" "+")
triple1
The squirrel is not red.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "red" "-")
triple2
The squirrel does not chase the dog.
Unknown
inv-rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "dog" "-")
The dog chases the squirrel.
Unknown
random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "+")
@0: The dog sees the squirrel.[(triple1)] The squirrel is red.[(triple2)]
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple1
The squirrel is red.
("squirrel" "is" "red" "+")
triple2