The dog needs the lion. The lion sees the squirrel. The squirrel is cold. If someone likes the lion and the lion needs the squirrel then they are nice. If someone likes the dog then the dog needs the squirrel. If someone is young and not kind then they see the lion. If someone likes the dog and they are not kind then they need the dog. If someone needs the squirrel then the squirrel is young. If someone sees the squirrel then the squirrel likes the dog.
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If someone likes the lion and the lion needs the squirrel then they are nice.
((("someone" "likes" "lion" "+") ("lion" "needs" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the dog then the dog needs the squirrel.
((("someone" "likes" "dog" "+")) -> ("dog" "needs" "squirrel" "+"))
If someone is young and not kind then they see the lion.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "sees" "lion" "+"))
If someone likes the dog and they are not kind then they need the dog.
((("someone" "likes" "dog" "+") ("someone" "is" "kind" "~")) -> ("someone" "needs" "dog" "+"))
If someone needs the squirrel then the squirrel is young.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "is" "young" "+"))
If someone sees the squirrel then the squirrel likes the dog.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "likes" "dog" "+"))
The squirrel is cold.
True
1
proof
[(triple3)]
("squirrel" "is" "cold" "+")
triple3
The lion does not see the squirrel.
False
1
inv-proof
[(triple2)]
("lion" "sees" "squirrel" "-")
triple2
The squirrel likes the dog.
True
2
proof
[(((triple2) -> rule6))]
("squirrel" "likes" "dog" "+")
((triple2) -> (rule6 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The squirrel does not like the dog.
False
2
inv-proof
[(((triple2) -> rule6))]
("squirrel" "likes" "dog" "-")
((triple2) -> (rule6 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The dog needs the squirrel.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("dog" "needs" "squirrel" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int2
The dog does not need the squirrel.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("dog" "needs" "squirrel" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int2
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "dog" "-")
The squirrel sees the lion.
Unknown
rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "lion" "+")
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "lion" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The dog needs the lion.[(triple1)] The lion sees the squirrel.[(triple2)] The squirrel is cold.[(triple3)] @1: The squirrel likes the dog.[(((triple2) -> rule6))] @2: The dog needs the squirrel.[(((((triple2) -> rule6)) -> rule2))] @3: The squirrel is young.[(((((((triple2) -> rule6)) -> rule2)) -> rule5))]
The dog needs the lion.
("dog" "needs" "lion" "+")
triple1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple2
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple3
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
((triple2) -> (rule6 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int2
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int3