The bear visits the lion. The cow visits the lion. The lion does not need the cow. If someone sees the bear and the bear is round then the bear does not need the lion. If someone needs the cow and they do not see the cow then they are young. If someone visits the lion then the lion is kind. If the lion is kind and the lion visits the cow then the cow sees the lion. If someone is kind then they need the lion. If someone needs the lion and the lion is kind then the lion is not rough. If the lion is rough then the lion does not visit the bear. If someone visits the bear and they need the bear then they visit the lion.
The bear visits the lion.
("bear" "visits" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion does not need the cow.
("lion" "needs" "cow" "-")
If someone sees the bear and the bear is round then the bear does not need the lion.
((("someone" "sees" "bear" "+") ("bear" "is" "round" "+")) -> ("bear" "needs" "lion" "-"))
If someone needs the cow and they do not see the cow then they are young.
((("someone" "needs" "cow" "+") ("someone" "sees" "cow" "~")) -> ("someone" "is" "young" "+"))
If someone visits the lion then the lion is kind.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "kind" "+"))
If the lion is kind and the lion visits the cow then the cow sees the lion.
((("lion" "is" "kind" "+") ("lion" "visits" "cow" "+")) -> ("cow" "sees" "lion" "+"))
If someone is kind then they need the lion.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the lion and the lion is kind then the lion is not rough.
((("someone" "needs" "lion" "+") ("lion" "is" "kind" "+")) -> ("lion" "is" "rough" "-"))
If the lion is rough then the lion does not visit the bear.
((("lion" "is" "rough" "+")) -> ("lion" "visits" "bear" "-"))
If someone visits the bear and they need the bear then they visit the lion.
((("someone" "visits" "bear" "+") ("someone" "needs" "bear" "+")) -> ("someone" "visits" "lion" "+"))
The bear visits the lion.
True
1
proof
[(triple1)]
("bear" "visits" "lion" "+")
triple1
The bear does not visit the lion.
False
1
inv-proof
[(triple1)]
("bear" "visits" "lion" "-")
triple1
The lion is kind.
True
2
proof
[(((triple1) -> rule3) OR ((triple2) -> rule3))]
("lion" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple2) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is not kind.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple2) -> rule3))]
("lion" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple2) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion needs the lion.
True
3
proof
[(((((triple1) -> rule3)) -> rule5) OR ((((triple2) -> rule3)) -> rule5))]
("lion" "needs" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5) OR ((((triple2) -> rule3)) -> rule5))]
("lion" "needs" "lion" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is not rough.
True
6
proof
[(((((((triple1) -> rule3)) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((((((triple1) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule6) OR ((((((triple2) -> rule3)) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule6))]
("lion" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is rough.
False
6
inv-proof
[(((((((triple1) -> rule3)) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((((((triple1) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule6) OR ((((((triple2) -> rule3)) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule6))]
("lion" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "young" "-")
The lion visits the lion.
Unknown
rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "visits" "lion" "+")
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "young" "-")
The cow sees the lion.
Unknown
rconc
[@1: The cow sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "sees" "lion" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The lion does not see the cow.
Unknown
inv-random
[@0: The lion sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cow" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The bear visits the lion.[(triple1)] The cow visits the lion.[(triple2)] The lion does not need the cow.[(triple3)] @1: The lion is kind.[(((triple1) -> rule3) OR ((triple2) -> rule3))] @2: The lion needs the lion.[(((((triple1) -> rule3)) -> rule5) OR ((((triple2) -> rule3)) -> rule5))] @3: The lion is not rough.[(((((((triple1) -> rule3)) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((((((triple1) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule6) OR ((((((triple2) -> rule3)) -> rule5) ((triple1) -> rule3)) -> rule6) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule6))]
The bear visits the lion.
("bear" "visits" "lion" "+")
triple1
The cow visits the lion.
("cow" "visits" "lion" "+")
triple2
The lion does not need the cow.
("lion" "needs" "cow" "-")
triple3
The lion is kind.
("lion" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple2) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is not rough.
("lion" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
The lion is not rough.
("lion" "is" "rough" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3