The dog eats the tiger. The dog is green. The tiger visits the dog. If the dog eats the tiger and the dog sees the tiger then the tiger sees the dog. If someone sees the tiger and the tiger visits the dog then the dog is rough. If the tiger sees the dog and the dog is nice then the tiger is nice.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is green.
("dog" "is" "green" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If the dog eats the tiger and the dog sees the tiger then the tiger sees the dog.
((("dog" "eats" "tiger" "+") ("dog" "sees" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If someone sees the tiger and the tiger visits the dog then the dog is rough.
((("someone" "sees" "tiger" "+") ("tiger" "visits" "dog" "+")) -> ("dog" "is" "rough" "+"))
If the tiger sees the dog and the dog is nice then the tiger is nice.
((("tiger" "sees" "dog" "+") ("dog" "is" "nice" "+")) -> ("tiger" "is" "nice" "+"))
The dog eats the tiger.
True
1
proof
[(triple1)]
("dog" "eats" "tiger" "+")
triple1
The tiger does not visit the dog.
False
1
inv-proof
[(triple3)]
("tiger" "visits" "dog" "-")
triple3
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "nice" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The dog eats the tiger.[(triple1)] The dog is green.[(triple2)] The tiger visits the dog.[(triple3)]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple3