The bald eagle is cold. The bald eagle is rough. The bald eagle sees the mouse. The bear chases the cow. The cow chases the mouse. The mouse is cold. The mouse is rough. If something needs the mouse and it sees the cow then the mouse is cold. If something is green then it is red. If something needs the cow and the cow chases the bald eagle then the cow is round. If something chases the cow then it needs the bear. If something sees the mouse then the mouse needs the bald eagle. If something needs the bald eagle then it sees the cow. If something needs the bald eagle then the bald eagle sees the bear. If something chases the mouse then it is cold.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
The bear chases the cow.
("bear" "chases" "cow" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
If something needs the mouse and it sees the cow then the mouse is cold.
((("something" "needs" "mouse" "+") ("something" "sees" "cow" "+")) -> ("mouse" "is" "cold" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something needs the cow and the cow chases the bald eagle then the cow is round.
((("something" "needs" "cow" "+") ("cow" "chases" "bald eagle" "+")) -> ("cow" "is" "round" "+"))
If something chases the cow then it needs the bear.
((("something" "chases" "cow" "+")) -> ("something" "needs" "bear" "+"))
If something sees the mouse then the mouse needs the bald eagle.
((("something" "sees" "mouse" "+")) -> ("mouse" "needs" "bald eagle" "+"))
If something needs the bald eagle then it sees the cow.
((("something" "needs" "bald eagle" "+")) -> ("something" "sees" "cow" "+"))
If something needs the bald eagle then the bald eagle sees the bear.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "sees" "bear" "+"))
If something chases the mouse then it is cold.
((("something" "chases" "mouse" "+")) -> ("something" "is" "cold" "+"))
The bald eagle is cold.
True
1
proof
[(triple1)]
("bald eagle" "is" "cold" "+")
triple1
The bear does not chase the cow.
False
1
inv-proof
[(triple4)]
("bear" "chases" "cow" "-")
triple4
The bear needs the bear.
True
2
proof
[(((triple4) -> rule4))]
("bear" "needs" "bear" "+")
((triple4) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple4) -> rule4))]
("bear" "needs" "bear" "-")
((triple4) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The mouse sees the cow.
True
3
proof
[(((((triple3) -> rule5)) -> rule6))]
("mouse" "sees" "cow" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int2
The mouse does not see the cow.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule6))]
("mouse" "sees" "cow" "-")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int2
The mouse does not need the bear.
Unknown
inv-rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "bear" "-")
The bald eagle is red.
Unknown
rconc
[@1: The bald eagle is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "red" "+")
The bear is not red.
Unknown
inv-rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "red" "-")
The bear needs the mouse.
Unknown
random
[@0: The bear needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "mouse" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
@0: The bald eagle is cold.[(triple1)] The bald eagle is rough.[(triple2)] The bald eagle sees the mouse.[(triple3)] The bear chases the cow.[(triple4)] The cow chases the mouse.[(triple5)] The mouse is cold.[(triple6)] The mouse is rough.[(triple7)] @1: The bear needs the bear.[(((triple4) -> rule4))] The cow is cold.[(((triple5) -> rule8))] The mouse needs the bald eagle.[(((triple3) -> rule5))] @2: The bald eagle sees the bear.[(((((triple3) -> rule5)) -> rule7))] The mouse sees the cow.[(((((triple3) -> rule5)) -> rule6))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple2
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
triple3
The bear chases the cow.
("bear" "chases" "cow" "+")
triple4
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple5
The mouse is cold.
("mouse" "is" "cold" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple4) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple5) -> (rule8 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
((triple3) -> (rule5 % int1))
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int1
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int1
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int2