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