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