The bald eagle eats the bear. The bear eats the cow. The cow eats the lion. The lion eats the cow. If someone is big then they see the lion. If someone sees the lion then they are round. If someone eats the bear then they are big. If someone sees the cow then the cow does not like the bald eagle. If someone eats the bear then the bear sees the bald eagle. If someone sees the bear then the bear is round. If someone is cold then they like the lion. If someone sees the cow and they do not like the bald eagle then the cow does not see the bald eagle.
The bald eagle eats the bear.
("bald eagle" "eats" "bear" "+")
The bear eats the cow.
("bear" "eats" "cow" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
If someone is big then they see the lion.
((("someone" "is" "big" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the lion then they are round.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "round" "+"))
If someone eats the bear then they are big.
((("someone" "eats" "bear" "+")) -> ("someone" "is" "big" "+"))
If someone sees the cow then the cow does not like the bald eagle.
((("someone" "sees" "cow" "+")) -> ("cow" "likes" "bald eagle" "-"))
If someone eats the bear then the bear sees the bald eagle.
((("someone" "eats" "bear" "+")) -> ("bear" "sees" "bald eagle" "+"))
If someone sees the bear then the bear is round.
((("someone" "sees" "bear" "+")) -> ("bear" "is" "round" "+"))
If someone is cold then they like the lion.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "lion" "+"))
If someone sees the cow and they do not like the bald eagle then the cow does not see the bald eagle.
((("someone" "sees" "cow" "+") ("someone" "likes" "bald eagle" "~")) -> ("cow" "sees" "bald eagle" "-"))
The bear eats the cow.
True
1
proof
[(triple2)]
("bear" "eats" "cow" "+")
triple2
The lion does not eat the cow.
False
1
inv-proof
[(triple4)]
("lion" "eats" "cow" "-")
triple4
The bear sees the bald eagle.
True
2
proof
[(((triple1) -> rule5))]
("bear" "sees" "bald eagle" "+")
((triple1) -> (rule5 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bear does not see the bald eagle.
False
2
inv-proof
[(((triple1) -> rule5))]
("bear" "sees" "bald eagle" "-")
((triple1) -> (rule5 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bald eagle sees the lion.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("bald eagle" "sees" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle is big.
("bald eagle" "is" "big" "+")
int2
The bald eagle does not see the lion.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("bald eagle" "sees" "lion" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle is big.
("bald eagle" "is" "big" "+")
int2
The bald eagle is round.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("bald eagle" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle is round.
("bald eagle" "is" "round" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The bald eagle is big.
("bald eagle" "is" "big" "+")
int3
The bald eagle is not round.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("bald eagle" "is" "round" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle is round.
("bald eagle" "is" "round" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The bald eagle is big.
("bald eagle" "is" "big" "+")
int3
The lion is not round.
Unknown
inv-rconc
[@3: The lion is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("lion" "is" "round" "-")
The bear likes the lion.
Unknown
rconc
[@1: The bear likes the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "likes" "lion" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "big" "-")
The bear sees the lion.
Unknown
rconc
[@2: The bear sees the lion.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("bear" "sees" "lion" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The bald eagle does not eat the lion.
Unknown
inv-random
[@0: The bald eagle eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "lion" "-")
The bald eagle sees the cow.
Unknown
random
[@0: The bald eagle sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "cow" "+")
@0: The bald eagle eats the bear.[(triple1)] The bear eats the cow.[(triple2)] The cow eats the lion.[(triple3)] The lion eats the cow.[(triple4)] @1: The bald eagle is big.[(((triple1) -> rule3))] The bear sees the bald eagle.[(((triple1) -> rule5))] @2: The bald eagle sees the lion.[(((((triple1) -> rule3)) -> rule1))] @3: The bald eagle is round.[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
The bald eagle eats the bear.
("bald eagle" "eats" "bear" "+")
triple1
The bear eats the cow.
("bear" "eats" "cow" "+")
triple2
The cow eats the lion.
("cow" "eats" "lion" "+")
triple3
The lion eats the cow.
("lion" "eats" "cow" "+")
triple4
The bald eagle is big.
("bald eagle" "is" "big" "+")
((triple1) -> (rule3 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
((triple1) -> (rule5 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle is big.
("bald eagle" "is" "big" "+")
int2
The bald eagle is round.
("bald eagle" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle is round.
("bald eagle" "is" "round" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The bald eagle is big.
("bald eagle" "is" "big" "+")
int3