The rabbit is red. The rabbit sees the squirrel. The squirrel chases the rabbit. The squirrel eats the rabbit. The squirrel is cold. The squirrel is red. The squirrel sees the rabbit. If someone sees the rabbit then they eat the squirrel. If someone chases the squirrel and the squirrel eats the rabbit then they eat the rabbit. If the squirrel eats the rabbit then the squirrel sees the rabbit.
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone sees the rabbit then they eat the squirrel.
((("someone" "sees" "rabbit" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone chases the squirrel and the squirrel eats the rabbit then they eat the rabbit.
((("someone" "chases" "squirrel" "+") ("squirrel" "eats" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
If the squirrel eats the rabbit then the squirrel sees the rabbit.
((("squirrel" "eats" "rabbit" "+")) -> ("squirrel" "sees" "rabbit" "+"))
The squirrel is red.
True
1
proof
[(triple6)]
("squirrel" "is" "red" "+")
triple6
The squirrel does not see the rabbit.
False
1
inv-proof
[(triple7 OR ((triple4) -> rule3))]
("squirrel" "sees" "rabbit" "-")
triple7
((triple4) -> (rule3 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel eats the squirrel.
True
2
proof
[(((triple7) -> rule1) OR ((((triple4) -> rule3)) -> rule1))]
("squirrel" "eats" "squirrel" "+")
((triple7) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The squirrel does not eat the squirrel.
False
2
inv-proof
[(((triple7) -> rule1) OR ((((triple4) -> rule3)) -> rule1))]
("squirrel" "eats" "squirrel" "-")
((triple7) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit does not eat the squirrel.
Unknown
inv-rconc
[@1: The rabbit eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "squirrel" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit chases the squirrel.
Unknown
random
[@0: The rabbit chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "squirrel" "+")
@0: The rabbit is red.[(triple1)] The rabbit sees the squirrel.[(triple2)] The squirrel chases the rabbit.[(triple3)] The squirrel eats the rabbit.[(triple4)] The squirrel is cold.[(triple5)] The squirrel is red.[(triple6)] The squirrel sees the rabbit.[(triple7 OR ((triple4) -> rule3))] @1: The squirrel eats the squirrel.[(((triple7) -> rule1) OR ((((triple4) -> rule3)) -> rule1))]
The rabbit is red.
("rabbit" "is" "red" "+")
triple1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple2
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple3
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple4
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple5
The squirrel is red.
("squirrel" "is" "red" "+")
triple6
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple7
((triple4) -> (rule3 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple7) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2