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