The dog is nice. The dog is red. The dog likes the lion. The dog sees the lion. The dog sees the rabbit. The lion is green. The lion is nice. The lion is young. The lion likes the rabbit. The lion sees the dog. The lion visits the dog. The rabbit is young. The rabbit likes the lion. The rabbit sees the dog. The rabbit sees the lion. The rabbit visits the lion. If something visits the dog and it sees the dog then the dog is green. If the rabbit visits the lion then the rabbit sees the dog. If the rabbit sees the lion and the lion visits the rabbit then the rabbit likes the dog.
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something visits the dog and it sees the dog then the dog is green.
((("something" "visits" "dog" "+") ("something" "sees" "dog" "+")) -> ("dog" "is" "green" "+"))
If the rabbit visits the lion then the rabbit sees the dog.
((("rabbit" "visits" "lion" "+")) -> ("rabbit" "sees" "dog" "+"))
If the rabbit sees the lion and the lion visits the rabbit then the rabbit likes the dog.
((("rabbit" "sees" "lion" "+") ("lion" "visits" "rabbit" "+")) -> ("rabbit" "likes" "dog" "+"))
The lion is nice.
True
1
proof
[(triple7)]
("lion" "is" "nice" "+")
triple7
The dog is not red.
False
1
inv-proof
[(triple2)]
("dog" "is" "red" "-")
triple2
The rabbit does not like the dog.
Unknown
inv-rconc
[@1: The rabbit likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "dog" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
@0: The dog is nice.[(triple1)] The dog is red.[(triple2)] The dog likes the lion.[(triple3)] The dog sees the lion.[(triple4)] The dog sees the rabbit.[(triple5)] The lion is green.[(triple6)] The lion is nice.[(triple7)] The lion is young.[(triple8)] The lion likes the rabbit.[(triple9)] The lion sees the dog.[(triple10)] The lion visits the dog.[(triple11)] The rabbit is young.[(triple12)] The rabbit likes the lion.[(triple13)] The rabbit sees the dog.[(triple14 OR ((triple16) -> rule2))] The rabbit sees the lion.[(triple15)] The rabbit visits the lion.[(triple16)] @1: The dog is green.[(((triple11 triple10) -> rule1))]
The dog is nice.
("dog" "is" "nice" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog likes the lion.
("dog" "likes" "lion" "+")
triple3
The dog sees the lion.
("dog" "sees" "lion" "+")
triple4
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple5
The lion is green.
("lion" "is" "green" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The lion is young.
("lion" "is" "young" "+")
triple8
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple9
The lion sees the dog.
("lion" "sees" "dog" "+")
triple10
The lion visits the dog.
("lion" "visits" "dog" "+")
triple11
The rabbit is young.
("rabbit" "is" "young" "+")
triple12
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple13
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple14
((triple16) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple15
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple16
The dog is green.
("dog" "is" "green" "+")
((triple11 triple10) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1