The bald eagle likes the lion. The lion is big. The lion visits the bald eagle. If the bald eagle does not like the lion then the lion likes the bald eagle. If someone is young then they visit the lion. If the lion visits the bald eagle then the lion is young.
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion visits the bald eagle.
("lion" "visits" "bald eagle" "+")
If the bald eagle does not like the lion then the lion likes the bald eagle.
((("bald eagle" "likes" "lion" "~")) -> ("lion" "likes" "bald eagle" "+"))
If someone is young then they visit the lion.
((("someone" "is" "young" "+")) -> ("someone" "visits" "lion" "+"))
If the lion visits the bald eagle then the lion is young.
((("lion" "visits" "bald eagle" "+")) -> ("lion" "is" "young" "+"))
The bald eagle likes the lion.
True
1
proof
[(triple1)]
("bald eagle" "likes" "lion" "+")
triple1
The lion is not big.
False
1
inv-proof
[(triple2)]
("lion" "is" "big" "-")
triple2
The lion is young.
True
2
proof
[(((triple3) -> rule3))]
("lion" "is" "young" "+")
((triple3) -> (rule3 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple3) -> rule3))]
("lion" "is" "young" "-")
((triple3) -> (rule3 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the lion.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("lion" "visits" "lion" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not visit the lion.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("lion" "visits" "lion" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not like the bald eagle.
Unknown
inv-rconc
[@1: The lion likes the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "bald eagle" "-")
The bald eagle visits the lion.
Unknown
rconc
[@1: The bald eagle visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "visits" "lion" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The bald eagle likes the bald eagle.
Unknown
random
[@0: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "bald eagle" "+")
@0: The bald eagle likes the lion.[(triple1)] The lion is big.[(triple2)] The lion visits the bald eagle.[(triple3)] @1: The lion is young.[(((triple3) -> rule3))] @2: The lion visits the lion.[(((((triple3) -> rule3)) -> rule2))]
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion visits the bald eagle.
("lion" "visits" "bald eagle" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
((triple3) -> (rule3 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2