The lion is young. The lion likes the rabbit. The lion needs the squirrel. The lion visits the squirrel. The rabbit is kind. The rabbit needs the lion. The rabbit does not visit the squirrel. The squirrel is big. The squirrel is not young. The squirrel does not like the lion. The squirrel likes the rabbit. The squirrel needs the lion. If someone visits the squirrel then they like the lion.
The lion is young.
("lion" "is" "young" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit does not visit the squirrel.
("rabbit" "visits" "squirrel" "-")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is not young.
("squirrel" "is" "young" "-")
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If someone visits the squirrel then they like the lion.
((("someone" "visits" "squirrel" "+")) -> ("someone" "likes" "lion" "+"))
The squirrel needs the lion.
True
1
proof
[(triple12)]
("squirrel" "needs" "lion" "+")
triple12
The rabbit is not kind.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "kind" "-")
triple5
The lion likes the lion.
True
2
proof
[(((triple4) -> rule1))]
("lion" "likes" "lion" "+")
((triple4) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not like the lion.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "likes" "lion" "-")
((triple4) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The rabbit does not like the lion.
Unknown
inv-rconc
[@1: The rabbit likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "lion" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The lion is young.[(triple1)] The lion likes the rabbit.[(triple2)] The lion needs the squirrel.[(triple3)] The lion visits the squirrel.[(triple4)] The rabbit does not visit the squirrel.[(triple7)] The rabbit is kind.[(triple5)] The rabbit needs the lion.[(triple6)] The squirrel does not like the lion.[(triple10)] The squirrel is big.[(triple8)] The squirrel is not young.[(triple9)] The squirrel likes the rabbit.[(triple11)] The squirrel needs the lion.[(triple12)] @1: The lion likes the lion.[(((triple4) -> rule1))]
The lion is young.
("lion" "is" "young" "+")
triple1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple4
The rabbit does not visit the squirrel.
("rabbit" "visits" "squirrel" "-")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple6
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
triple10
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel is not young.
("squirrel" "is" "young" "-")
triple9
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple11
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple12
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple4) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1