The bear visits the cat. The cat likes the bear. The lion visits the cat. If someone is red then they like the cat. All blue people are red. If the cat is rough and the cat visits the lion then the lion visits the cat. If the lion visits the cat then the lion is blue. If someone is blue then they visit the bear. If someone is blue and they visit the cat then they visit the bear.
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone is red then they like the cat.
((("someone" "is" "red" "+")) -> ("someone" "likes" "cat" "+"))
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If the cat is rough and the cat visits the lion then the lion visits the cat.
((("cat" "is" "rough" "+") ("cat" "visits" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If the lion visits the cat then the lion is blue.
((("lion" "visits" "cat" "+")) -> ("lion" "is" "blue" "+"))
If someone is blue then they visit the bear.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "bear" "+"))
If someone is blue and they visit the cat then they visit the bear.
((("someone" "is" "blue" "+") ("someone" "visits" "cat" "+")) -> ("someone" "visits" "bear" "+"))
The lion visits the cat.
True
1
proof
[(triple3)]
("lion" "visits" "cat" "+")
triple3
The cat does not like the bear.
False
1
inv-proof
[(triple2)]
("cat" "likes" "bear" "-")
triple2
The lion is blue.
True
2
proof
[(((triple3) -> rule4))]
("lion" "is" "blue" "+")
((triple3) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple3) -> rule4))]
("lion" "is" "blue" "-")
((triple3) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is red.
True
3
proof
[(((((triple3) -> rule4)) -> rule2))]
("lion" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is not red.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule2))]
("lion" "is" "red" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the cat.
True
4
proof
[(((((((triple3) -> rule4)) -> rule2)) -> rule1))]
("lion" "likes" "cat" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion does not like the cat.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule2)) -> rule1))]
("lion" "likes" "cat" "-")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "bear" "-")
The bear is red.
Unknown
rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "red" "+")
The cat does not like the cat.
Unknown
inv-rconc
[@2: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("cat" "likes" "cat" "-")
The cat visits the bear.
Unknown
rconc
[@1: The cat visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The lion likes the bear.
Unknown
random
[@0: The lion likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "bear" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear visits the cat.[(triple1)] The cat likes the bear.[(triple2)] The lion visits the cat.[(triple3)] @1: The lion is blue.[(((triple3) -> rule4))] @2: The lion is red.[(((((triple3) -> rule4)) -> rule2))] The lion visits the bear.[(((((triple3) -> rule4)) -> rule5) OR ((((triple3) -> rule4) triple3) -> rule6))] @3: The lion likes the cat.[(((((((triple3) -> rule4)) -> rule2)) -> rule1))]
The bear visits the cat.
("bear" "visits" "cat" "+")
triple1
The cat likes the bear.
("cat" "likes" "bear" "+")
triple2
The lion visits the cat.
("lion" "visits" "cat" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
((triple3) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple3) -> (rule4 % int2)) triple3) -> (rule6 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the cat.
("lion" "likes" "cat" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3