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