The dog likes the squirrel. The dog needs the squirrel. The squirrel likes the dog. If something sees the dog and it is not round then the dog likes the squirrel. If the squirrel is kind and the squirrel is red then the squirrel needs the dog. If something likes the squirrel then the squirrel is not blue.
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
If something sees the dog and it is not round then the dog likes the squirrel.
((("something" "sees" "dog" "+") ("something" "is" "round" "~")) -> ("dog" "likes" "squirrel" "+"))
If the squirrel is kind and the squirrel is red then the squirrel needs the dog.
((("squirrel" "is" "kind" "+") ("squirrel" "is" "red" "+")) -> ("squirrel" "needs" "dog" "+"))
If something likes the squirrel then the squirrel is not blue.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "is" "blue" "-"))
The dog needs the squirrel.
True
1
proof
[(triple2)]
("dog" "needs" "squirrel" "+")
triple2
The dog does not like the squirrel.
False
1
inv-proof
[(triple1)]
("dog" "likes" "squirrel" "-")
triple1
The squirrel does not need the dog.
Unknown
inv-rconc
[@1: The squirrel needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "dog" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The dog likes the squirrel.[(triple1)] The dog needs the squirrel.[(triple2)] The squirrel likes the dog.[(triple3)] @1: The squirrel is not blue.[(((triple1) -> rule3))]
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple2
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple3
The squirrel is not blue.
("squirrel" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The squirrel is not blue.
("squirrel" "is" "blue" "-")
int1