The bear is kind. The lion likes the bear. If someone visits the bear then they need the lion. If the lion needs the bear then the lion likes the bear. If someone needs the lion then they are not kind. If the lion likes the bear and the bear likes the lion then the bear visits the lion. If someone likes the bear then they visit the bear. If the bear needs the lion then the lion does not need the bear. If someone likes the lion and they do not need the lion then the lion is green. If someone is kind and they do not visit the lion then they are not green.
The bear is kind.
("bear" "is" "kind" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
If someone visits the bear then they need the lion.
((("someone" "visits" "bear" "+")) -> ("someone" "needs" "lion" "+"))
If the lion needs the bear then the lion likes the bear.
((("lion" "needs" "bear" "+")) -> ("lion" "likes" "bear" "+"))
If someone needs the lion then they are not kind.
((("someone" "needs" "lion" "+")) -> ("someone" "is" "kind" "-"))
If the lion likes the bear and the bear likes the lion then the bear visits the lion.
((("lion" "likes" "bear" "+") ("bear" "likes" "lion" "+")) -> ("bear" "visits" "lion" "+"))
If someone likes the bear then they visit the bear.
((("someone" "likes" "bear" "+")) -> ("someone" "visits" "bear" "+"))
If the bear needs the lion then the lion does not need the bear.
((("bear" "needs" "lion" "+")) -> ("lion" "needs" "bear" "-"))
If someone likes the lion and they do not need the lion then the lion is green.
((("someone" "likes" "lion" "+") ("someone" "needs" "lion" "~")) -> ("lion" "is" "green" "+"))
If someone is kind and they do not visit the lion then they are not green.
((("someone" "is" "kind" "+") ("someone" "visits" "lion" "~")) -> ("someone" "is" "green" "-"))
The lion likes the bear.
True
1
proof
[(triple2)]
("lion" "likes" "bear" "+")
triple2
The bear is not kind.
False
1
inv-proof
[(triple1)]
("bear" "is" "kind" "-")
triple1
The lion visits the bear.
True
2
proof
[(((triple2) -> rule5))]
("lion" "visits" "bear" "+")
((triple2) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion does not visit the bear.
False
2
inv-proof
[(((triple2) -> rule5))]
("lion" "visits" "bear" "-")
((triple2) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion needs the lion.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("lion" "needs" "lion" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion does not need the lion.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("lion" "needs" "lion" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion is not kind.
True
4
proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
("lion" "is" "kind" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
int3
The lion is kind.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
("lion" "is" "kind" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
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 visits the lion.
Unknown
rconc
[@1: The bear visits the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "lion" "+")
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "is" "green" "-")
The bear needs the lion.
Unknown
rconc
[@2: The bear needs the lion.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("bear" "needs" "lion" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The bear likes the lion.
Unknown
random
[@0: The bear likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "lion" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The bear is kind.[(triple1)] The lion likes the bear.[(triple2)] @1: The lion visits the bear.[(((triple2) -> rule5))] @2: The lion needs the lion.[(((((triple2) -> rule5)) -> rule1))] @3: The lion is not kind.[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The lion likes the bear.
("lion" "likes" "bear" "+")
triple2
The lion visits the bear.
("lion" "visits" "bear" "+")
((triple2) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion is not kind.
("lion" "is" "kind" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
int3