============================== Mace4 ================================= Mace4 (32) version 2008-10A+, October 2008. Process 26918 was started by mccune on cleo, Thu Oct 30 20:06:22 2008 The command was "mace4 -n8 -m -1 -f queens1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file queens1.in set(integer_ring). set(order_domain). formulas(assumptions). x != z -> Q(x) != Q(z). x < z & Q(x) < Q(z) -> z -- x != Q(z) -- Q(x). x < z & Q(z) < Q(x) -> z -- x != Q(x) -- Q(z). end_of_list. % assign(domain_size, 8) -> assign(start_size, 8). % assign(domain_size, 8) -> assign(end_size, 8). % From the command line: assign(domain_size, 8). % From the command line: assign(max_models, -1). ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x != z -> Q(x) != Q(z) # label(non_clause). [assumption]. 2 x < z & Q(x) < Q(z) -> z -- x != Q(z) -- Q(x) # label(non_clause). [assumption]. 3 x < z & Q(z) < Q(x) -> z -- x != Q(x) -- Q(z) # label(non_clause). [assumption]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). x = y | Q(x) != Q(y). -(x < y) | -(Q(x) < Q(y)) | Q(y) -- Q(x) != y -- x. -(x < y) | -(Q(y) < Q(x)) | Q(x) -- Q(y) != y -- x. end_of_list. ============================== end of clauses for search ============= % There are no domain elements in the input. ============================== DOMAIN SIZE 8 ========================= Clearing flag lnh, because the least number heuristic is not compatible with flags integer_ring or order_domain. ============================== MODEL ================================= interpretation( 8, [number=1, seconds=0], [ function(Q(_), [ 0, 4, 7, 5, 2, 6, 1, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=2, seconds=0], [ function(Q(_), [ 0, 5, 7, 2, 6, 3, 1, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=3, seconds=0], [ function(Q(_), [ 0, 6, 3, 5, 7, 1, 4, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=4, seconds=0], [ function(Q(_), [ 0, 6, 4, 7, 1, 3, 5, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=5, seconds=0], [ function(Q(_), [ 1, 3, 5, 7, 2, 0, 6, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=6, seconds=0], [ function(Q(_), [ 1, 4, 6, 0, 2, 7, 5, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=7, seconds=0], [ function(Q(_), [ 1, 4, 6, 3, 0, 7, 5, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=8, seconds=0], [ function(Q(_), [ 1, 5, 0, 6, 3, 7, 2, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=9, seconds=0], [ function(Q(_), [ 1, 5, 7, 2, 0, 3, 6, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=10, seconds=0], [ function(Q(_), [ 1, 6, 2, 5, 7, 4, 0, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=11, seconds=0], [ function(Q(_), [ 1, 6, 4, 7, 0, 3, 5, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=12, seconds=0], [ function(Q(_), [ 1, 7, 5, 0, 2, 4, 6, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=13, seconds=0], [ function(Q(_), [ 2, 0, 6, 4, 7, 1, 3, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=14, seconds=0], [ function(Q(_), [ 2, 4, 1, 7, 0, 6, 3, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=15, seconds=0], [ function(Q(_), [ 2, 4, 1, 7, 5, 3, 6, 0 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=16, seconds=0], [ function(Q(_), [ 2, 4, 6, 0, 3, 1, 7, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=17, seconds=0], [ function(Q(_), [ 2, 4, 7, 3, 0, 6, 1, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=18, seconds=0], [ function(Q(_), [ 2, 5, 1, 4, 7, 0, 6, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=19, seconds=0], [ function(Q(_), [ 2, 5, 1, 6, 0, 3, 7, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=20, seconds=0], [ function(Q(_), [ 2, 5, 1, 6, 4, 0, 7, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=21, seconds=0], [ function(Q(_), [ 2, 5, 3, 0, 7, 4, 6, 1 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=22, seconds=0], [ function(Q(_), [ 2, 5, 3, 1, 7, 4, 6, 0 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=23, seconds=0], [ function(Q(_), [ 2, 5, 7, 0, 3, 6, 4, 1 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=24, seconds=0], [ function(Q(_), [ 2, 5, 7, 0, 4, 6, 1, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=25, seconds=0], [ function(Q(_), [ 2, 5, 7, 1, 3, 0, 6, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=26, seconds=0], [ function(Q(_), [ 2, 6, 1, 7, 4, 0, 3, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=27, seconds=0], [ function(Q(_), [ 2, 6, 1, 7, 5, 3, 0, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=28, seconds=0], [ function(Q(_), [ 2, 7, 3, 6, 0, 5, 1, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=29, seconds=0], [ function(Q(_), [ 3, 0, 4, 7, 1, 6, 2, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=30, seconds=0], [ function(Q(_), [ 3, 0, 4, 7, 5, 2, 6, 1 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=31, seconds=0], [ function(Q(_), [ 3, 1, 4, 7, 5, 0, 2, 6 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=32, seconds=0], [ function(Q(_), [ 3, 1, 6, 2, 5, 7, 0, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=33, seconds=0], [ function(Q(_), [ 3, 1, 6, 2, 5, 7, 4, 0 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=34, seconds=0], [ function(Q(_), [ 3, 1, 6, 4, 0, 7, 5, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=35, seconds=0], [ function(Q(_), [ 3, 1, 7, 4, 6, 0, 2, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=36, seconds=0], [ function(Q(_), [ 3, 1, 7, 5, 0, 2, 4, 6 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=37, seconds=0], [ function(Q(_), [ 3, 5, 0, 4, 1, 7, 2, 6 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=38, seconds=0], [ function(Q(_), [ 3, 5, 7, 1, 6, 0, 2, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=39, seconds=0], [ function(Q(_), [ 3, 5, 7, 2, 0, 6, 4, 1 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=40, seconds=0], [ function(Q(_), [ 3, 6, 0, 7, 4, 1, 5, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=41, seconds=0], [ function(Q(_), [ 3, 6, 2, 7, 1, 4, 0, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=42, seconds=0], [ function(Q(_), [ 3, 6, 4, 1, 5, 0, 2, 7 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=43, seconds=0], [ function(Q(_), [ 3, 6, 4, 2, 0, 5, 7, 1 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=44, seconds=0], [ function(Q(_), [ 3, 7, 0, 2, 5, 1, 6, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=45, seconds=0], [ function(Q(_), [ 3, 7, 0, 4, 6, 1, 5, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=46, seconds=0], [ function(Q(_), [ 3, 7, 4, 2, 0, 6, 1, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=47, seconds=0], [ function(Q(_), [ 4, 0, 3, 5, 7, 1, 6, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=48, seconds=0], [ function(Q(_), [ 4, 0, 7, 3, 1, 6, 2, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=49, seconds=0], [ function(Q(_), [ 4, 0, 7, 5, 2, 6, 1, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=50, seconds=0], [ function(Q(_), [ 4, 1, 3, 5, 7, 2, 0, 6 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=51, seconds=0], [ function(Q(_), [ 4, 1, 3, 6, 2, 7, 5, 0 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=52, seconds=0], [ function(Q(_), [ 4, 1, 5, 0, 6, 3, 7, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=53, seconds=0], [ function(Q(_), [ 4, 1, 7, 0, 3, 6, 2, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=54, seconds=0], [ function(Q(_), [ 4, 2, 0, 5, 7, 1, 3, 6 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=55, seconds=0], [ function(Q(_), [ 4, 2, 0, 6, 1, 7, 5, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=56, seconds=0], [ function(Q(_), [ 4, 2, 7, 3, 6, 0, 5, 1 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=57, seconds=0], [ function(Q(_), [ 4, 6, 0, 2, 7, 5, 3, 1 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=58, seconds=0], [ function(Q(_), [ 4, 6, 0, 3, 1, 7, 5, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=59, seconds=0], [ function(Q(_), [ 4, 6, 1, 3, 7, 0, 2, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=60, seconds=0], [ function(Q(_), [ 4, 6, 1, 5, 2, 0, 3, 7 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=61, seconds=0], [ function(Q(_), [ 4, 6, 1, 5, 2, 0, 7, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=62, seconds=0], [ function(Q(_), [ 4, 6, 3, 0, 2, 7, 5, 1 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=63, seconds=0], [ function(Q(_), [ 4, 7, 3, 0, 2, 5, 1, 6 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=64, seconds=0], [ function(Q(_), [ 4, 7, 3, 0, 6, 1, 5, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=65, seconds=0], [ function(Q(_), [ 5, 0, 4, 1, 7, 2, 6, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=66, seconds=0], [ function(Q(_), [ 5, 1, 6, 0, 2, 4, 7, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=67, seconds=0], [ function(Q(_), [ 5, 1, 6, 0, 3, 7, 4, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=68, seconds=0], [ function(Q(_), [ 5, 2, 0, 6, 4, 7, 1, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=69, seconds=0], [ function(Q(_), [ 5, 2, 0, 7, 3, 1, 6, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=70, seconds=0], [ function(Q(_), [ 5, 2, 0, 7, 4, 1, 3, 6 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=71, seconds=0], [ function(Q(_), [ 5, 2, 4, 6, 0, 3, 1, 7 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=72, seconds=0], [ function(Q(_), [ 5, 2, 4, 7, 0, 3, 1, 6 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=73, seconds=0], [ function(Q(_), [ 5, 2, 6, 1, 3, 7, 0, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=74, seconds=0], [ function(Q(_), [ 5, 2, 6, 1, 7, 4, 0, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=75, seconds=0], [ function(Q(_), [ 5, 2, 6, 3, 0, 7, 1, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=76, seconds=0], [ function(Q(_), [ 5, 3, 0, 4, 7, 1, 6, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=77, seconds=0], [ function(Q(_), [ 5, 3, 1, 7, 4, 6, 0, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=78, seconds=0], [ function(Q(_), [ 5, 3, 6, 0, 2, 4, 1, 7 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=79, seconds=0], [ function(Q(_), [ 5, 3, 6, 0, 7, 1, 4, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=80, seconds=0], [ function(Q(_), [ 5, 7, 1, 3, 0, 6, 4, 2 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=81, seconds=0], [ function(Q(_), [ 6, 0, 2, 7, 5, 3, 1, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=82, seconds=0], [ function(Q(_), [ 6, 1, 3, 0, 7, 4, 2, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=83, seconds=0], [ function(Q(_), [ 6, 1, 5, 2, 0, 3, 7, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=84, seconds=0], [ function(Q(_), [ 6, 2, 0, 5, 7, 4, 1, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=85, seconds=0], [ function(Q(_), [ 6, 2, 7, 1, 4, 0, 5, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=86, seconds=0], [ function(Q(_), [ 6, 3, 1, 4, 7, 0, 2, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=87, seconds=0], [ function(Q(_), [ 6, 3, 1, 7, 5, 0, 2, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=88, seconds=0], [ function(Q(_), [ 6, 4, 2, 0, 5, 7, 1, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=89, seconds=0], [ function(Q(_), [ 7, 1, 3, 0, 6, 4, 2, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=90, seconds=0], [ function(Q(_), [ 7, 1, 4, 2, 0, 6, 3, 5 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=91, seconds=0], [ function(Q(_), [ 7, 2, 0, 5, 1, 4, 6, 3 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== MODEL ================================= interpretation( 8, [number=92, seconds=0], [ function(Q(_), [ 7, 3, 0, 2, 5, 1, 6, 4 ]), function(--(_,_), [ 0, 7, 6, 5, 4, 3, 2, 1, 1, 0, 7, 6, 5, 4, 3, 2, 2, 1, 0, 7, 6, 5, 4, 3, 3, 2, 1, 0, 7, 6, 5, 4, 4, 3, 2, 1, 0, 7, 6, 5, 5, 4, 3, 2, 1, 0, 7, 6, 6, 5, 4, 3, 2, 1, 0, 7, 7, 6, 5, 4, 3, 2, 1, 0 ]), relation(<(_,_), [ 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 8. Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds). Ground clauses: seen=192, kept=112. Selections=1653, assignments=13224, propagations=312, current_models=92. Rewrite_terms=402128, rewrite_bools=124864, indexes=0. Rules_from_neg_clauses=312, cross_offs=5500. ============================== end of statistics ===================== User_CPU=0.06, System_CPU=0.00, Wall_clock=0. Exiting with 92 models. Process 26918 exit (all_models) Thu Oct 30 20:06:22 2008 The process finished Thu Oct 30 20:06:22 2008