The lion eats the mouse. The lion is not big. The lion is blue. The lion is green. The lion is rough. The lion is young. The lion needs the mouse. The lion visits the mouse. The mouse eats the lion. The mouse is blue. The mouse is green. The mouse is rough. The mouse is young. The mouse needs the lion. The mouse visits the lion. If someone eats the lion and they need the mouse then the lion is blue. If someone needs the lion then the lion is blue. If someone visits the lion then the lion visits the mouse. If someone is young then they need the lion. If someone eats the lion then the lion is green. If someone needs the lion then they visit the mouse.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
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 is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone eats the lion and they need the mouse then the lion is blue.
((("someone" "eats" "lion" "+") ("someone" "needs" "mouse" "+")) -> ("lion" "is" "blue" "+"))
If someone needs the lion then the lion is blue.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "blue" "+"))
If someone visits the lion then the lion visits the mouse.
((("someone" "visits" "lion" "+")) -> ("lion" "visits" "mouse" "+"))
If someone is young then they need the lion.
((("someone" "is" "young" "+")) -> ("someone" "needs" "lion" "+"))
If someone eats the lion then the lion is green.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If someone needs the lion then they visit the mouse.
((("someone" "needs" "lion" "+")) -> ("someone" "visits" "mouse" "+"))
The mouse visits the lion.
True
1
proof
[(triple15)]
("mouse" "visits" "lion" "+")
triple15
The mouse is not young.
False
1
inv-proof
[(triple13)]
("mouse" "is" "young" "-")
triple13
The lion needs the lion.
True
2
proof
[(((triple6) -> rule4))]
("lion" "needs" "lion" "+")
((triple6) -> (rule4 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple14) -> rule6) OR ((((triple13) -> rule4)) -> rule6))]
("mouse" "visits" "mouse" "-")
((triple14) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "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 blue.[(triple3 OR ((triple14) -> rule2) OR ((((triple13) -> rule4)) -> rule2) OR ((((triple6) -> rule4)) -> rule2))] The lion is green.[(triple4 OR ((triple9) -> rule5))] The lion is not big.[(triple2)] The lion is rough.[(triple5)] The lion is young.[(triple6)] The lion needs the mouse.[(triple7)] The lion visits the mouse.[(triple8 OR ((triple15) -> rule3) OR ((((triple6) -> rule4)) -> rule6))] The mouse eats the lion.[(triple9)] The mouse is blue.[(triple10)] The mouse is green.[(triple11)] The mouse is rough.[(triple12)] The mouse is young.[(triple13)] The mouse needs the lion.[(triple14 OR ((triple13) -> rule4))] The mouse visits the lion.[(triple15)] @1: The lion needs the lion.[(((triple6) -> rule4))] The mouse visits the mouse.[(((triple14) -> rule6) OR ((((triple13) -> rule4)) -> rule6))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple3
((triple14) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
triple4
((triple9) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is not big.
("lion" "is" "big" "-")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple7
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple8
((triple15) -> (rule3 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse is rough.
("mouse" "is" "rough" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple13
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple14
((triple13) -> (rule4 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple15
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple6) -> (rule4 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple14) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule6 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2