The bear sees the lion. The lion is nice. The tiger is round. If something sees the lion then the lion is green. If something sees the tiger then the tiger is green. If something likes the lion and the lion visits the bear then the bear visits the tiger.
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something sees the lion then the lion is green.
((("something" "sees" "lion" "+")) -> ("lion" "is" "green" "+"))
If something sees the tiger then the tiger is green.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If something likes the lion and the lion visits the bear then the bear visits the tiger.
((("something" "likes" "lion" "+") ("lion" "visits" "bear" "+")) -> ("bear" "visits" "tiger" "+"))
The lion is nice.
True
1
proof
[(triple2)]
("lion" "is" "nice" "+")
triple2
The bear does not see the lion.
False
1
inv-proof
[(triple1)]
("bear" "sees" "lion" "-")
triple1
The lion is green.
True
2
proof
[(((triple1) -> rule1))]
("lion" "is" "green" "+")
((triple1) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "is" "green" "-")
((triple1) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The bear does not visit the tiger.
Unknown
inv-rconc
[@1: The bear visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "tiger" "-")
The tiger is green.
Unknown
rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "green" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The bear sees the lion.[(triple1)] The lion is nice.[(triple2)] The tiger is round.[(triple3)] @1: The lion is green.[(((triple1) -> rule1))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The tiger is round.
("tiger" "is" "round" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
((triple1) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1