The bald eagle chases the mouse. The bald eagle chases the tiger. The bald eagle needs the mouse. The bald eagle needs the tiger. The mouse chases the tiger. The mouse sees the tiger. The tiger chases the bald eagle. The tiger chases the mouse. The tiger is big. The tiger is green. The tiger is red. The tiger needs the bald eagle. The tiger needs the mouse. The tiger sees the bald eagle. The tiger sees the mouse. If someone needs the tiger then they see the mouse. If someone is round then they are green. If someone chases the tiger then the tiger sees the mouse.
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger chases the bald eagle.
("tiger" "chases" "bald eagle" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If someone needs the tiger then they see the mouse.
((("someone" "needs" "tiger" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone chases the tiger then the tiger sees the mouse.
((("someone" "chases" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
The tiger sees the mouse.
True
1
proof
[(triple15 OR ((triple2) -> rule3) OR ((triple5) -> rule3))]
("tiger" "sees" "mouse" "+")
triple15
((triple2) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
((triple5) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The bald eagle does not chase the tiger.
False
1
inv-proof
[(triple2)]
("bald eagle" "chases" "tiger" "-")
triple2
The bald eagle sees the mouse.
True
2
proof
[(((triple4) -> rule1))]
("bald eagle" "sees" "mouse" "+")
((triple4) -> (rule1 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The bald eagle does not see the mouse.
False
2
inv-proof
[(((triple4) -> rule1))]
("bald eagle" "sees" "mouse" "-")
((triple4) -> (rule1 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The bald eagle is green.
Unknown
rconc
[@1: The bald eagle is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "green" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The mouse sees the bald eagle.
Unknown
random
[@0: The mouse sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bald eagle" "+")
@0: The bald eagle chases the mouse.[(triple1)] The bald eagle chases the tiger.[(triple2)] The bald eagle needs the mouse.[(triple3)] The bald eagle needs the tiger.[(triple4)] The mouse chases the tiger.[(triple5)] The mouse sees the tiger.[(triple6)] The tiger chases the bald eagle.[(triple7)] The tiger chases the mouse.[(triple8)] The tiger is big.[(triple9)] The tiger is green.[(triple10)] The tiger is red.[(triple11)] The tiger needs the bald eagle.[(triple12)] The tiger needs the mouse.[(triple13)] The tiger sees the bald eagle.[(triple14)] The tiger sees the mouse.[(triple15 OR ((triple2) -> rule3) OR ((triple5) -> rule3))] @1: The bald eagle sees the mouse.[(((triple4) -> rule1))]
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
triple2
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple3
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
triple4
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple5
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple6
The tiger chases the bald eagle.
("tiger" "chases" "bald eagle" "+")
triple7
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
triple12
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple13
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15
((triple2) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
((triple5) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
((triple4) -> (rule1 % int1))
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
int1