The mouse is cold. The squirrel sees the mouse. The tiger sees the squirrel. If someone needs the squirrel and the squirrel is not young then they do not chase the squirrel. If someone sees the mouse then they are not green. If someone needs the tiger then they see the tiger.
The mouse is cold.
("mouse" "is" "cold" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If someone needs the squirrel and the squirrel is not young then they do not chase the squirrel.
((("someone" "needs" "squirrel" "+") ("squirrel" "is" "young" "~")) -> ("someone" "chases" "squirrel" "-"))
If someone sees the mouse then they are not green.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "green" "-"))
If someone needs the tiger then they see the tiger.
((("someone" "needs" "tiger" "+")) -> ("someone" "sees" "tiger" "+"))
The mouse is cold.
True
1
proof
[(triple1)]
("mouse" "is" "cold" "+")
triple1
The tiger does not see the squirrel.
False
1
inv-proof
[(triple3)]
("tiger" "sees" "squirrel" "-")
triple3
The squirrel is not green.
True
2
proof
[(((triple2) -> rule2))]
("squirrel" "is" "green" "-")
((triple2) -> (rule2 % int1))
The squirrel is not green.
("squirrel" "is" "green" "-")
int1
The squirrel is green.
False
2
inv-proof
[(((triple2) -> rule2))]
("squirrel" "is" "green" "+")
((triple2) -> (rule2 % int1))
The squirrel is not green.
("squirrel" "is" "green" "-")
int1
The mouse does not see the tiger.
Unknown
inv-rconc
[@1: The mouse sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "tiger" "-")
The squirrel sees the tiger.
Unknown
rconc
[@1: The squirrel sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "tiger" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse chases the tiger.
Unknown
random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "+")
@0: The mouse is cold.[(triple1)] The squirrel sees the mouse.[(triple2)] The tiger sees the squirrel.[(triple3)] @1: The squirrel is not green.[(((triple2) -> rule2))]
The mouse is cold.
("mouse" "is" "cold" "+")
triple1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple3
The squirrel is not green.
("squirrel" "is" "green" "-")
((triple2) -> (rule2 % int1))
The squirrel is not green.
("squirrel" "is" "green" "-")
int1