The bear is big. The bear is rough. The bear is round. The bear needs the mouse. The cat sees the cow. The cow is big. The cow is not round. The cow is young. The cow needs the bear. The cow needs the mouse. The cow sees the cat. The mouse needs the cow. The mouse sees the cat. The mouse visits the bear. The mouse visits the cat. The mouse visits the cow. If something needs the cow and it is big then the cow visits the bear. If something is cold and it does not visit the cow then the cow sees the bear.
The bear is big.
("bear" "is" "big" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is not round.
("cow" "is" "round" "-")
The cow is young.
("cow" "is" "young" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something needs the cow and it is big then the cow visits the bear.
((("something" "needs" "cow" "+") ("something" "is" "big" "+")) -> ("cow" "visits" "bear" "+"))
If something is cold and it does not visit the cow then the cow sees the bear.
((("something" "is" "cold" "+") ("something" "visits" "cow" "~")) -> ("cow" "sees" "bear" "+"))
The mouse visits the bear.
True
1
proof
[(triple14)]
("mouse" "visits" "bear" "+")
triple14
The bear is not rough.
False
1
inv-proof
[(triple2)]
("bear" "is" "rough" "-")
triple2
The cow does not see the bear.
Unknown
inv-rconc
[@1: The cow sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "bear" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear is big.[(triple1)] The bear is rough.[(triple2)] The bear is round.[(triple3)] The bear needs the mouse.[(triple4)] The cat sees the cow.[(triple5)] The cow is big.[(triple6)] The cow is not round.[(triple7)] The cow is young.[(triple8)] The cow needs the bear.[(triple9)] The cow needs the mouse.[(triple10)] The cow sees the cat.[(triple11)] The mouse needs the cow.[(triple12)] The mouse sees the cat.[(triple13)] The mouse visits the bear.[(triple14)] The mouse visits the cat.[(triple15)] The mouse visits the cow.[(triple16)]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple4
The cat sees the cow.
("cat" "sees" "cow" "+")
triple5
The cow is big.
("cow" "is" "big" "+")
triple6
The cow is not round.
("cow" "is" "round" "-")
triple7
The cow is young.
("cow" "is" "young" "+")
triple8
The cow needs the bear.
("cow" "needs" "bear" "+")
triple9
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple10
The cow sees the cat.
("cow" "sees" "cat" "+")
triple11
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple12
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple13
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple14
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple15
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple16