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