The bald eagle is not kind. The bald eagle does not visit the mouse. The mouse visits the bald eagle. If the bald eagle likes the mouse then the mouse is not young. If something likes the mouse and it is young then the mouse is red. If something likes the mouse then it does not eat the bald eagle. If the bald eagle visits the mouse and the mouse is kind then the bald eagle does not like the mouse. If something visits the bald eagle then it likes the mouse. If something is kind and it likes the bald eagle then the bald eagle eats the mouse. If the mouse does not eat the bald eagle then the mouse is rough. If something is rough then it does not like the bald eagle.
The bald eagle is not kind.
("bald eagle" "is" "kind" "-")
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
If the bald eagle likes the mouse then the mouse is not young.
((("bald eagle" "likes" "mouse" "+")) -> ("mouse" "is" "young" "-"))
If something likes the mouse and it is young then the mouse is red.
((("something" "likes" "mouse" "+") ("something" "is" "young" "+")) -> ("mouse" "is" "red" "+"))
If something likes the mouse then it does not eat the bald eagle.
((("something" "likes" "mouse" "+")) -> ("something" "eats" "bald eagle" "-"))
If the bald eagle visits the mouse and the mouse is kind then the bald eagle does not like the mouse.
((("bald eagle" "visits" "mouse" "+") ("mouse" "is" "kind" "+")) -> ("bald eagle" "likes" "mouse" "-"))
If something visits the bald eagle then it likes the mouse.
((("something" "visits" "bald eagle" "+")) -> ("something" "likes" "mouse" "+"))
If something is kind and it likes the bald eagle then the bald eagle eats the mouse.
((("something" "is" "kind" "+") ("something" "likes" "bald eagle" "+")) -> ("bald eagle" "eats" "mouse" "+"))
If the mouse does not eat the bald eagle then the mouse is rough.
((("mouse" "eats" "bald eagle" "~")) -> ("mouse" "is" "rough" "+"))
If something is rough then it does not like the bald eagle.
((("something" "is" "rough" "+")) -> ("something" "likes" "bald eagle" "-"))
The mouse visits the bald eagle.
True
1
proof
[(triple3)]
("mouse" "visits" "bald eagle" "+")
triple3
The bald eagle is kind.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "kind" "+")
triple1
The mouse likes the mouse.
True
2
proof
[(((triple3) -> rule5))]
("mouse" "likes" "mouse" "+")
((triple3) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple3) -> rule5))]
("mouse" "likes" "mouse" "-")
((triple3) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not eat the bald eagle.
True
3
proof
[(((((triple3) -> rule5)) -> rule3))]
("mouse" "eats" "bald eagle" "-")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The mouse does not eat the bald eagle.
("mouse" "eats" "bald eagle" "-")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse eats the bald eagle.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule3))]
("mouse" "eats" "bald eagle" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The mouse does not eat the bald eagle.
("mouse" "eats" "bald eagle" "-")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse is rough.
True
4
proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule7))]
("mouse" "is" "rough" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse does not eat the bald eagle.
("mouse" "eats" "bald eagle" "-")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse is not rough.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule7))]
("mouse" "is" "rough" "-")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse does not eat the bald eagle.
("mouse" "eats" "bald eagle" "-")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "red" "-")
The bald eagle eats the mouse.
Unknown
rconc
[@1: The bald eagle eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "eats" "mouse" "+")
The bald eagle does not like the mouse.
Unknown
inv-rconc
[@1: The bald eagle likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "likes" "mouse" "-")
The bald eagle is red.
Unknown
random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "+")
The bald eagle is not young.
Unknown
inv-random
[@0: The bald eagle is young.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "young" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The bald eagle does not visit the mouse.[(triple2)] The bald eagle is not kind.[(triple1)] The mouse visits the bald eagle.[(triple3)] @1: The mouse likes the mouse.[(((triple3) -> rule5))] @2: The mouse does not eat the bald eagle.[(((((triple3) -> rule5)) -> rule3))] @3: The mouse is rough.[(((((((triple3) -> rule5)) -> rule3)) -> rule7))] @4: The mouse does not like the bald eagle.[(((((((((triple3) -> rule5)) -> rule3)) -> rule7)) -> rule8))]
The bald eagle does not visit the mouse.
("bald eagle" "visits" "mouse" "-")
triple2
The bald eagle is not kind.
("bald eagle" "is" "kind" "-")
triple1
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
triple3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple3) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not eat the bald eagle.
("mouse" "eats" "bald eagle" "-")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The mouse does not eat the bald eagle.
("mouse" "eats" "bald eagle" "-")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse does not eat the bald eagle.
("mouse" "eats" "bald eagle" "-")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse does not like the bald eagle.
("mouse" "likes" "bald eagle" "-")
((((((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The mouse does not like the bald eagle.
("mouse" "likes" "bald eagle" "-")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not eat the bald eagle.
("mouse" "eats" "bald eagle" "-")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int4