The rabbit is red. The squirrel chases the rabbit. If someone eats the squirrel then they are red. If the squirrel chases the rabbit then the rabbit sees the squirrel. If the squirrel chases the rabbit and the rabbit does not see the squirrel then the squirrel does not see the rabbit. If someone sees the squirrel then the squirrel sees the rabbit. If someone sees the rabbit then they eat the rabbit. If someone is red and not kind then they eat the rabbit.
The rabbit is red.
("rabbit" "is" "red" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
If someone eats the squirrel then they are red.
((("someone" "eats" "squirrel" "+")) -> ("someone" "is" "red" "+"))
If the squirrel chases the rabbit then the rabbit sees the squirrel.
((("squirrel" "chases" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If the squirrel chases the rabbit and the rabbit does not see the squirrel then the squirrel does not see the rabbit.
((("squirrel" "chases" "rabbit" "+") ("rabbit" "sees" "squirrel" "~")) -> ("squirrel" "sees" "rabbit" "-"))
If someone sees the squirrel then the squirrel sees the rabbit.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "rabbit" "+"))
If someone sees the rabbit then they eat the rabbit.
((("someone" "sees" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is red and not kind then they eat the rabbit.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "eats" "rabbit" "+"))
The squirrel chases the rabbit.
True
1
proof
[(triple2)]
("squirrel" "chases" "rabbit" "+")
triple2
The rabbit is not red.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "red" "-")
triple1
The rabbit sees the squirrel.
True
2
proof
[(((triple2) -> rule2))]
("rabbit" "sees" "squirrel" "+")
((triple2) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit does not see the squirrel.
False
2
inv-proof
[(((triple2) -> rule2))]
("rabbit" "sees" "squirrel" "-")
((triple2) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel sees the rabbit.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("squirrel" "sees" "rabbit" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel does not see the rabbit.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("squirrel" "sees" "rabbit" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel eats the rabbit.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule5))]
("squirrel" "eats" "rabbit" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel does not eat the rabbit.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule5))]
("squirrel" "eats" "rabbit" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "red" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit chases the squirrel.
Unknown
random
[@0: The rabbit chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "squirrel" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit eats the squirrel.
Unknown
random
[@0: The rabbit eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "squirrel" "+")
@0: The rabbit is red.[(triple1)] The squirrel chases the rabbit.[(triple2)] @1: The rabbit sees the squirrel.[(((triple2) -> rule2))] @2: The squirrel sees the rabbit.[(((((triple2) -> rule2)) -> rule4))] @3: The squirrel eats the rabbit.[(((((((triple2) -> rule2)) -> rule4)) -> rule5))]
The rabbit is red.
("rabbit" "is" "red" "+")
triple1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple2) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3