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