The lion chases the mouse. The lion is big. The mouse eats the lion. If something sees the lion and it is red then the lion sees the mouse. If something chases the mouse then it eats the lion. If something eats the lion and the lion eats the mouse then it eats the mouse. If something eats the lion then the lion sees the mouse. If something chases the mouse then it is red. If something is red and young then it sees the mouse. If the lion sees the mouse and the lion chases the mouse then the mouse sees the lion. If something chases the mouse and it eats the lion then it is red.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is big.
("lion" "is" "big" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
If something sees the lion and it is red then the lion sees the mouse.
((("something" "sees" "lion" "+") ("something" "is" "red" "+")) -> ("lion" "sees" "mouse" "+"))
If something chases the mouse then it eats the lion.
((("something" "chases" "mouse" "+")) -> ("something" "eats" "lion" "+"))
If something eats the lion and the lion eats the mouse then it eats the mouse.
((("something" "eats" "lion" "+") ("lion" "eats" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
If something eats the lion then the lion sees the mouse.
((("something" "eats" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If something chases the mouse then it is red.
((("something" "chases" "mouse" "+")) -> ("something" "is" "red" "+"))
If something is red and young then it sees the mouse.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "sees" "mouse" "+"))
If the lion sees the mouse and the lion chases the mouse then the mouse sees the lion.
((("lion" "sees" "mouse" "+") ("lion" "chases" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
If something chases the mouse and it eats the lion then it is red.
((("something" "chases" "mouse" "+") ("something" "eats" "lion" "+")) -> ("something" "is" "red" "+"))
The mouse eats the lion.
True
1
proof
[(triple3)]
("mouse" "eats" "lion" "+")
triple3
The mouse does not eat the lion.
False
1
inv-proof
[(triple3)]
("mouse" "eats" "lion" "-")
triple3
The lion eats the lion.
True
2
proof
[(((triple1) -> rule2))]
("lion" "eats" "lion" "+")
((triple1) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is not red.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple1 ((triple1) -> rule2)) -> rule8))]
("lion" "is" "red" "-")
((triple1) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple1 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The mouse sees the lion.
True
4
proof
[(((((triple3) -> rule4) triple1) -> rule7) OR ((((((triple1) -> rule2)) -> rule4) triple1) -> rule7))]
("mouse" "sees" "lion" "+")
((((triple3) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The mouse does not see the lion.
False
4
inv-proof
[(((((triple3) -> rule4) triple1) -> rule7) OR ((((((triple1) -> rule2)) -> rule4) triple1) -> rule7))]
("mouse" "sees" "lion" "-")
((((triple3) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The lion eats the mouse.
Unknown
rconc
[@1: The lion eats the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "mouse" "+")
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "red" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The lion chases the mouse.[(triple1)] The lion is big.[(triple2)] The mouse eats the lion.[(triple3)] @1: The lion eats the lion.[(((triple1) -> rule2))] The lion is red.[(((triple1) -> rule5) OR ((triple1 ((triple1) -> rule2)) -> rule8))] The lion sees the mouse.[(((triple3) -> rule4) OR ((((triple1) -> rule2)) -> rule4))] @2: The mouse sees the lion.[(((((triple3) -> rule4) triple1) -> rule7) OR ((((((triple1) -> rule2)) -> rule4) triple1) -> rule7))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple3
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple1) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((triple1) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple1 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
((triple3) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((((triple3) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3