The bear is big. The bear sees the rabbit. The mouse is big. The mouse is nice. The mouse sees the bear. The mouse sees the squirrel. The rabbit is nice. The rabbit is not rough. The rabbit sees the mouse. The squirrel eats the mouse. The squirrel does not eat the rabbit. The squirrel is nice. If someone is green and they do not like the mouse then they do not like the squirrel. If someone eats the squirrel then they eat the rabbit. If someone eats the mouse and the mouse sees the squirrel then they do not see the rabbit. If someone eats the mouse and they are nice then the mouse does not see the rabbit. If the bear does not like the mouse then the bear sees the mouse. If someone is green then they are nice.
The bear is big.
("bear" "is" "big" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is not rough.
("rabbit" "is" "rough" "-")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel does not eat the rabbit.
("squirrel" "eats" "rabbit" "-")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If someone is green and they do not like the mouse then they do not like the squirrel.
((("someone" "is" "green" "+") ("someone" "likes" "mouse" "~")) -> ("someone" "likes" "squirrel" "-"))
If someone eats the squirrel then they eat the rabbit.
((("someone" "eats" "squirrel" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone eats the mouse and the mouse sees the squirrel then they do not see the rabbit.
((("someone" "eats" "mouse" "+") ("mouse" "sees" "squirrel" "+")) -> ("someone" "sees" "rabbit" "-"))
If someone eats the mouse and they are nice then the mouse does not see the rabbit.
((("someone" "eats" "mouse" "+") ("someone" "is" "nice" "+")) -> ("mouse" "sees" "rabbit" "-"))
If the bear does not like the mouse then the bear sees the mouse.
((("bear" "likes" "mouse" "~")) -> ("bear" "sees" "mouse" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple9)]
("rabbit" "sees" "mouse" "+")
triple9
The mouse does not see the squirrel.
False
1
inv-proof
[(triple6)]
("mouse" "sees" "squirrel" "-")
triple6
The squirrel does not see the rabbit.
True
3
proof
[(((triple10 triple6) -> rule3))]
("squirrel" "sees" "rabbit" "-")
((triple10 triple6) -> (rule3 % int1))
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
int1
The mouse sees the rabbit.
False
3
inv-proof
[(((triple10 triple12) -> rule4))]
("mouse" "sees" "rabbit" "+")
((triple10 triple12) -> (rule4 % int1))
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
int1
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "nice" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The bear is big.[(triple1)] The bear sees the rabbit.[(triple2)] The mouse is big.[(triple3)] The mouse is nice.[(triple4)] The mouse sees the bear.[(triple5)] The mouse sees the squirrel.[(triple6)] The rabbit is nice.[(triple7)] The rabbit is not rough.[(triple8)] The rabbit sees the mouse.[(triple9)] The squirrel does not eat the rabbit.[(triple11)] The squirrel eats the mouse.[(triple10)] The squirrel is nice.[(triple12)] @1: The mouse does not see the rabbit.[(((triple10 triple12) -> rule4))] The squirrel does not see the rabbit.[(((triple10 triple6) -> rule3))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple5
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit is not rough.
("rabbit" "is" "rough" "-")
triple8
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple9
The squirrel does not eat the rabbit.
("squirrel" "eats" "rabbit" "-")
triple11
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple10
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple12
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
((triple10 triple12) -> (rule4 % int1))
The mouse does not see the rabbit.
("mouse" "sees" "rabbit" "-")
int1
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
((triple10 triple6) -> (rule3 % int1))
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
int1