The bear does not eat the mouse. The bear needs the rabbit. The mouse is kind. The mouse is not young. The rabbit sees the bear. The rabbit sees the mouse. The tiger is big. If someone is kind and not young then they do not see the tiger. If the rabbit needs the tiger and the rabbit does not eat the bear then the rabbit sees the mouse. If someone needs the mouse then the mouse sees the rabbit.
The bear does not eat the mouse.
("bear" "eats" "mouse" "-")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
If someone is kind and not young then they do not see the tiger.
((("someone" "is" "kind" "+") ("someone" "is" "young" "~")) -> ("someone" "sees" "tiger" "-"))
If the rabbit needs the tiger and the rabbit does not eat the bear then the rabbit sees the mouse.
((("rabbit" "needs" "tiger" "+") ("rabbit" "eats" "bear" "~")) -> ("rabbit" "sees" "mouse" "+"))
If someone needs the mouse then the mouse sees the rabbit.
((("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
The bear does not eat the mouse.
True
1
proof
[(triple1)]
("bear" "eats" "mouse" "-")
triple1
The tiger is not big.
False
1
inv-proof
[(triple7)]
("tiger" "is" "big" "-")
triple7
The mouse does not see the rabbit.
Unknown
inv-rconc
[@1: The mouse sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "rabbit" "-")
The rabbit eats the tiger.
Unknown
random
[@0: The rabbit eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "tiger" "+")
@0: The bear does not eat the mouse.[(triple1)] The bear needs the rabbit.[(triple2)] The mouse is kind.[(triple3)] The mouse is not young.[(triple4)] The rabbit sees the bear.[(triple5)] The rabbit sees the mouse.[(triple6)] The tiger is big.[(triple7)] @1: The mouse does not see the tiger.[(((triple3 triple4) -> rule1))]
The bear does not eat the mouse.
("bear" "eats" "mouse" "-")
triple1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse is not young.
("mouse" "is" "young" "-")
triple4
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple5
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
((triple3 triple4) -> (rule1 % int1))
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
int1