The bald eagle likes the cow. The bear is rough. The cow sees the bald eagle. If something sees the bald eagle then the bald eagle is cold. If something likes the cow and it sees the bear then the bear is cold. If something likes the bald eagle and it likes the cow then it sees the bald eagle. If something sees the bear then the bear is young. If something sees the bald eagle then it needs the bear. If something is green then it sees the bald eagle. If something likes the bald eagle and it needs the bear then the bald eagle needs the bear. If something is cold then it sees the cow.
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
The bear is rough.
("bear" "is" "rough" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
If something sees the bald eagle then the bald eagle is cold.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "is" "cold" "+"))
If something likes the cow and it sees the bear then the bear is cold.
((("something" "likes" "cow" "+") ("something" "sees" "bear" "+")) -> ("bear" "is" "cold" "+"))
If something likes the bald eagle and it likes the cow then it sees the bald eagle.
((("something" "likes" "bald eagle" "+") ("something" "likes" "cow" "+")) -> ("something" "sees" "bald eagle" "+"))
If something sees the bear then the bear is young.
((("something" "sees" "bear" "+")) -> ("bear" "is" "young" "+"))
If something sees the bald eagle then it needs the bear.
((("something" "sees" "bald eagle" "+")) -> ("something" "needs" "bear" "+"))
If something is green then it sees the bald eagle.
((("something" "is" "green" "+")) -> ("something" "sees" "bald eagle" "+"))
If something likes the bald eagle and it needs the bear then the bald eagle needs the bear.
((("something" "likes" "bald eagle" "+") ("something" "needs" "bear" "+")) -> ("bald eagle" "needs" "bear" "+"))
If something is cold then it sees the cow.
((("something" "is" "cold" "+")) -> ("something" "sees" "cow" "+"))
The bear is rough.
True
1
proof
[(triple2)]
("bear" "is" "rough" "+")
triple2
The bald eagle does not like the cow.
False
1
inv-proof
[(triple1)]
("bald eagle" "likes" "cow" "-")
triple1
The bald eagle is cold.
True
2
proof
[(((triple3) -> rule1))]
("bald eagle" "is" "cold" "+")
((triple3) -> (rule1 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The cow does not need the bear.
False
2
inv-proof
[(((triple3) -> rule5))]
("cow" "needs" "bear" "-")
((triple3) -> (rule5 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The bear is not cold.
Unknown
inv-rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "cold" "-")
The bald eagle needs the bear.
Unknown
rconc
[@2: The bald eagle needs the bear.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("bald eagle" "needs" "bear" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
@0: The bald eagle likes the cow.[(triple1)] The bear is rough.[(triple2)] The cow sees the bald eagle.[(triple3)] @1: The bald eagle is cold.[(((triple3) -> rule1))] The cow needs the bear.[(((triple3) -> rule5))] @2: The bald eagle sees the cow.[(((((triple3) -> rule1)) -> rule8))]
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple3
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
((triple3) -> (rule1 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
((triple3) -> (rule5 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The bald eagle sees the cow.
("bald eagle" "sees" "cow" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2