The bear is green. The lion needs the mouse. The mouse eats the lion. The rabbit is blue. If someone eats the lion then the lion is green. If someone needs the mouse and the mouse is big then the mouse eats the lion. If someone eats the lion and they do not need the mouse then they see the rabbit. If someone is nice then they need the rabbit. If someone sees the bear then the bear eats the rabbit. If someone needs the mouse then they do not eat the rabbit. If someone eats the lion then they see the lion. If someone is nice then they see the mouse.
The bear is green.
("bear" "is" "green" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
If someone eats the lion then the lion is green.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If someone needs the mouse and the mouse is big then the mouse eats the lion.
((("someone" "needs" "mouse" "+") ("mouse" "is" "big" "+")) -> ("mouse" "eats" "lion" "+"))
If someone eats the lion and they do not need the mouse then they see the rabbit.
((("someone" "eats" "lion" "+") ("someone" "needs" "mouse" "~")) -> ("someone" "sees" "rabbit" "+"))
If someone is nice then they need the rabbit.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone sees the bear then the bear eats the rabbit.
((("someone" "sees" "bear" "+")) -> ("bear" "eats" "rabbit" "+"))
If someone needs the mouse then they do not eat the rabbit.
((("someone" "needs" "mouse" "+")) -> ("someone" "eats" "rabbit" "-"))
If someone eats the lion then they see the lion.
((("someone" "eats" "lion" "+")) -> ("someone" "sees" "lion" "+"))
If someone is nice then they see the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "mouse" "+"))
The mouse eats the lion.
True
1
proof
[(triple3)]
("mouse" "eats" "lion" "+")
triple3
The bear is not green.
False
1
inv-proof
[(triple1)]
("bear" "is" "green" "-")
triple1
The lion is green.
True
2
proof
[(((triple3) -> rule1))]
("lion" "is" "green" "+")
((triple3) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion eats the rabbit.
False
2
inv-proof
[(((triple2) -> rule6))]
("lion" "eats" "rabbit" "+")
((triple2) -> (rule6 % int1))
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
int1
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The bear needs the rabbit.
Unknown
rconc
[@1: The bear needs the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "needs" "rabbit" "+")
The lion does not see the bear.
Unknown
inv-random
[@0: The lion sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bear" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
@0: The bear is green.[(triple1)] The lion needs the mouse.[(triple2)] The mouse eats the lion.[(triple3)] The rabbit is blue.[(triple4)] @1: The lion does not eat the rabbit.[(((triple2) -> rule6))] The lion is green.[(((triple3) -> rule1))] The mouse sees the lion.[(((triple3) -> rule7))]
The bear is green.
("bear" "is" "green" "+")
triple1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
((triple2) -> (rule6 % int1))
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
int1
The lion is green.
("lion" "is" "green" "+")
((triple3) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((triple3) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1