The bald eagle likes the bear. The bear eats the rabbit. The cow visits the bald eagle. The rabbit eats the bald eagle. If something visits the cow and it is not young then the cow visits the rabbit. If something visits the cow and the cow is not blue then it likes the cow. If something eats the cow then it likes the cow. If something likes the bear then the bear eats the cow. If something likes the cow then the cow visits the bear. If the bear is green and the bear is not round then the bear eats the rabbit. If something eats the bald eagle then the bald eagle is not kind. If the rabbit does not eat the cow then the cow does not like the bald eagle.
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
The rabbit eats the bald eagle.
("rabbit" "eats" "bald eagle" "+")
If something visits the cow and it is not young then the cow visits the rabbit.
((("something" "visits" "cow" "+") ("something" "is" "young" "~")) -> ("cow" "visits" "rabbit" "+"))
If something visits the cow and the cow is not blue then it likes the cow.
((("something" "visits" "cow" "+") ("cow" "is" "blue" "~")) -> ("something" "likes" "cow" "+"))
If something eats the cow then it likes the cow.
((("something" "eats" "cow" "+")) -> ("something" "likes" "cow" "+"))
If something likes the bear then the bear eats the cow.
((("something" "likes" "bear" "+")) -> ("bear" "eats" "cow" "+"))
If something likes the cow then the cow visits the bear.
((("something" "likes" "cow" "+")) -> ("cow" "visits" "bear" "+"))
If the bear is green and the bear is not round then the bear eats the rabbit.
((("bear" "is" "green" "+") ("bear" "is" "round" "~")) -> ("bear" "eats" "rabbit" "+"))
If something eats the bald eagle then the bald eagle is not kind.
((("something" "eats" "bald eagle" "+")) -> ("bald eagle" "is" "kind" "-"))
If the rabbit does not eat the cow then the cow does not like the bald eagle.
((("rabbit" "eats" "cow" "~")) -> ("cow" "likes" "bald eagle" "-"))
The bald eagle likes the bear.
True
1
proof
[(triple1)]
("bald eagle" "likes" "bear" "+")
triple1
The bald eagle does not like the bear.
False
1
inv-proof
[(triple1)]
("bald eagle" "likes" "bear" "-")
triple1
The bear eats the cow.
True
2
proof
[(((triple1) -> rule4))]
("bear" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bald eagle is kind.
False
2
inv-proof
[(((triple4) -> rule7))]
("bald eagle" "is" "kind" "+")
((triple4) -> (rule7 % int1))
The bald eagle is not kind.
("bald eagle" "is" "kind" "-")
int1
The bear likes the cow.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("bear" "likes" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
int2
The bear does not like the cow.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("bear" "likes" "cow" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
int2
The cow visits the bear.
True
4
proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule5))]
("cow" "visits" "bear" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3
The cow does not visit the bear.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule5))]
("cow" "visits" "bear" "-")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "cow" "-")
The rabbit likes the cow.
Unknown
rconc
[@1: The rabbit likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "likes" "cow" "+")
The bald eagle does not like the cow.
Unknown
inv-rconc
[@1: The bald eagle likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "likes" "cow" "-")
The cow visits the rabbit.
Unknown
rconc
[@1: The cow visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "rabbit" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The cow likes the rabbit.
Unknown
random
[@0: The cow likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "rabbit" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
@0: The bald eagle likes the bear.[(triple1)] The bear eats the rabbit.[(triple2)] The cow visits the bald eagle.[(triple3)] The rabbit eats the bald eagle.[(triple4)] @1: The bald eagle is not kind.[(((triple4) -> rule7))] The bear eats the cow.[(((triple1) -> rule4))] @2: The bear likes the cow.[(((((triple1) -> rule4)) -> rule3))] @3: The cow visits the bear.[(((((((triple1) -> rule4)) -> rule3)) -> rule5))]
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
triple1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple2
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
triple3
The rabbit eats the bald eagle.
("rabbit" "eats" "bald eagle" "+")
triple4
The bald eagle is not kind.
("bald eagle" "is" "kind" "-")
((triple4) -> (rule7 % int1))
The bald eagle is not kind.
("bald eagle" "is" "kind" "-")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
int2
The cow visits the bear.
("cow" "visits" "bear" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3