The bear is round. The bear likes the dog. The bear likes the lion. The bear sees the dog. The bear sees the lion. The bear visits the lion. The dog likes the lion. The dog sees the bear. The dog sees the lion. The dog visits the lion. The lion is green. The lion is kind. The lion likes the bear. The lion likes the dog. The lion sees the bear. If the dog is green and the dog likes the lion then the lion is blue. If someone is round and green then they visit the bear. If someone visits the lion then they visit the dog. If someone visits the dog and they are blue then the dog is blue. If someone is round then they see the bear. If the bear is round then the bear likes the lion.
The bear is round.
("bear" "is" "round" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
If the dog is green and the dog likes the lion then the lion is blue.
((("dog" "is" "green" "+") ("dog" "likes" "lion" "+")) -> ("lion" "is" "blue" "+"))
If someone is round and green then they visit the bear.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "visits" "bear" "+"))
If someone visits the lion then they visit the dog.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the dog and they are blue then the dog is blue.
((("someone" "visits" "dog" "+") ("someone" "is" "blue" "+")) -> ("dog" "is" "blue" "+"))
If someone is round then they see the bear.
((("someone" "is" "round" "+")) -> ("someone" "sees" "bear" "+"))
If the bear is round then the bear likes the lion.
((("bear" "is" "round" "+")) -> ("bear" "likes" "lion" "+"))
The bear visits the lion.
True
1
proof
[(triple6)]
("bear" "visits" "lion" "+")
triple6
The lion does not like the bear.
False
1
inv-proof
[(triple13)]
("lion" "likes" "bear" "-")
triple13
The dog visits the dog.
True
2
proof
[(((triple10) -> rule3))]
("dog" "visits" "dog" "+")
((triple10) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The bear does not see the bear.
False
2
inv-proof
[(((triple1) -> rule5))]
("bear" "sees" "bear" "-")
((triple1) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The lion does not visit the dog.
Unknown
inv-rconc
[@1: The lion visits the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "dog" "-")
The lion is blue.
Unknown
rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "blue" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The bear is round.[(triple1)] The bear likes the dog.[(triple2)] The bear likes the lion.[(triple3 OR ((triple1) -> rule6))] The bear sees the dog.[(triple4)] The bear sees the lion.[(triple5)] The bear visits the lion.[(triple6)] The dog likes the lion.[(triple7)] The dog sees the bear.[(triple8)] The dog sees the lion.[(triple9)] The dog visits the lion.[(triple10)] The lion is green.[(triple11)] The lion is kind.[(triple12)] The lion likes the bear.[(triple13)] The lion likes the dog.[(triple14)] The lion sees the bear.[(triple15)] @1: The bear sees the bear.[(((triple1) -> rule5))] The bear visits the dog.[(((triple6) -> rule3))] The dog visits the dog.[(((triple10) -> rule3))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear likes the dog.
("bear" "likes" "dog" "+")
triple2
The bear likes the lion.
("bear" "likes" "lion" "+")
triple3
((triple1) -> (rule6 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple4
The bear sees the lion.
("bear" "sees" "lion" "+")
triple5
The bear visits the lion.
("bear" "visits" "lion" "+")
triple6
The dog likes the lion.
("dog" "likes" "lion" "+")
triple7
The dog sees the bear.
("dog" "sees" "bear" "+")
triple8
The dog sees the lion.
("dog" "sees" "lion" "+")
triple9
The dog visits the lion.
("dog" "visits" "lion" "+")
triple10
The lion is green.
("lion" "is" "green" "+")
triple11
The lion is kind.
("lion" "is" "kind" "+")
triple12
The lion likes the bear.
("lion" "likes" "bear" "+")
triple13
The lion likes the dog.
("lion" "likes" "dog" "+")
triple14
The lion sees the bear.
("lion" "sees" "bear" "+")
triple15
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple1) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
((triple6) -> (rule3 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple10) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1