The cow sees the squirrel. The dog is not nice. The squirrel is red. If the cow needs the squirrel and the cow does not see the dog then the cow is red. If something needs the dog then the dog sees the cow.
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The dog is not nice.
("dog" "is" "nice" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
If the cow needs the squirrel and the cow does not see the dog then the cow is red.
((("cow" "needs" "squirrel" "+") ("cow" "sees" "dog" "~")) -> ("cow" "is" "red" "+"))
If something needs the dog then the dog sees the cow.
((("something" "needs" "dog" "+")) -> ("dog" "sees" "cow" "+"))
The squirrel is red.
True
1
proof
[(triple3)]
("squirrel" "is" "red" "+")
triple3
The squirrel is not red.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "red" "-")
triple3
The dog does not see the cow.
Unknown
inv-rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "cow" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The cow sees the squirrel.[(triple1)] The dog is not nice.[(triple2)] The squirrel is red.[(triple3)]
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple1
The dog is not nice.
("dog" "is" "nice" "-")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3