The bear chases the tiger. The bear is rough. The bear likes the dog. The dog is green. The dog needs the lion. The lion likes the bear. The lion needs the bear. The tiger chases the bear. The tiger chases the dog. The tiger likes the lion. If something chases the bear and the bear likes the lion then the bear needs the lion. If something chases the bear then it is blue. If the lion likes the tiger then the tiger needs the lion.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If something chases the bear and the bear likes the lion then the bear needs the lion.
((("something" "chases" "bear" "+") ("bear" "likes" "lion" "+")) -> ("bear" "needs" "lion" "+"))
If something chases the bear then it is blue.
((("something" "chases" "bear" "+")) -> ("something" "is" "blue" "+"))
If the lion likes the tiger then the tiger needs the lion.
((("lion" "likes" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
The tiger chases the dog.
True
1
proof
[(triple9)]
("tiger" "chases" "dog" "+")
triple9
The bear is not rough.
False
1
inv-proof
[(triple2)]
("bear" "is" "rough" "-")
triple2
The tiger is blue.
True
2
proof
[(((triple8) -> rule2))]
("tiger" "is" "blue" "+")
((triple8) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple8) -> rule2))]
("tiger" "is" "blue" "-")
((triple8) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger does not need the lion.
Unknown
inv-rconc
[@1: The tiger needs the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "lion" "-")
The lion is blue.
Unknown
rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "blue" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear chases the tiger.[(triple1)] The bear is rough.[(triple2)] The bear likes the dog.[(triple3)] The dog is green.[(triple4)] The dog needs the lion.[(triple5)] The lion likes the bear.[(triple6)] The lion needs the bear.[(triple7)] The tiger chases the bear.[(triple8)] The tiger chases the dog.[(triple9)] The tiger likes the lion.[(triple10)] @1: The tiger is blue.[(((triple8) -> rule2))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear likes the dog.
("bear" "likes" "dog" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
The dog needs the lion.
("dog" "needs" "lion" "+")
triple5
The lion likes the bear.
("lion" "likes" "bear" "+")
triple6
The lion needs the bear.
("lion" "needs" "bear" "+")
triple7
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple8
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple9
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
((triple8) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1