The lion eats the squirrel. The lion is not young. The lion needs the squirrel. The rabbit is kind. The rabbit is nice. The rabbit needs the lion. The squirrel is kind. If the lion needs the rabbit then the rabbit is nice. If someone needs the lion then the lion is not big. If someone is young then they need the lion. If someone is nice and not rough then they need the squirrel. If someone needs the squirrel and they are not big then they do not eat the rabbit. If someone is rough then they eat the rabbit. If someone is kind and they do not eat the rabbit then they see the lion. If someone sees the rabbit and they do not eat the rabbit then the rabbit sees the squirrel.
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If the lion needs the rabbit then the rabbit is nice.
((("lion" "needs" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If someone needs the lion then the lion is not big.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "big" "-"))
If someone is young then they need the lion.
((("someone" "is" "young" "+")) -> ("someone" "needs" "lion" "+"))
If someone is nice and not rough then they need the squirrel.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "~")) -> ("someone" "needs" "squirrel" "+"))
If someone needs the squirrel and they are not big then they do not eat the rabbit.
((("someone" "needs" "squirrel" "+") ("someone" "is" "big" "~")) -> ("someone" "eats" "rabbit" "-"))
If someone is rough then they eat the rabbit.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is kind and they do not eat the rabbit then they see the lion.
((("someone" "is" "kind" "+") ("someone" "eats" "rabbit" "~")) -> ("someone" "sees" "lion" "+"))
If someone sees the rabbit and they do not eat the rabbit then the rabbit sees the squirrel.
((("someone" "sees" "rabbit" "+") ("someone" "eats" "rabbit" "~")) -> ("rabbit" "sees" "squirrel" "+"))
The rabbit needs the lion.
True
1
proof
[(triple6)]
("rabbit" "needs" "lion" "+")
triple6
The squirrel is not kind.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "kind" "-")
triple7
The lion is not big.
True
2
proof
[(((triple6) -> rule2))]
("lion" "is" "big" "-")
((triple6) -> (rule2 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The lion is big.
False
2
inv-proof
[(((triple6) -> rule2))]
("lion" "is" "big" "+")
((triple6) -> (rule2 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The lion does not eat the rabbit.
True
4
proof
[(((triple3 ((triple6) -> rule2)) -> rule5))]
("lion" "eats" "rabbit" "-")
((triple3 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
int1
The lion is not big.
("lion" "is" "big" "-")
int2
The lion eats the rabbit.
False
4
inv-proof
[(((triple3 ((triple6) -> rule2)) -> rule5))]
("lion" "eats" "rabbit" "+")
((triple3 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
int1
The lion is not big.
("lion" "is" "big" "-")
int2
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "lion" "-")
The squirrel sees the lion.
Unknown
rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "sees" "lion" "+")
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The lion eats the squirrel.[(triple1)] The lion is not young.[(triple2)] The lion needs the squirrel.[(triple3)] The rabbit is kind.[(triple4)] The rabbit is nice.[(triple5)] The rabbit needs the lion.[(triple6)] The squirrel is kind.[(triple7)] @1: The lion is not big.[(((triple6) -> rule2))] @2: The lion does not eat the rabbit.[(((triple3 ((triple6) -> rule2)) -> rule5))]
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple1
The lion is not young.
("lion" "is" "young" "-")
triple2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple5
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple6
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple7
The lion is not big.
("lion" "is" "big" "-")
((triple6) -> (rule2 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
((triple3 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
int1
The lion is not big.
("lion" "is" "big" "-")
int2