The bald eagle does not like the rabbit. The bear likes the bald eagle. The dog is rough. The rabbit eats the dog. If something eats the rabbit and it is big then it needs the bald eagle. Rough things are young. Young things are kind. If something is kind then it does not eat the bald eagle. If something eats the bear and the bear is big then the bear likes the dog. If something likes the bear and the bear does not need the bald eagle then the bald eagle eats the bear.
The bald eagle does not like the rabbit.
("bald eagle" "likes" "rabbit" "-")
The bear likes the bald eagle.
("bear" "likes" "bald eagle" "+")
The dog is rough.
("dog" "is" "rough" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
If something eats the rabbit and it is big then it needs the bald eagle.
((("something" "eats" "rabbit" "+") ("something" "is" "big" "+")) -> ("something" "needs" "bald eagle" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it does not eat the bald eagle.
((("something" "is" "kind" "+")) -> ("something" "eats" "bald eagle" "-"))
If something eats the bear and the bear is big then the bear likes the dog.
((("something" "eats" "bear" "+") ("bear" "is" "big" "+")) -> ("bear" "likes" "dog" "+"))
If something likes the bear and the bear does not need the bald eagle then the bald eagle eats the bear.
((("something" "likes" "bear" "+") ("bear" "needs" "bald eagle" "~")) -> ("bald eagle" "eats" "bear" "+"))
The bald eagle does not like the rabbit.
True
1
proof
[(triple1)]
("bald eagle" "likes" "rabbit" "-")
triple1
The dog is not rough.
False
1
inv-proof
[(triple3)]
("dog" "is" "rough" "-")
triple3
The dog is young.
True
2
proof
[(((triple3) -> rule2))]
("dog" "is" "young" "+")
((triple3) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "is" "young" "-")
((triple3) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is kind.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("dog" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is not kind.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("dog" "is" "kind" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog does not eat the bald eagle.
True
4
proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule4))]
("dog" "eats" "bald eagle" "-")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The dog does not eat the bald eagle.
("dog" "eats" "bald eagle" "-")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog eats the bald eagle.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule4))]
("dog" "eats" "bald eagle" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The dog does not eat the bald eagle.
("dog" "eats" "bald eagle" "-")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "young" "-")
The bear is young.
Unknown
rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "young" "+")
The bald eagle is not kind.
Unknown
inv-rconc
[@2: The bald eagle is kind.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("bald eagle" "is" "kind" "-")
The bald eagle is young.
Unknown
rconc
[@1: The bald eagle is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "young" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bald eagle needs the dog.
Unknown
random
[@0: The bald eagle needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "dog" "+")
The rabbit does not eat the bear.
Unknown
inv-random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The bald eagle does not like the rabbit.[(triple1)] The bear likes the bald eagle.[(triple2)] The dog is rough.[(triple3)] The rabbit eats the dog.[(triple4)] @1: The dog is young.[(((triple3) -> rule2))] @2: The dog is kind.[(((((triple3) -> rule2)) -> rule3))] @3: The dog does not eat the bald eagle.[(((((((triple3) -> rule2)) -> rule3)) -> rule4))]
The bald eagle does not like the rabbit.
("bald eagle" "likes" "rabbit" "-")
triple1
The bear likes the bald eagle.
("bear" "likes" "bald eagle" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
((triple3) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog does not eat the bald eagle.
("dog" "eats" "bald eagle" "-")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The dog does not eat the bald eagle.
("dog" "eats" "bald eagle" "-")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3