The bear needs the mouse. The bear does not see the dog. The cat needs the dog. The dog is young. The dog likes the cat. The mouse does not need the cat. The mouse sees the cat. If someone is big then they like the cat. Big people are young.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear does not see the dog.
("bear" "sees" "dog" "-")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone is big then they like the cat.
((("someone" "is" "big" "+")) -> ("someone" "likes" "cat" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
The bear does not see the dog.
True
1
proof
[(triple2)]
("bear" "sees" "dog" "-")
triple2
The bear does not need the mouse.
False
1
inv-proof
[(triple1)]
("bear" "needs" "mouse" "-")
triple1
The bear does not like the cat.
Unknown
inv-rconc
[@1: The bear likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "cat" "-")
The mouse likes the dog.
Unknown
random
[@0: The mouse likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "dog" "+")
@0: The bear does not see the dog.[(triple2)] The bear needs the mouse.[(triple1)] The cat needs the dog.[(triple3)] The dog is young.[(triple4)] The dog likes the cat.[(triple5)] The mouse does not need the cat.[(triple6)] The mouse sees the cat.[(triple7)]
The bear does not see the dog.
("bear" "sees" "dog" "-")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog likes the cat.
("dog" "likes" "cat" "+")
triple5
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
triple6
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple7