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