The lion eats the mouse. The lion is big. The lion is blue. The lion is not cold. The lion is green. The lion is young. The lion visits the mouse. The mouse eats the lion. The mouse is blue. The mouse needs the lion. If someone is cold and young then they need the mouse. If someone needs the lion then they do not need the mouse. If someone is young then they need the lion. If someone is cold then they eat the lion. If the mouse eats the lion then the lion is young. If the mouse is young then the mouse eats the lion. If the lion eats the mouse and the lion is not green then the lion does not visit the mouse. If the lion does not need the mouse then the mouse is big.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The lion is green.
("lion" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If someone is cold and young then they need the mouse.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the lion then they do not need the mouse.
((("someone" "needs" "lion" "+")) -> ("someone" "needs" "mouse" "-"))
If someone is young then they need the lion.
((("someone" "is" "young" "+")) -> ("someone" "needs" "lion" "+"))
If someone is cold then they eat the lion.
((("someone" "is" "cold" "+")) -> ("someone" "eats" "lion" "+"))
If the mouse eats the lion then the lion is young.
((("mouse" "eats" "lion" "+")) -> ("lion" "is" "young" "+"))
If the mouse is young then the mouse eats the lion.
((("mouse" "is" "young" "+")) -> ("mouse" "eats" "lion" "+"))
If the lion eats the mouse and the lion is not green then the lion does not visit the mouse.
((("lion" "eats" "mouse" "+") ("lion" "is" "green" "~")) -> ("lion" "visits" "mouse" "-"))
If the lion does not need the mouse then the mouse is big.
((("lion" "needs" "mouse" "~")) -> ("mouse" "is" "big" "+"))
The mouse needs the lion.
True
1
proof
[(triple10)]
("mouse" "needs" "lion" "+")
triple10
The lion is not young.
False
1
inv-proof
[(triple6 OR ((triple8) -> rule5))]
("lion" "is" "young" "-")
triple6
((triple8) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the lion.
True
2
proof
[(((triple6) -> rule3) OR ((((triple8) -> rule5)) -> rule3))]
("lion" "needs" "lion" "+")
((triple6) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The mouse needs the mouse.
False
2
inv-proof
[(((triple10) -> rule2))]
("mouse" "needs" "mouse" "+")
((triple10) -> (rule2 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The lion does not need the mouse.
True
3
proof
[(((((triple6) -> rule3)) -> rule2) OR ((((((triple8) -> rule5)) -> rule3)) -> rule2))]
("lion" "needs" "mouse" "-")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion needs the mouse.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule2) OR ((((((triple8) -> rule5)) -> rule3)) -> rule2))]
("lion" "needs" "mouse" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The mouse is big.
True
4
proof
[(((((((triple6) -> rule3)) -> rule2)) -> rule8) OR ((((((((triple8) -> rule5)) -> rule3)) -> rule2)) -> rule8))]
("mouse" "is" "big" "+")
((((((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
((((((((triple8) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The mouse is not big.
False
4
inv-proof
[(((((((triple6) -> rule3)) -> rule2)) -> rule8) OR ((((((((triple8) -> rule5)) -> rule3)) -> rule2)) -> rule8))]
("mouse" "is" "big" "-")
((((((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
((((((((triple8) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "lion" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse does not visit the lion.
Unknown
inv-random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The lion eats the mouse.[(triple1)] The lion is big.[(triple2)] The lion is blue.[(triple3)] The lion is green.[(triple5)] The lion is not cold.[(triple4)] The lion is young.[(triple6 OR ((triple8) -> rule5))] The lion visits the mouse.[(triple7)] The mouse eats the lion.[(triple8)] The mouse is blue.[(triple9)] The mouse needs the lion.[(triple10)] @1: The lion needs the lion.[(((triple6) -> rule3) OR ((((triple8) -> rule5)) -> rule3))] The mouse does not need the mouse.[(((triple10) -> rule2))] @2: The lion does not need the mouse.[(((((triple6) -> rule3)) -> rule2) OR ((((((triple8) -> rule5)) -> rule3)) -> rule2))] @3: The mouse is big.[(((((((triple6) -> rule3)) -> rule2)) -> rule8) OR ((((((((triple8) -> rule5)) -> rule3)) -> rule2)) -> rule8))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple5
The lion is not cold.
("lion" "is" "cold" "-")
triple4
The lion is young.
("lion" "is" "young" "+")
triple6
((triple8) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple7
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple10
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple6) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
((triple10) -> (rule2 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
((((((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
((((((((triple8) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion does not need the mouse.
("lion" "needs" "mouse" "-")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4