The bald eagle needs the mouse. The cow sees the mouse. The mouse sees the cow. If someone is round then they are big. If someone needs the mouse then they see the mouse. If the bald eagle sees the cow then the bald eagle does not see the mouse. If the cow sees the bald eagle then the cow is not blue. If someone sees the mouse then they are cold. If someone is cold and they do not need the cow then the cow needs the mouse.
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone needs the mouse then they see the mouse.
((("someone" "needs" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
If the bald eagle sees the cow then the bald eagle does not see the mouse.
((("bald eagle" "sees" "cow" "+")) -> ("bald eagle" "sees" "mouse" "-"))
If the cow sees the bald eagle then the cow is not blue.
((("cow" "sees" "bald eagle" "+")) -> ("cow" "is" "blue" "-"))
If someone sees the mouse then they are cold.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and they do not need the cow then the cow needs the mouse.
((("someone" "is" "cold" "+") ("someone" "needs" "cow" "~")) -> ("cow" "needs" "mouse" "+"))
The mouse sees the cow.
True
1
proof
[(triple3)]
("mouse" "sees" "cow" "+")
triple3
The mouse does not see the cow.
False
1
inv-proof
[(triple3)]
("mouse" "sees" "cow" "-")
triple3
The bald eagle sees the mouse.
True
2
proof
[(((triple1) -> rule2))]
("bald eagle" "sees" "mouse" "+")
((triple1) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The bald eagle does not see the mouse.
False
2
inv-proof
[(((triple1) -> rule2))]
("bald eagle" "sees" "mouse" "-")
((triple1) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The bald eagle is cold.
True
3
proof
[(((((triple1) -> rule2)) -> rule5))]
("bald eagle" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int2
The bald eagle is not cold.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("bald eagle" "is" "cold" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int2
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "big" "-")
The bald eagle is big.
Unknown
rconc
[@1: The bald eagle is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "big" "+")
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The bald eagle is blue.
Unknown
random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "+")
The cow does not need the bald eagle.
Unknown
inv-random
[@0: The cow needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bald eagle" "-")
The bald eagle likes the cow.
Unknown
random
[@0: The bald eagle likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "cow" "+")
@0: The bald eagle needs the mouse.[(triple1)] The cow sees the mouse.[(triple2)] The mouse sees the cow.[(triple3)] @1: The bald eagle sees the mouse.[(((triple1) -> rule2))] The cow is cold.[(((triple2) -> rule5))] @2: The bald eagle is cold.[(((((triple1) -> rule2)) -> rule5))]
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple3
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
((triple1) -> (rule2 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int2