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