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