The bear is young. The bear visits the cow. The bear visits the lion. The cow sees the bear. The lion is young. The lion likes the bear. The lion visits the cow. The rabbit is green. The rabbit likes the cow. The rabbit visits the lion. If someone likes the lion then the lion visits the rabbit. If someone is red then they like the lion. If someone is green then they are red.
The bear is young.
("bear" "is" "young" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone likes the lion then the lion visits the rabbit.
((("someone" "likes" "lion" "+")) -> ("lion" "visits" "rabbit" "+"))
If someone is red then they like the lion.
((("someone" "is" "red" "+")) -> ("someone" "likes" "lion" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
The rabbit is green.
True
1
proof
[(triple8)]
("rabbit" "is" "green" "+")
triple8
The rabbit is not green.
False
1
inv-proof
[(triple8)]
("rabbit" "is" "green" "-")
triple8
The rabbit is red.
True
2
proof
[(((triple8) -> rule3))]
("rabbit" "is" "red" "+")
((triple8) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple8) -> rule3))]
("rabbit" "is" "red" "-")
((triple8) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit likes the lion.
True
3
proof
[(((((triple8) -> rule3)) -> rule2))]
("rabbit" "likes" "lion" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit does not like the lion.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule2))]
("rabbit" "likes" "lion" "-")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The lion visits the rabbit.
True
4
proof
[(((((((triple8) -> rule3)) -> rule2)) -> rule1))]
("lion" "visits" "rabbit" "+")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The lion does not visit the rabbit.
False
4
inv-proof
[(((((((triple8) -> rule3)) -> rule2)) -> rule1))]
("lion" "visits" "rabbit" "-")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The bear does not like the lion.
Unknown
inv-rconc
[@2: The bear likes the lion.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("bear" "likes" "lion" "-")
The lion likes the lion.
Unknown
rconc
[@2: The lion likes the lion.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("lion" "likes" "lion" "+")
The cow does not like the lion.
Unknown
inv-rconc
[@2: The cow likes the lion.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("cow" "likes" "lion" "-")
The bear is red.
Unknown
rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "red" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The rabbit sees the bear.
Unknown
random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The bear sees the cow.
Unknown
random
[@0: The bear sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cow" "+")
@0: The bear is young.[(triple1)] The bear visits the cow.[(triple2)] The bear visits the lion.[(triple3)] The cow sees the bear.[(triple4)] The lion is young.[(triple5)] The lion likes the bear.[(triple6)] The lion visits the cow.[(triple7)] The rabbit is green.[(triple8)] The rabbit likes the cow.[(triple9)] The rabbit visits the lion.[(triple10)] @1: The rabbit is red.[(((triple8) -> rule3))] @2: The rabbit likes the lion.[(((((triple8) -> rule3)) -> rule2))] @3: The lion visits the rabbit.[(((((((triple8) -> rule3)) -> rule2)) -> rule1))]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear visits the cow.
("bear" "visits" "cow" "+")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple3
The cow sees the bear.
("cow" "sees" "bear" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion likes the bear.
("lion" "likes" "bear" "+")
triple6
The lion visits the cow.
("lion" "visits" "cow" "+")
triple7
The rabbit is green.
("rabbit" "is" "green" "+")
triple8
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple9
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
((triple8) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3