The bear likes the cat. The cat eats the bear. If someone is big then they do not like the bear. If someone is rough then they like the bear. If someone is big and not red then they like the bear. If the cat does not eat the bear then the cat sees the bear. If someone likes the bear then the bear is not rough. If the cat sees the bear then the bear sees the cat.
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
If someone is big then they do not like the bear.
((("someone" "is" "big" "+")) -> ("someone" "likes" "bear" "-"))
If someone is rough then they like the bear.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "bear" "+"))
If someone is big and not red then they like the bear.
((("someone" "is" "big" "+") ("someone" "is" "red" "~")) -> ("someone" "likes" "bear" "+"))
If the cat does not eat the bear then the cat sees the bear.
((("cat" "eats" "bear" "~")) -> ("cat" "sees" "bear" "+"))
If someone likes the bear then the bear is not rough.
((("someone" "likes" "bear" "+")) -> ("bear" "is" "rough" "-"))
If the cat sees the bear then the bear sees the cat.
((("cat" "sees" "bear" "+")) -> ("bear" "sees" "cat" "+"))
The cat eats the bear.
True
1
proof
[(triple2)]
("cat" "eats" "bear" "+")
triple2
The bear does not like the cat.
False
1
inv-proof
[(triple1)]
("bear" "likes" "cat" "-")
triple1
The bear does not see the cat.
Unknown
inv-rconc
[@2: The bear sees the cat.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("bear" "sees" "cat" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear likes the cat.[(triple1)] The cat eats the bear.[(triple2)]
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The cat eats the bear.
("cat" "eats" "bear" "+")
triple2