The bear eats the lion. The bear eats the squirrel. The lion does not need the squirrel. The squirrel eats the bear. The squirrel needs the bear. The squirrel needs the lion. The squirrel visits the lion. If the squirrel is not young then the squirrel eats the bear. If the squirrel needs the lion then the lion is not kind. If someone needs the bear and the bear does not visit the lion then the bear eats the lion. If someone is round and they eat the squirrel then they eat the lion. If someone visits the bear and they need the squirrel then the squirrel is kind. If someone needs the lion and they do not visit the squirrel then the lion needs the bear.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The lion does not need the squirrel.
("lion" "needs" "squirrel" "-")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If the squirrel is not young then the squirrel eats the bear.
((("squirrel" "is" "young" "~")) -> ("squirrel" "eats" "bear" "+"))
If the squirrel needs the lion then the lion is not kind.
((("squirrel" "needs" "lion" "+")) -> ("lion" "is" "kind" "-"))
If someone needs the bear and the bear does not visit the lion then the bear eats the lion.
((("someone" "needs" "bear" "+") ("bear" "visits" "lion" "~")) -> ("bear" "eats" "lion" "+"))
If someone is round and they eat the squirrel then they eat the lion.
((("someone" "is" "round" "+") ("someone" "eats" "squirrel" "+")) -> ("someone" "eats" "lion" "+"))
If someone visits the bear and they need the squirrel then the squirrel is kind.
((("someone" "visits" "bear" "+") ("someone" "needs" "squirrel" "+")) -> ("squirrel" "is" "kind" "+"))
If someone needs the lion and they do not visit the squirrel then the lion needs the bear.
((("someone" "needs" "lion" "+") ("someone" "visits" "squirrel" "~")) -> ("lion" "needs" "bear" "+"))
The squirrel eats the bear.
True
1
proof
[(triple4)]
("squirrel" "eats" "bear" "+")
triple4
The lion needs the squirrel.
False
1
inv-proof
[(triple3)]
("lion" "needs" "squirrel" "+")
triple3
The lion is not kind.
True
2
proof
[(((triple6) -> rule2))]
("lion" "is" "kind" "-")
((triple6) -> (rule2 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The lion is kind.
False
2
inv-proof
[(((triple6) -> rule2))]
("lion" "is" "kind" "+")
((triple6) -> (rule2 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The lion does not need the bear.
Unknown
inv-rconc
[@1: The lion needs the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "needs" "bear" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "lion" "+")
The lion does not visit the bear.
Unknown
inv-random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The bear eats the lion.[(triple1)] The bear eats the squirrel.[(triple2)] The lion does not need the squirrel.[(triple3)] The squirrel eats the bear.[(triple4)] The squirrel needs the bear.[(triple5)] The squirrel needs the lion.[(triple6)] The squirrel visits the lion.[(triple7)] @1: The lion is not kind.[(((triple6) -> rule2))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple2
The lion does not need the squirrel.
("lion" "needs" "squirrel" "-")
triple3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple4
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple5
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple6
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple7
The lion is not kind.
("lion" "is" "kind" "-")
((triple6) -> (rule2 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1