The bear is green. The lion needs the bear. If someone needs the bear then they visit the lion. If someone sees the lion and they visit the lion then they need the bear. If someone visits the lion then they are kind.
The bear is green.
("bear" "is" "green" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
If someone needs the bear then they visit the lion.
((("someone" "needs" "bear" "+")) -> ("someone" "visits" "lion" "+"))
If someone sees the lion and they visit the lion then they need the bear.
((("someone" "sees" "lion" "+") ("someone" "visits" "lion" "+")) -> ("someone" "needs" "bear" "+"))
If someone visits the lion then they are kind.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "kind" "+"))
The lion needs the bear.
True
1
proof
[(triple2)]
("lion" "needs" "bear" "+")
triple2
The bear is not green.
False
1
inv-proof
[(triple1)]
("bear" "is" "green" "-")
triple1
The lion visits the lion.
True
2
proof
[(((triple2) -> rule1))]
("lion" "visits" "lion" "+")
((triple2) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "visits" "lion" "-")
((triple2) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is kind.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("lion" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is not kind.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("lion" "is" "kind" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear visits the lion.
Unknown
rconc
[@2: The bear visits the lion.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("bear" "visits" "lion" "+")
The bear is not kind.
Unknown
inv-rconc
[@3: The bear is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("bear" "is" "kind" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear is green.[(triple1)] The lion needs the bear.[(triple2)] @1: The lion visits the lion.[(((triple2) -> rule1))] @2: The lion is kind.[(((((triple2) -> rule1)) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The lion needs the bear.
("lion" "needs" "bear" "+")
triple2
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple2) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2