The cat visits the dog. The dog is red. The lion is kind. The mouse is nice. If something visits the lion and the lion is kind then it visits the mouse. If something is nice and it sees the dog then the dog sees the lion.
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is red.
("dog" "is" "red" "+")
The lion is kind.
("lion" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
If something visits the lion and the lion is kind then it visits the mouse.
((("something" "visits" "lion" "+") ("lion" "is" "kind" "+")) -> ("something" "visits" "mouse" "+"))
If something is nice and it sees the dog then the dog sees the lion.
((("something" "is" "nice" "+") ("something" "sees" "dog" "+")) -> ("dog" "sees" "lion" "+"))
The cat visits the dog.
True
1
proof
[(triple1)]
("cat" "visits" "dog" "+")
triple1
The dog is not red.
False
1
inv-proof
[(triple2)]
("dog" "is" "red" "-")
triple2
The dog does not visit the mouse.
Unknown
inv-rconc
[@1: The dog visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "mouse" "-")
The mouse visits the cat.
Unknown
random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "+")
@0: The cat visits the dog.[(triple1)] The dog is red.[(triple2)] The lion is kind.[(triple3)] The mouse is nice.[(triple4)]
The cat visits the dog.
("cat" "visits" "dog" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4