The bald eagle sees the mouse. The bear sees the rabbit. The mouse sees the bald eagle. The rabbit is rough. If the bald eagle sees the rabbit then the rabbit eats the bear. If something sees the rabbit then it sees the bald eagle. If the mouse visits the bear then the bear is blue.
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
If the bald eagle sees the rabbit then the rabbit eats the bear.
((("bald eagle" "sees" "rabbit" "+")) -> ("rabbit" "eats" "bear" "+"))
If something sees the rabbit then it sees the bald eagle.
((("something" "sees" "rabbit" "+")) -> ("something" "sees" "bald eagle" "+"))
If the mouse visits the bear then the bear is blue.
((("mouse" "visits" "bear" "+")) -> ("bear" "is" "blue" "+"))
The mouse sees the bald eagle.
True
1
proof
[(triple3)]
("mouse" "sees" "bald eagle" "+")
triple3
The bald eagle does not see the mouse.
False
1
inv-proof
[(triple1)]
("bald eagle" "sees" "mouse" "-")
triple1
The bear sees the bald eagle.
True
2
proof
[(((triple2) -> rule2))]
("bear" "sees" "bald eagle" "+")
((triple2) -> (rule2 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bear does not see the bald eagle.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "sees" "bald eagle" "-")
((triple2) -> (rule2 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "blue" "-")
The rabbit eats the bear.
Unknown
rconc
[@1: The rabbit eats the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "bear" "+")
The rabbit does not visit the bear.
Unknown
inv-random
[@0: The rabbit visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "bear" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
@0: The bald eagle sees the mouse.[(triple1)] The bear sees the rabbit.[(triple2)] The mouse sees the bald eagle.[(triple3)] The rabbit is rough.[(triple4)] @1: The bear sees the bald eagle.[(((triple2) -> rule2))]
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
triple1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple2
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
triple3
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple4
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
((triple2) -> (rule2 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1