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