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