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