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