The bear is red. The bear likes the cat. The bear needs the cat. The bear sees the cat. The cat is not big. The cat does not need the bear. The cat sees the bear. If the cat does not like the bear then the cat is nice. If someone sees the bear and they are not red then the bear is green.
The bear is red.
("bear" "is" "red" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat is not big.
("cat" "is" "big" "-")
The cat does not need the bear.
("cat" "needs" "bear" "-")
The cat sees the bear.
("cat" "sees" "bear" "+")
If the cat does not like the bear then the cat is nice.
((("cat" "likes" "bear" "~")) -> ("cat" "is" "nice" "+"))
If someone sees the bear and they are not red then the bear is green.
((("someone" "sees" "bear" "+") ("someone" "is" "red" "~")) -> ("bear" "is" "green" "+"))
The bear likes the cat.
True
1
proof
[(triple2)]
("bear" "likes" "cat" "+")
triple2
The cat is big.
False
1
inv-proof
[(triple5)]
("cat" "is" "big" "+")
triple5
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 sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is red.[(triple1)] The bear likes the cat.[(triple2)] The bear needs the cat.[(triple3)] The bear sees the cat.[(triple4)] The cat does not need the bear.[(triple6)] The cat is not big.[(triple5)] The cat sees the bear.[(triple7)]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
The bear needs the cat.
("bear" "needs" "cat" "+")
triple3
The bear sees the cat.
("bear" "sees" "cat" "+")
triple4
The cat does not need the bear.
("cat" "needs" "bear" "-")
triple6
The cat is not big.
("cat" "is" "big" "-")
triple5
The cat sees the bear.
("cat" "sees" "bear" "+")
triple7