The bear eats the lion. The bear likes the lion. The lion eats the bear. If something is young and green then it is cold. If something likes the lion then the lion eats the bear. If something visits the lion and the lion visits the bear then the bear eats the lion. If something eats the lion then the lion visits the bear. If something eats the bear and it is round then the bear likes the lion. If something likes the lion and the lion likes the bear then it eats the bear.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
If something is young and green then it is cold.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something likes the lion then the lion eats the bear.
((("something" "likes" "lion" "+")) -> ("lion" "eats" "bear" "+"))
If something visits the lion and the lion visits the bear then the bear eats the lion.
((("something" "visits" "lion" "+") ("lion" "visits" "bear" "+")) -> ("bear" "eats" "lion" "+"))
If something eats the lion then the lion visits the bear.
((("something" "eats" "lion" "+")) -> ("lion" "visits" "bear" "+"))
If something eats the bear and it is round then the bear likes the lion.
((("something" "eats" "bear" "+") ("something" "is" "round" "+")) -> ("bear" "likes" "lion" "+"))
If something likes the lion and the lion likes the bear then it eats the bear.
((("something" "likes" "lion" "+") ("lion" "likes" "bear" "+")) -> ("something" "eats" "bear" "+"))
The bear likes the lion.
True
1
proof
[(triple2)]
("bear" "likes" "lion" "+")
triple2
The lion does not eat the bear.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule2))]
("lion" "eats" "bear" "-")
triple3
((triple2) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion visits the bear.
True
2
proof
[(((triple1) -> rule4))]
("lion" "visits" "bear" "+")
((triple1) -> (rule4 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion does not visit the bear.
False
2
inv-proof
[(((triple1) -> rule4))]
("lion" "visits" "bear" "-")
((triple1) -> (rule4 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "bear" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "cold" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The bear eats the lion.[(triple1)] The bear likes the lion.[(triple2)] The lion eats the bear.[(triple3 OR ((triple2) -> rule2))] @1: The lion visits the bear.[(((triple1) -> rule4))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear likes the lion.
("bear" "likes" "lion" "+")
triple2
The lion eats the bear.
("lion" "eats" "bear" "+")
triple3
((triple2) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
((triple1) -> (rule4 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1