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