The rabbit eats the squirrel. The rabbit is not cold. The squirrel eats the rabbit. The squirrel is nice. The squirrel is red. The squirrel needs the rabbit. The squirrel sees the rabbit. If something sees the rabbit and it does not eat the rabbit then the rabbit does not see the squirrel. If something needs the rabbit and the rabbit eats the squirrel then the rabbit sees the squirrel. If the rabbit is nice then the rabbit is red. If something eats the squirrel and it needs the rabbit then the squirrel sees the rabbit. If something eats the squirrel then it is kind. If the squirrel eats the rabbit and the squirrel does not see the rabbit then the squirrel is kind.
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If something sees the rabbit and it does not eat the rabbit then the rabbit does not see the squirrel.
((("something" "sees" "rabbit" "+") ("something" "eats" "rabbit" "~")) -> ("rabbit" "sees" "squirrel" "-"))
If something needs the rabbit and the rabbit eats the squirrel then the rabbit sees the squirrel.
((("something" "needs" "rabbit" "+") ("rabbit" "eats" "squirrel" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If the rabbit is nice then the rabbit is red.
((("rabbit" "is" "nice" "+")) -> ("rabbit" "is" "red" "+"))
If something eats the squirrel and it needs the rabbit then the squirrel sees the rabbit.
((("something" "eats" "squirrel" "+") ("something" "needs" "rabbit" "+")) -> ("squirrel" "sees" "rabbit" "+"))
If something eats the squirrel then it is kind.
((("something" "eats" "squirrel" "+")) -> ("something" "is" "kind" "+"))
If the squirrel eats the rabbit and the squirrel does not see the rabbit then the squirrel is kind.
((("squirrel" "eats" "rabbit" "+") ("squirrel" "sees" "rabbit" "~")) -> ("squirrel" "is" "kind" "+"))
The rabbit is not cold.
True
1
proof
[(triple2)]
("rabbit" "is" "cold" "-")
triple2
The rabbit does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("rabbit" "eats" "squirrel" "-")
triple1
The rabbit sees the squirrel.
True
3
proof
[(((triple6 triple1) -> rule2))]
("rabbit" "sees" "squirrel" "+")
((triple6 triple1) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit does not see the squirrel.
False
3
inv-proof
[(((triple6 triple1) -> rule2))]
("rabbit" "sees" "squirrel" "-")
((triple6 triple1) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "red" "-")
The squirrel is kind.
Unknown
rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "kind" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The rabbit eats the squirrel.[(triple1)] The rabbit is not cold.[(triple2)] The squirrel eats the rabbit.[(triple3)] The squirrel is nice.[(triple4)] The squirrel is red.[(triple5)] The squirrel needs the rabbit.[(triple6)] The squirrel sees the rabbit.[(triple7)] @1: The rabbit is kind.[(((triple1) -> rule5))] The rabbit sees the squirrel.[(((triple6 triple1) -> rule2))]
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple1
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple4
The squirrel is red.
("squirrel" "is" "red" "+")
triple5
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple6
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple1) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple6 triple1) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1