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