The bald eagle visits the cow. The cow needs the mouse. The mouse chases the cow. If something chases the bald eagle and the bald eagle visits the mouse then it is kind. If something chases the bald eagle and the bald eagle visits the cow then it is green. If something chases the cow then it chases the bald eagle.
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
If something chases the bald eagle and the bald eagle visits the mouse then it is kind.
((("something" "chases" "bald eagle" "+") ("bald eagle" "visits" "mouse" "+")) -> ("something" "is" "kind" "+"))
If something chases the bald eagle and the bald eagle visits the cow then it is green.
((("something" "chases" "bald eagle" "+") ("bald eagle" "visits" "cow" "+")) -> ("something" "is" "green" "+"))
If something chases the cow then it chases the bald eagle.
((("something" "chases" "cow" "+")) -> ("something" "chases" "bald eagle" "+"))
The cow needs the mouse.
True
1
proof
[(triple2)]
("cow" "needs" "mouse" "+")
triple2
The cow does not need the mouse.
False
1
inv-proof
[(triple2)]
("cow" "needs" "mouse" "-")
triple2
The mouse chases the bald eagle.
True
2
proof
[(((triple3) -> rule3))]
("mouse" "chases" "bald eagle" "+")
((triple3) -> (rule3 % int1))
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int1
The mouse does not chase the bald eagle.
False
2
inv-proof
[(((triple3) -> rule3))]
("mouse" "chases" "bald eagle" "-")
((triple3) -> (rule3 % int1))
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int1
The mouse is green.
True
4
proof
[(((((triple3) -> rule3) triple1) -> rule2))]
("mouse" "is" "green" "+")
((((triple3) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int2
The mouse is not green.
False
4
inv-proof
[(((((triple3) -> rule3) triple1) -> rule2))]
("mouse" "is" "green" "-")
((((triple3) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int2
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "kind" "-")
The bald eagle is kind.
Unknown
rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "kind" "+")
The bald eagle is not green.
Unknown
inv-rconc
[@2: The bald eagle is green.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("bald eagle" "is" "green" "-")
The bald eagle visits the mouse.
Unknown
random
[@0: The bald eagle visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "mouse" "+")
The mouse does not visit the bald eagle.
Unknown
inv-random
[@0: The mouse visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bald eagle" "-")
The bald eagle chases the mouse.
Unknown
random
[@0: The bald eagle chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "mouse" "+")
@0: The bald eagle visits the cow.[(triple1)] The cow needs the mouse.[(triple2)] The mouse chases the cow.[(triple3)] @1: The mouse chases the bald eagle.[(((triple3) -> rule3))] @2: The mouse is green.[(((((triple3) -> rule3) triple1) -> rule2))]
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
triple1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple3
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
((triple3) -> (rule3 % int1))
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple3) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int2