The bald eagle eats the lion. The bald eagle eats the rabbit. The bald eagle does not visit the mouse. The lion does not eat the rabbit. The lion is big. The lion is green. The lion is kind. The mouse is big. The mouse is kind. The rabbit eats the mouse. The rabbit is not kind. The rabbit does not see the bald eagle. If something sees the lion then it does not visit the rabbit. If something sees the mouse and it eats the bald eagle then the bald eagle is green. If something is green then it sees the rabbit. If something eats the bald eagle and it is not blue then it eats the lion. If something eats the rabbit then the rabbit sees the lion. If something visits the rabbit and it eats the mouse then the mouse is red.
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
The bald eagle eats the rabbit.
("bald eagle" "eats" "rabbit" "+")
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is not kind.
("rabbit" "is" "kind" "-")
The rabbit does not see the bald eagle.
("rabbit" "sees" "bald eagle" "-")
If something sees the lion then it does not visit the rabbit.
((("something" "sees" "lion" "+")) -> ("something" "visits" "rabbit" "-"))
If something sees the mouse and it eats the bald eagle then the bald eagle is green.
((("something" "sees" "mouse" "+") ("something" "eats" "bald eagle" "+")) -> ("bald eagle" "is" "green" "+"))
If something is green then it sees the rabbit.
((("something" "is" "green" "+")) -> ("something" "sees" "rabbit" "+"))
If something eats the bald eagle and it is not blue then it eats the lion.
((("something" "eats" "bald eagle" "+") ("something" "is" "blue" "~")) -> ("something" "eats" "lion" "+"))
If something eats the rabbit then the rabbit sees the lion.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
If something visits the rabbit and it eats the mouse then the mouse is red.
((("something" "visits" "rabbit" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "is" "red" "+"))
The lion is kind.
True
1
proof
[(triple7)]
("lion" "is" "kind" "+")
triple7
The mouse is not kind.
False
1
inv-proof
[(triple9)]
("mouse" "is" "kind" "-")
triple9
The lion sees the rabbit.
True
2
proof
[(((triple6) -> rule3))]
("lion" "sees" "rabbit" "+")
((triple6) -> (rule3 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The rabbit does not see the lion.
False
2
inv-proof
[(((triple2) -> rule5))]
("rabbit" "sees" "lion" "-")
((triple2) -> (rule5 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit does not visit the rabbit.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("rabbit" "visits" "rabbit" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit visits the rabbit.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("rabbit" "visits" "rabbit" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The bald eagle does not see the rabbit.
Unknown
inv-rconc
[@2: The bald eagle sees the rabbit.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("bald eagle" "sees" "rabbit" "-")
The mouse sees the rabbit.
Unknown
rconc
[@1: The mouse sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "rabbit" "+")
The rabbit does not eat the lion.
Unknown
inv-rconc
[@1: The rabbit eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "eats" "lion" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The bald eagle does not visit the mouse.[(triple3)] The bald eagle eats the lion.[(triple1)] The bald eagle eats the rabbit.[(triple2)] The lion does not eat the rabbit.[(triple4)] The lion is big.[(triple5)] The lion is green.[(triple6)] The lion is kind.[(triple7)] The mouse is big.[(triple8)] The mouse is kind.[(triple9)] The rabbit does not see the bald eagle.[(triple12)] The rabbit eats the mouse.[(triple10)] The rabbit is not kind.[(triple11)] @1: The lion sees the rabbit.[(((triple6) -> rule3))] The rabbit sees the lion.[(((triple2) -> rule5))] @2: The rabbit does not visit the rabbit.[(((((triple2) -> rule5)) -> rule1))]
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
triple3
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
triple1
The bald eagle eats the rabbit.
("bald eagle" "eats" "rabbit" "+")
triple2
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
triple4
The lion is big.
("lion" "is" "big" "+")
triple5
The lion is green.
("lion" "is" "green" "+")
triple6
The lion is kind.
("lion" "is" "kind" "+")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple8
The mouse is kind.
("mouse" "is" "kind" "+")
triple9
The rabbit does not see the bald eagle.
("rabbit" "sees" "bald eagle" "-")
triple12
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple10
The rabbit is not kind.
("rabbit" "is" "kind" "-")
triple11
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
((triple6) -> (rule3 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
((triple2) -> (rule5 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2