The bald eagle is red. The bald eagle likes the lion. The lion is kind. If someone needs the bald eagle then they like the lion. If someone needs the lion then the lion is rough. If someone sees the bald eagle and the bald eagle needs the lion then the bald eagle likes the lion. If the bald eagle sees the lion then the bald eagle needs the lion. If someone needs the bald eagle then the bald eagle likes the lion. If the bald eagle likes the lion then the bald eagle sees the lion.
The bald eagle is red.
("bald eagle" "is" "red" "+")
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
If someone needs the bald eagle then they like the lion.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "likes" "lion" "+"))
If someone needs the lion then the lion is rough.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "rough" "+"))
If someone sees the bald eagle and the bald eagle needs the lion then the bald eagle likes the lion.
((("someone" "sees" "bald eagle" "+") ("bald eagle" "needs" "lion" "+")) -> ("bald eagle" "likes" "lion" "+"))
If the bald eagle sees the lion then the bald eagle needs the lion.
((("bald eagle" "sees" "lion" "+")) -> ("bald eagle" "needs" "lion" "+"))
If someone needs the bald eagle then the bald eagle likes the lion.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "likes" "lion" "+"))
If the bald eagle likes the lion then the bald eagle sees the lion.
((("bald eagle" "likes" "lion" "+")) -> ("bald eagle" "sees" "lion" "+"))
The bald eagle is red.
True
1
proof
[(triple1)]
("bald eagle" "is" "red" "+")
triple1
The lion is not kind.
False
1
inv-proof
[(triple3)]
("lion" "is" "kind" "-")
triple3
The bald eagle sees the lion.
True
2
proof
[(((triple2) -> rule6))]
("bald eagle" "sees" "lion" "+")
((triple2) -> (rule6 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle does not see the lion.
False
2
inv-proof
[(((triple2) -> rule6))]
("bald eagle" "sees" "lion" "-")
((triple2) -> (rule6 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle needs the lion.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("bald eagle" "needs" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The bald eagle does not need the lion.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("bald eagle" "needs" "lion" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The lion is rough.
True
4
proof
[(((((((triple2) -> rule6)) -> rule4)) -> rule2))]
("lion" "is" "rough" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The lion is not rough.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule4)) -> rule2))]
("lion" "is" "rough" "-")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "lion" "-")
The bald eagle is kind.
Unknown
random
[@0: The bald eagle is kind.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "kind" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The bald eagle needs the bald eagle.
Unknown
random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "+")
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 bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The bald eagle is big.
Unknown
random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "+")
@0: The bald eagle is red.[(triple1)] The bald eagle likes the lion.[(triple2)] The lion is kind.[(triple3)] @1: The bald eagle sees the lion.[(((triple2) -> rule6))] @2: The bald eagle needs the lion.[(((((triple2) -> rule6)) -> rule4))] @3: The lion is rough.[(((((((triple2) -> rule6)) -> rule4)) -> rule2))]
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple1
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
((triple2) -> (rule6 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3