The bear chases the lion. The bear likes the lion. The lion chases the bear. The lion is cold. The lion is young. The lion likes the bear. The lion visits the bear. If someone likes the bear and the bear likes the lion then they like the lion. If someone is big then they like the bear.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If someone likes the bear and the bear likes the lion then they like the lion.
((("someone" "likes" "bear" "+") ("bear" "likes" "lion" "+")) -> ("someone" "likes" "lion" "+"))
If someone is big then they like the bear.
((("someone" "is" "big" "+")) -> ("someone" "likes" "bear" "+"))
The lion is cold.
True
1
proof
[(triple4)]
("lion" "is" "cold" "+")
triple4
The lion is not young.
False
1
inv-proof
[(triple5)]
("lion" "is" "young" "-")
triple5
The lion likes the lion.
True
3
proof
[(((triple6 triple2) -> rule1))]
("lion" "likes" "lion" "+")
((triple6 triple2) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not like the lion.
False
3
inv-proof
[(((triple6 triple2) -> rule1))]
("lion" "likes" "lion" "-")
((triple6 triple2) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "bear" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The bear chases the lion.[(triple1)] The bear likes the lion.[(triple2)] The lion chases the bear.[(triple3)] The lion is cold.[(triple4)] The lion is young.[(triple5)] The lion likes the bear.[(triple6)] The lion visits the bear.[(triple7)] @1: The lion likes the lion.[(((triple6 triple2) -> rule1))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear likes the lion.
("bear" "likes" "lion" "+")
triple2
The lion chases the bear.
("lion" "chases" "bear" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion likes the bear.
("lion" "likes" "bear" "+")
triple6
The lion visits the bear.
("lion" "visits" "bear" "+")
triple7
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple6 triple2) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1