The lion is big. The mouse sees the rabbit. The rabbit is red. The squirrel is red. If someone eats the mouse and the mouse sees the squirrel then the squirrel sees the rabbit. If someone is green then they chase the squirrel. If someone sees the rabbit then they are red. If someone is green then they do not eat the mouse. If someone eats the mouse and they are not kind then they do not chase the lion. If someone eats the lion then the lion is red.
The lion is big.
("lion" "is" "big" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
If someone eats the mouse and the mouse sees the squirrel then the squirrel sees the rabbit.
((("someone" "eats" "mouse" "+") ("mouse" "sees" "squirrel" "+")) -> ("squirrel" "sees" "rabbit" "+"))
If someone is green then they chase the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone sees the rabbit then they are red.
((("someone" "sees" "rabbit" "+")) -> ("someone" "is" "red" "+"))
If someone is green then they do not eat the mouse.
((("someone" "is" "green" "+")) -> ("someone" "eats" "mouse" "-"))
If someone eats the mouse and they are not kind then they do not chase the lion.
((("someone" "eats" "mouse" "+") ("someone" "is" "kind" "~")) -> ("someone" "chases" "lion" "-"))
If someone eats the lion then the lion is red.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "red" "+"))
The lion is big.
True
1
proof
[(triple1)]
("lion" "is" "big" "+")
triple1
The squirrel is not red.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "red" "-")
triple4
The mouse is red.
True
2
proof
[(((triple2) -> rule3))]
("mouse" "is" "red" "+")
((triple2) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is not red.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "is" "red" "-")
((triple2) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "red" "-")
The squirrel sees the rabbit.
Unknown
rconc
[@1: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "rabbit" "+")
The lion does not chase the mouse.
Unknown
inv-random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The lion is big.[(triple1)] The mouse sees the rabbit.[(triple2)] The rabbit is red.[(triple3)] The squirrel is red.[(triple4)] @1: The mouse is red.[(((triple2) -> rule3))]
The lion is big.
("lion" "is" "big" "+")
triple1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple2
The rabbit is red.
("rabbit" "is" "red" "+")
triple3
The squirrel is red.
("squirrel" "is" "red" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
((triple2) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1