The bald eagle is nice. The bald eagle likes the bear. The bald eagle sees the cow. The bald eagle sees the mouse. The bear chases the mouse. The bear is big. The bear is nice. The bear sees the bald eagle. The cow chases the mouse. The mouse chases the bald eagle. The mouse is young. The mouse does not see the cow. If something is cold and nice then it sees the mouse. If something chases the bald eagle then it likes the bald eagle. If something is big and it likes the bear then it does not like the mouse. If something likes the bald eagle then the bald eagle is big. If something is young and it does not like the bear then the bear sees the mouse. If something sees the bear and it does not see the mouse then the mouse sees the cow.
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
If something is cold and nice then it sees the mouse.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "sees" "mouse" "+"))
If something chases the bald eagle then it likes the bald eagle.
((("something" "chases" "bald eagle" "+")) -> ("something" "likes" "bald eagle" "+"))
If something is big and it likes the bear then it does not like the mouse.
((("something" "is" "big" "+") ("something" "likes" "bear" "+")) -> ("something" "likes" "mouse" "-"))
If something likes the bald eagle then the bald eagle is big.
((("something" "likes" "bald eagle" "+")) -> ("bald eagle" "is" "big" "+"))
If something is young and it does not like the bear then the bear sees the mouse.
((("something" "is" "young" "+") ("something" "likes" "bear" "~")) -> ("bear" "sees" "mouse" "+"))
If something sees the bear and it does not see the mouse then the mouse sees the cow.
((("something" "sees" "bear" "+") ("something" "sees" "mouse" "~")) -> ("mouse" "sees" "cow" "+"))
The bald eagle sees the mouse.
True
1
proof
[(triple4)]
("bald eagle" "sees" "mouse" "+")
triple4
The mouse sees the cow.
False
1
inv-proof
[(triple12)]
("mouse" "sees" "cow" "+")
triple12
The mouse likes the bald eagle.
True
2
proof
[(((triple10) -> rule2))]
("mouse" "likes" "bald eagle" "+")
((triple10) -> (rule2 % int1))
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int1
The mouse does not like the bald eagle.
False
2
inv-proof
[(((triple10) -> rule2))]
("mouse" "likes" "bald eagle" "-")
((triple10) -> (rule2 % int1))
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int1
The bald eagle is big.
True
3
proof
[(((((triple10) -> rule2)) -> rule4))]
("bald eagle" "is" "big" "+")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
The bald eagle is not big.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule4))]
("bald eagle" "is" "big" "-")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
The bald eagle does not like the mouse.
True
5
proof
[(((((((triple10) -> rule2)) -> rule4) triple2) -> rule3))]
("bald eagle" "likes" "mouse" "-")
((((((triple10) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The bald eagle does not like the mouse.
("bald eagle" "likes" "mouse" "-")
int1
The bald eagle is big.
("bald eagle" "is" "big" "+")
int2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int3
The bald eagle likes the mouse.
False
5
inv-proof
[(((((((triple10) -> rule2)) -> rule4) triple2) -> rule3))]
("bald eagle" "likes" "mouse" "+")
((((((triple10) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The bald eagle does not like the mouse.
("bald eagle" "likes" "mouse" "-")
int1
The bald eagle is big.
("bald eagle" "is" "big" "+")
int2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int3
The bald eagle does not like the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "likes" "bald eagle" "-")
The cow sees the mouse.
Unknown
rconc
[@1: The cow sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "mouse" "+")
The bear does not see the mouse.
Unknown
inv-rconc
[@1: The bear sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "mouse" "-")
The bear likes the bald eagle.
Unknown
rconc
[@1: The bear likes the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "bald eagle" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The bald eagle chases the bear.
Unknown
random
[@0: The bald eagle chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bear" "+")
The cow does not like the mouse.
Unknown
inv-random
[@0: The cow likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The bald eagle is nice.[(triple1)] The bald eagle likes the bear.[(triple2)] The bald eagle sees the cow.[(triple3)] The bald eagle sees the mouse.[(triple4)] The bear chases the mouse.[(triple5)] The bear is big.[(triple6)] The bear is nice.[(triple7)] The bear sees the bald eagle.[(triple8)] The cow chases the mouse.[(triple9)] The mouse chases the bald eagle.[(triple10)] The mouse does not see the cow.[(triple12)] The mouse is young.[(triple11)] @1: The mouse likes the bald eagle.[(((triple10) -> rule2))] @2: The bald eagle is big.[(((((triple10) -> rule2)) -> rule4))] @3: The bald eagle does not like the mouse.[(((((((triple10) -> rule2)) -> rule4) triple2) -> rule3))]
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
triple1
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
triple2
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
triple3
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
triple4
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple5
The bear is big.
("bear" "is" "big" "+")
triple6
The bear is nice.
("bear" "is" "nice" "+")
triple7
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
triple8
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple9
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
triple10
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple11
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
((triple10) -> (rule2 % int1))
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int1
The bald eagle is big.
("bald eagle" "is" "big" "+")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int2
The bald eagle does not like the mouse.
("bald eagle" "likes" "mouse" "-")
((((((triple10) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The bald eagle does not like the mouse.
("bald eagle" "likes" "mouse" "-")
int1
The bald eagle is big.
("bald eagle" "is" "big" "+")
int2
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
int3