The bald eagle is cold. The bald eagle is green. The lion needs the mouse. The lion sees the bald eagle. The mouse is green. The mouse sees the tiger. The tiger is round. If someone is red and rough then they see the tiger. If someone sees the tiger then they see the lion. If someone chases the mouse then the mouse sees the lion. If someone needs the bald eagle and they chase the mouse then they see the lion. If someone is green then they see the tiger. If someone needs the lion then they are cold.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle is green.
("bald eagle" "is" "green" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone is red and rough then they see the tiger.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "sees" "tiger" "+"))
If someone sees the tiger then they see the lion.
((("someone" "sees" "tiger" "+")) -> ("someone" "sees" "lion" "+"))
If someone chases the mouse then the mouse sees the lion.
((("someone" "chases" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
If someone needs the bald eagle and they chase the mouse then they see the lion.
((("someone" "needs" "bald eagle" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "sees" "lion" "+"))
If someone is green then they see the tiger.
((("someone" "is" "green" "+")) -> ("someone" "sees" "tiger" "+"))
If someone needs the lion then they are cold.
((("someone" "needs" "lion" "+")) -> ("someone" "is" "cold" "+"))
The lion sees the bald eagle.
True
1
proof
[(triple4)]
("lion" "sees" "bald eagle" "+")
triple4
The lion does not need the mouse.
False
1
inv-proof
[(triple3)]
("lion" "needs" "mouse" "-")
triple3
The mouse sees the lion.
True
2
proof
[(((triple6) -> rule2) OR ((((triple5) -> rule5)) -> rule2))]
("mouse" "sees" "lion" "+")
((triple6) -> (rule2 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The bald eagle does not see the tiger.
False
2
inv-proof
[(((triple2) -> rule5))]
("bald eagle" "sees" "tiger" "-")
((triple2) -> (rule5 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The bald eagle sees the lion.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("bald eagle" "sees" "lion" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2
The bald eagle does not see the lion.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("bald eagle" "sees" "lion" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "cold" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "cold" "-")
The bald eagle chases the bald eagle.
Unknown
random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "+")
The mouse does not chase the tiger.
Unknown
inv-random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "-")
The mouse needs the tiger.
Unknown
random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "+")
@0: The bald eagle is cold.[(triple1)] The bald eagle is green.[(triple2)] The lion needs the mouse.[(triple3)] The lion sees the bald eagle.[(triple4)] The mouse is green.[(triple5)] The mouse sees the tiger.[(triple6 OR ((triple5) -> rule5))] The tiger is round.[(triple7)] @1: The bald eagle sees the tiger.[(((triple2) -> rule5))] The mouse sees the lion.[(((triple6) -> rule2) OR ((((triple5) -> rule5)) -> rule2))] @2: The bald eagle sees the lion.[(((((triple2) -> rule5)) -> rule2))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple3
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple5
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple6
((triple5) -> (rule5 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple7
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
((triple2) -> (rule5 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((triple6) -> (rule2 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2