The bear eats the lion. The lion eats the bear. The rabbit eats the lion. If the bear visits the rabbit and the bear visits the lion then the rabbit sees the lion. If someone visits the lion then they are blue. If the lion visits the bear then the bear visits the lion. If the lion visits the rabbit and the lion eats the rabbit then the rabbit visits the bear. If someone eats the lion then the lion visits the bear. If someone is round then they eat the lion. If someone sees the lion and they are kind then the lion sees the rabbit. If the rabbit sees the lion then the rabbit is blue.
The bear eats the lion.
("bear" "eats" "lion" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
If the bear visits the rabbit and the bear visits the lion then the rabbit sees the lion.
((("bear" "visits" "rabbit" "+") ("bear" "visits" "lion" "+")) -> ("rabbit" "sees" "lion" "+"))
If someone visits the lion then they are blue.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "blue" "+"))
If the lion visits the bear then the bear visits the lion.
((("lion" "visits" "bear" "+")) -> ("bear" "visits" "lion" "+"))
If the lion visits the rabbit and the lion eats the rabbit then the rabbit visits the bear.
((("lion" "visits" "rabbit" "+") ("lion" "eats" "rabbit" "+")) -> ("rabbit" "visits" "bear" "+"))
If someone eats the lion then the lion visits the bear.
((("someone" "eats" "lion" "+")) -> ("lion" "visits" "bear" "+"))
If someone is round then they eat the lion.
((("someone" "is" "round" "+")) -> ("someone" "eats" "lion" "+"))
If someone sees the lion and they are kind then the lion sees the rabbit.
((("someone" "sees" "lion" "+") ("someone" "is" "kind" "+")) -> ("lion" "sees" "rabbit" "+"))
If the rabbit sees the lion then the rabbit is blue.
((("rabbit" "sees" "lion" "+")) -> ("rabbit" "is" "blue" "+"))
The rabbit eats the lion.
True
1
proof
[(triple3)]
("rabbit" "eats" "lion" "+")
triple3
The rabbit does not eat the lion.
False
1
inv-proof
[(triple3)]
("rabbit" "eats" "lion" "-")
triple3
The lion visits the bear.
True
2
proof
[(((triple1) -> rule5) OR ((triple3) -> rule5))]
("lion" "visits" "bear" "+")
((triple1) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
((triple3) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion does not visit the bear.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple3) -> rule5))]
("lion" "visits" "bear" "-")
((triple1) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
((triple3) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The bear visits the lion.
True
3
proof
[(((((triple1) -> rule5)) -> rule3) OR ((((triple3) -> rule5)) -> rule3))]
("bear" "visits" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The bear does not visit the lion.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3) OR ((((triple3) -> rule5)) -> rule3))]
("bear" "visits" "lion" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The bear is blue.
True
4
proof
[(((((((triple1) -> rule5)) -> rule3)) -> rule2) OR ((((((triple3) -> rule5)) -> rule3)) -> rule2))]
("bear" "is" "blue" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
int3
The bear is not blue.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule3)) -> rule2) OR ((((((triple3) -> rule5)) -> rule3)) -> rule2))]
("bear" "is" "blue" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
int3
The rabbit does not see the lion.
Unknown
inv-rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "lion" "-")
The rabbit is blue.
Unknown
rconc
[@2: The rabbit is blue.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("rabbit" "is" "blue" "+")
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "lion" "-")
The rabbit visits the bear.
Unknown
rconc
[@1: The rabbit visits the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "visits" "bear" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The bear visits the rabbit.
Unknown
random
[@0: The bear visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "rabbit" "+")
The lion does not see the bear.
Unknown
inv-random
[@0: The lion sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bear" "-")
The bear eats the rabbit.
Unknown
random
[@0: The bear eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "rabbit" "+")
@0: The bear eats the lion.[(triple1)] The lion eats the bear.[(triple2)] The rabbit eats the lion.[(triple3)] @1: The lion visits the bear.[(((triple1) -> rule5) OR ((triple3) -> rule5))] @2: The bear visits the lion.[(((((triple1) -> rule5)) -> rule3) OR ((((triple3) -> rule5)) -> rule3))] @3: The bear is blue.[(((((((triple1) -> rule5)) -> rule3)) -> rule2) OR ((((((triple3) -> rule5)) -> rule3)) -> rule2))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The lion eats the bear.
("lion" "eats" "bear" "+")
triple2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple3
The lion visits the bear.
("lion" "visits" "bear" "+")
((triple1) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
((triple3) -> (rule5 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
int3