The bald eagle sees the bear. The bear is cold. The dog eats the bald eagle. The lion sees the bear. If the lion is green then the lion likes the bald eagle. If the bald eagle is rough then the bald eagle eats the dog. If something sees the bear then it eats the bear. If the bald eagle likes the dog then the bald eagle likes the bear. If something likes the dog and the dog sees the bald eagle then the bald eagle is young. If the lion eats the bear then the bear sees the bald eagle. If something sees the bald eagle then it eats the lion. If something is young then it sees the lion.
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
The bear is cold.
("bear" "is" "cold" "+")
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
If the lion is green then the lion likes the bald eagle.
((("lion" "is" "green" "+")) -> ("lion" "likes" "bald eagle" "+"))
If the bald eagle is rough then the bald eagle eats the dog.
((("bald eagle" "is" "rough" "+")) -> ("bald eagle" "eats" "dog" "+"))
If something sees the bear then it eats the bear.
((("something" "sees" "bear" "+")) -> ("something" "eats" "bear" "+"))
If the bald eagle likes the dog then the bald eagle likes the bear.
((("bald eagle" "likes" "dog" "+")) -> ("bald eagle" "likes" "bear" "+"))
If something likes the dog and the dog sees the bald eagle then the bald eagle is young.
((("something" "likes" "dog" "+") ("dog" "sees" "bald eagle" "+")) -> ("bald eagle" "is" "young" "+"))
If the lion eats the bear then the bear sees the bald eagle.
((("lion" "eats" "bear" "+")) -> ("bear" "sees" "bald eagle" "+"))
If something sees the bald eagle then it eats the lion.
((("something" "sees" "bald eagle" "+")) -> ("something" "eats" "lion" "+"))
If something is young then it sees the lion.
((("something" "is" "young" "+")) -> ("something" "sees" "lion" "+"))
The bald eagle sees the bear.
True
1
proof
[(triple1)]
("bald eagle" "sees" "bear" "+")
triple1
The dog does not eat the bald eagle.
False
1
inv-proof
[(triple3)]
("dog" "eats" "bald eagle" "-")
triple3
The bald eagle eats the bear.
True
2
proof
[(((triple1) -> rule3))]
("bald eagle" "eats" "bear" "+")
((triple1) -> (rule3 % int1))
The bald eagle eats the bear.
("bald eagle" "eats" "bear" "+")
int1
The lion does not eat the bear.
False
2
inv-proof
[(((triple4) -> rule3))]
("lion" "eats" "bear" "-")
((triple4) -> (rule3 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The bear sees the bald eagle.
True
3
proof
[(((((triple4) -> rule3)) -> rule6))]
("bear" "sees" "bald eagle" "+")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The bear does not see the bald eagle.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule6))]
("bear" "sees" "bald eagle" "-")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The bear eats the lion.
True
4
proof
[(((((((triple4) -> rule3)) -> rule6)) -> rule7))]
("bear" "eats" "lion" "+")
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The bear does not eat the lion.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule6)) -> rule7))]
("bear" "eats" "lion" "-")
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "eats" "lion" "-")
The bald eagle eats the lion.
Unknown
rconc
[@1: The bald eagle eats the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "eats" "lion" "+")
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "eats" "bear" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "sees" "lion" "+")
The bear does not like the bald eagle.
Unknown
inv-random
[@0: The bear likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bald eagle" "-")
The lion eats the bald eagle.
Unknown
random
[@0: The lion eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "bald eagle" "+")
The lion does not like the dog.
Unknown
inv-random
[@0: The lion likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "dog" "-")
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 sees the bear.[(triple1)] The bear is cold.[(triple2)] The dog eats the bald eagle.[(triple3)] The lion sees the bear.[(triple4)] @1: The bald eagle eats the bear.[(((triple1) -> rule3))] The lion eats the bear.[(((triple4) -> rule3))] @2: The bear sees the bald eagle.[(((((triple4) -> rule3)) -> rule6))] @3: The bear eats the lion.[(((((((triple4) -> rule3)) -> rule6)) -> rule7))]
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
triple3
The lion sees the bear.
("lion" "sees" "bear" "+")
triple4
The bald eagle eats the bear.
("bald eagle" "eats" "bear" "+")
((triple1) -> (rule3 % int1))
The bald eagle eats the bear.
("bald eagle" "eats" "bear" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
((triple4) -> (rule3 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The bear eats the lion.
("bear" "eats" "lion" "+")
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3