The bear is round. The dog eats the bear. The lion is young. The tiger sees the bear. If something is round and it visits the tiger then it eats the lion. If something eats the tiger then the tiger eats the dog. If something is red and it eats the lion then the lion sees the tiger. If the tiger is round and the tiger eats the dog then the tiger eats the bear. If the bear is big then the bear is round. If something eats the tiger and it eats the bear then the bear is round. If something sees the lion then it eats the bear. If something eats the bear then the bear sees the lion.
The bear is round.
("bear" "is" "round" "+")
The dog eats the bear.
("dog" "eats" "bear" "+")
The lion is young.
("lion" "is" "young" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something is round and it visits the tiger then it eats the lion.
((("something" "is" "round" "+") ("something" "visits" "tiger" "+")) -> ("something" "eats" "lion" "+"))
If something eats the tiger then the tiger eats the dog.
((("something" "eats" "tiger" "+")) -> ("tiger" "eats" "dog" "+"))
If something is red and it eats the lion then the lion sees the tiger.
((("something" "is" "red" "+") ("something" "eats" "lion" "+")) -> ("lion" "sees" "tiger" "+"))
If the tiger is round and the tiger eats the dog then the tiger eats the bear.
((("tiger" "is" "round" "+") ("tiger" "eats" "dog" "+")) -> ("tiger" "eats" "bear" "+"))
If the bear is big then the bear is round.
((("bear" "is" "big" "+")) -> ("bear" "is" "round" "+"))
If something eats the tiger and it eats the bear then the bear is round.
((("something" "eats" "tiger" "+") ("something" "eats" "bear" "+")) -> ("bear" "is" "round" "+"))
If something sees the lion then it eats the bear.
((("something" "sees" "lion" "+")) -> ("something" "eats" "bear" "+"))
If something eats the bear then the bear sees the lion.
((("something" "eats" "bear" "+")) -> ("bear" "sees" "lion" "+"))
The bear is round.
True
1
proof
[(triple1)]
("bear" "is" "round" "+")
triple1
The lion is not young.
False
1
inv-proof
[(triple3)]
("lion" "is" "young" "-")
triple3
The bear sees the lion.
True
2
proof
[(((triple2) -> rule8))]
("bear" "sees" "lion" "+")
((triple2) -> (rule8 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear does not see the lion.
False
2
inv-proof
[(((triple2) -> rule8))]
("bear" "sees" "lion" "-")
((triple2) -> (rule8 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear eats the bear.
True
3
proof
[(((((triple2) -> rule8)) -> rule7))]
("bear" "eats" "bear" "+")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The bear does not eat the bear.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule7))]
("bear" "eats" "bear" "-")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2
The dog does not eat the lion.
Unknown
inv-rconc
[@1: The dog eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "lion" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "lion" "+")
The tiger does not eat the dog.
Unknown
inv-rconc
[@1: The tiger eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "dog" "-")
The tiger sees the dog.
Unknown
random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "+")
The bear does not see the tiger.
Unknown
inv-random
[@0: The bear sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "tiger" "-")
The tiger visits the bear.
Unknown
random
[@0: The tiger visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "bear" "+")
@0: The bear is round.[(triple1)] The dog eats the bear.[(triple2)] The lion is young.[(triple3)] The tiger sees the bear.[(triple4)] @1: The bear sees the lion.[(((triple2) -> rule8))] @2: The bear eats the bear.[(((((triple2) -> rule8)) -> rule7))]
The bear is round.
("bear" "is" "round" "+")
triple1
The dog eats the bear.
("dog" "eats" "bear" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple4
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple2) -> (rule8 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
int2