The bald eagle needs the mouse. The lion likes the bald eagle. The mouse chases the lion. If something is big then it chases the mouse. If the bald eagle is young then the bald eagle chases the lion. If something needs the mouse then the mouse needs the bald eagle. If something chases the lion then the lion needs the mouse. If something needs the mouse then the mouse is big. If something is big then it is green.
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
If something is big then it chases the mouse.
((("something" "is" "big" "+")) -> ("something" "chases" "mouse" "+"))
If the bald eagle is young then the bald eagle chases the lion.
((("bald eagle" "is" "young" "+")) -> ("bald eagle" "chases" "lion" "+"))
If something needs the mouse then the mouse needs the bald eagle.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "bald eagle" "+"))
If something chases the lion then the lion needs the mouse.
((("something" "chases" "lion" "+")) -> ("lion" "needs" "mouse" "+"))
If something needs the mouse then the mouse is big.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
The lion likes the bald eagle.
True
1
proof
[(triple2)]
("lion" "likes" "bald eagle" "+")
triple2
The mouse does not chase the lion.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "lion" "-")
triple3
The mouse needs the bald eagle.
True
2
proof
[(((triple1) -> rule3) OR ((((triple3) -> rule4)) -> rule3))]
("mouse" "needs" "bald eagle" "+")
((triple1) -> (rule3 % int1))
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The mouse does not need the bald eagle.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple3) -> rule4)) -> rule3))]
("mouse" "needs" "bald eagle" "-")
((triple1) -> (rule3 % int1))
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The bald eagle does not chase the lion.
Unknown
inv-rconc
[@1: The bald eagle chases the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "chases" "lion" "-")
The lion is green.
Unknown
rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "green" "+")
The lion does not like the mouse.
Unknown
inv-random
[@0: The lion likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "mouse" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The bald eagle needs the mouse.[(triple1)] The lion likes the bald eagle.[(triple2)] The mouse chases the lion.[(triple3)] @1: The lion needs the mouse.[(((triple3) -> rule4))] The mouse is big.[(((triple1) -> rule5) OR ((((triple3) -> rule4)) -> rule5))] The mouse needs the bald eagle.[(((triple1) -> rule3) OR ((((triple3) -> rule4)) -> rule3))] @2: The mouse chases the mouse.[(((((triple1) -> rule5)) -> rule1) OR ((((((triple3) -> rule4)) -> rule5)) -> rule1))] The mouse is green.[(((((triple1) -> rule5)) -> rule6) OR ((((((triple3) -> rule4)) -> rule5)) -> rule6))]
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple1
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
triple2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((triple3) -> (rule4 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((triple1) -> (rule5 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
((triple1) -> (rule3 % int1))
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The mouse is green.
("mouse" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3