The dog is big. The dog needs the squirrel. The lion is green. The lion is kind. The lion sees the dog. The rabbit is young. The rabbit needs the squirrel. The rabbit visits the squirrel. The squirrel is big. The squirrel needs the dog. If someone needs the rabbit and they are young then the rabbit is kind. If the squirrel needs the dog then the squirrel needs the lion. If someone is big and they visit the squirrel then they are round. If someone needs the rabbit then the rabbit sees the lion. If someone needs the rabbit and the rabbit visits the lion then the rabbit is green. If someone visits the rabbit and they need the squirrel then the squirrel sees the lion. If the squirrel needs the dog and the squirrel does not see the dog then the squirrel sees the lion. If someone is green and not kind then they need the squirrel.
The dog is big.
("dog" "is" "big" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If someone needs the rabbit and they are young then the rabbit is kind.
((("someone" "needs" "rabbit" "+") ("someone" "is" "young" "+")) -> ("rabbit" "is" "kind" "+"))
If the squirrel needs the dog then the squirrel needs the lion.
((("squirrel" "needs" "dog" "+")) -> ("squirrel" "needs" "lion" "+"))
If someone is big and they visit the squirrel then they are round.
((("someone" "is" "big" "+") ("someone" "visits" "squirrel" "+")) -> ("someone" "is" "round" "+"))
If someone needs the rabbit then the rabbit sees the lion.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
If someone needs the rabbit and the rabbit visits the lion then the rabbit is green.
((("someone" "needs" "rabbit" "+") ("rabbit" "visits" "lion" "+")) -> ("rabbit" "is" "green" "+"))
If someone visits the rabbit and they need the squirrel then the squirrel sees the lion.
((("someone" "visits" "rabbit" "+") ("someone" "needs" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If the squirrel needs the dog and the squirrel does not see the dog then the squirrel sees the lion.
((("squirrel" "needs" "dog" "+") ("squirrel" "sees" "dog" "~")) -> ("squirrel" "sees" "lion" "+"))
If someone is green and not kind then they need the squirrel.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "needs" "squirrel" "+"))
The lion is green.
True
1
proof
[(triple3)]
("lion" "is" "green" "+")
triple3
The lion is not kind.
False
1
inv-proof
[(triple4)]
("lion" "is" "kind" "-")
triple4
The squirrel needs the lion.
True
2
proof
[(((triple10) -> rule2))]
("squirrel" "needs" "lion" "+")
((triple10) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel does not need the lion.
False
2
inv-proof
[(((triple10) -> rule2))]
("squirrel" "needs" "lion" "-")
((triple10) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The rabbit does not see the lion.
Unknown
inv-rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "lion" "-")
The squirrel is round.
Unknown
rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "round" "+")
The lion does not visit the dog.
Unknown
inv-random
[@0: The lion visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "dog" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The dog is big.[(triple1)] The dog needs the squirrel.[(triple2)] The lion is green.[(triple3)] The lion is kind.[(triple4)] The lion sees the dog.[(triple5)] The rabbit is young.[(triple6)] The rabbit needs the squirrel.[(triple7)] The rabbit visits the squirrel.[(triple8)] The squirrel is big.[(triple9)] The squirrel needs the dog.[(triple10)] @1: The squirrel needs the lion.[(((triple10) -> rule2))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
triple4
The lion sees the dog.
("lion" "sees" "dog" "+")
triple5
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple7
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple10
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((triple10) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1