The bald eagle is green. The mouse needs the bald eagle. The tiger sees the bald eagle. If someone sees the tiger then the tiger sees the mouse. If someone sees the bald eagle then they see the mouse. If the mouse needs the tiger and the mouse visits the tiger then the tiger visits the bald eagle. If someone is young then they see the mouse. If someone sees the mouse then they need the tiger. If the mouse sees the bald eagle and the mouse is nice then the mouse sees the tiger.
The bald eagle is green.
("bald eagle" "is" "green" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
If someone sees the tiger then the tiger sees the mouse.
((("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If someone sees the bald eagle then they see the mouse.
((("someone" "sees" "bald eagle" "+")) -> ("someone" "sees" "mouse" "+"))
If the mouse needs the tiger and the mouse visits the tiger then the tiger visits the bald eagle.
((("mouse" "needs" "tiger" "+") ("mouse" "visits" "tiger" "+")) -> ("tiger" "visits" "bald eagle" "+"))
If someone is young then they see the mouse.
((("someone" "is" "young" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the mouse then they need the tiger.
((("someone" "sees" "mouse" "+")) -> ("someone" "needs" "tiger" "+"))
If the mouse sees the bald eagle and the mouse is nice then the mouse sees the tiger.
((("mouse" "sees" "bald eagle" "+") ("mouse" "is" "nice" "+")) -> ("mouse" "sees" "tiger" "+"))
The mouse needs the bald eagle.
True
1
proof
[(triple2)]
("mouse" "needs" "bald eagle" "+")
triple2
The tiger does not see the bald eagle.
False
1
inv-proof
[(triple3)]
("tiger" "sees" "bald eagle" "-")
triple3
The tiger sees the mouse.
True
2
proof
[(((triple3) -> rule2))]
("tiger" "sees" "mouse" "+")
((triple3) -> (rule2 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger does not see the mouse.
False
2
inv-proof
[(((triple3) -> rule2))]
("tiger" "sees" "mouse" "-")
((triple3) -> (rule2 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger needs the tiger.
True
3
proof
[(((((triple3) -> rule2)) -> rule5))]
("tiger" "needs" "tiger" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The tiger does not need the tiger.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule5))]
("tiger" "needs" "tiger" "-")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The tiger visits the bald eagle.
Unknown
rconc
[@1: The tiger visits the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "bald eagle" "+")
The bald eagle does not see the mouse.
Unknown
inv-rconc
[@1: The bald eagle sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "sees" "mouse" "-")
The tiger visits the mouse.
Unknown
random
[@0: The tiger visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "mouse" "+")
The bald eagle is not red.
Unknown
inv-random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The bald eagle is green.[(triple1)] The mouse needs the bald eagle.[(triple2)] The tiger sees the bald eagle.[(triple3)] @1: The tiger sees the mouse.[(((triple3) -> rule2))] @2: The tiger needs the tiger.[(((((triple3) -> rule2)) -> rule5))]
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple1
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
triple3
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((triple3) -> (rule2 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2