The bear does not chase the lion. The bear likes the lion. The bear likes the mouse. The bear does not visit the lion. The lion chases the mouse. The lion is cold. The lion is not rough. The lion does not like the bear. The lion likes the mouse. The lion visits the bear. The lion visits the mouse. The mouse is not green. The mouse is round. The mouse likes the lion. The mouse visits the bear. The mouse does not visit the lion. If someone is round then they visit the bear. If someone likes the bear then the bear does not chase the mouse.
The bear does not chase the lion.
("bear" "chases" "lion" "-")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear does not visit the lion.
("bear" "visits" "lion" "-")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is not rough.
("lion" "is" "rough" "-")
The lion does not like the bear.
("lion" "likes" "bear" "-")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
If someone is round then they visit the bear.
((("someone" "is" "round" "+")) -> ("someone" "visits" "bear" "+"))
If someone likes the bear then the bear does not chase the mouse.
((("someone" "likes" "bear" "+")) -> ("bear" "chases" "mouse" "-"))
The mouse likes the lion.
True
1
proof
[(triple14)]
("mouse" "likes" "lion" "+")
triple14
The mouse is green.
False
1
inv-proof
[(triple12)]
("mouse" "is" "green" "+")
triple12
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "bear" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear does not chase the lion.[(triple1)] The bear does not visit the lion.[(triple4)] The bear likes the lion.[(triple2)] The bear likes the mouse.[(triple3)] The lion chases the mouse.[(triple5)] The lion does not like the bear.[(triple8)] The lion is cold.[(triple6)] The lion is not rough.[(triple7)] The lion likes the mouse.[(triple9)] The lion visits the bear.[(triple10)] The lion visits the mouse.[(triple11)] The mouse does not visit the lion.[(triple16)] The mouse is not green.[(triple12)] The mouse is round.[(triple13)] The mouse likes the lion.[(triple14)] The mouse visits the bear.[(triple15 OR ((triple13) -> rule1))]
The bear does not chase the lion.
("bear" "chases" "lion" "-")
triple1
The bear does not visit the lion.
("bear" "visits" "lion" "-")
triple4
The bear likes the lion.
("bear" "likes" "lion" "+")
triple2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple5
The lion does not like the bear.
("lion" "likes" "bear" "-")
triple8
The lion is cold.
("lion" "is" "cold" "+")
triple6
The lion is not rough.
("lion" "is" "rough" "-")
triple7
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple9
The lion visits the bear.
("lion" "visits" "bear" "+")
triple10
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple11
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
triple16
The mouse is not green.
("mouse" "is" "green" "-")
triple12
The mouse is round.
("mouse" "is" "round" "+")
triple13
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple14
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple15
((triple13) -> (rule1 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1