The bald eagle is kind. The bald eagle is red. The lion is blue. The lion is rough. The lion likes the rabbit. The lion sees the bald eagle. The lion sees the mouse. The mouse likes the lion. The rabbit is blue. The rabbit likes the mouse. If something likes the lion then it needs the rabbit. If something needs the rabbit then the rabbit sees the mouse.
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle is red.
("bald eagle" "is" "red" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
If something likes the lion then it needs the rabbit.
((("something" "likes" "lion" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the rabbit then the rabbit sees the mouse.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
The lion sees the bald eagle.
True
1
proof
[(triple6)]
("lion" "sees" "bald eagle" "+")
triple6
The rabbit does not like the mouse.
False
1
inv-proof
[(triple10)]
("rabbit" "likes" "mouse" "-")
triple10
The mouse needs the rabbit.
True
2
proof
[(((triple8) -> rule1))]
("mouse" "needs" "rabbit" "+")
((triple8) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse does not need the rabbit.
False
2
inv-proof
[(((triple8) -> rule1))]
("mouse" "needs" "rabbit" "-")
((triple8) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit sees the mouse.
True
3
proof
[(((((triple8) -> rule1)) -> rule2))]
("rabbit" "sees" "mouse" "+")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit does not see the mouse.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule2))]
("rabbit" "sees" "mouse" "-")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The lion does not need the rabbit.
Unknown
inv-rconc
[@1: The lion needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The bald eagle does not need the rabbit.
Unknown
inv-rconc
[@1: The bald eagle needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "needs" "rabbit" "-")
The bald eagle needs the lion.
Unknown
random
[@0: The bald eagle needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "lion" "+")
The mouse does not like the rabbit.
Unknown
inv-random
[@0: The mouse likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "rabbit" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The bald eagle is kind.[(triple1)] The bald eagle is red.[(triple2)] The lion is blue.[(triple3)] The lion is rough.[(triple4)] The lion likes the rabbit.[(triple5)] The lion sees the bald eagle.[(triple6)] The lion sees the mouse.[(triple7)] The mouse likes the lion.[(triple8)] The rabbit is blue.[(triple9)] The rabbit likes the mouse.[(triple10)] @1: The mouse needs the rabbit.[(((triple8) -> rule1))] @2: The rabbit sees the mouse.[(((((triple8) -> rule1)) -> rule2))]
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple1
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple5
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple6
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple7
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple10
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((triple8) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2