/**
 * Copyright 2016, Auctionomics, Alexandre Fréchette, Neil Newman, Kevin Leyton-Brown.
 *
 * This file is part of SATFC.
 *
 * SATFC is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * SATFC is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with SATFC.  If not, see <http://www.gnu.org/licenses/>.
 *
 * For questions, contact us at:
 * afrechet@cs.ubc.ca
 */
package ca.ubc.cs.beta.stationpacking.execution;

import static org.junit.Assert.assertEquals;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;

import org.apache.commons.lang3.StringUtils;
import org.apache.commons.math3.util.Pair;
import org.junit.Test;

import ca.ubc.cs.beta.aeatk.misc.jcommander.JCommanderHelper;
import ca.ubc.cs.beta.stationpacking.execution.parameters.solver.base.InstanceParameters;
import ca.ubc.cs.beta.stationpacking.facade.InterruptibleSATFCResult;
import ca.ubc.cs.beta.stationpacking.facade.SATFCFacade;
import ca.ubc.cs.beta.stationpacking.facade.SATFCFacadeBuilder;
import ca.ubc.cs.beta.stationpacking.facade.SATFCResult;
import ca.ubc.cs.beta.stationpacking.solvers.base.SATResult;
import lombok.Cleanup;
import lombok.extern.slf4j.Slf4j;

@Slf4j
public class SATFCFacadeTests {

    //A map taking a (data foldername, domains) pair of string to its expected result in the form of a (SAT result, runtime double) pair.
    public final static Map<InstanceParameters, Pair<SATResult, Double>> TEST_CASES = new HashMap<InstanceParameters, Pair<SATResult, Double>>();

    //Add in some test cases.
    static {
        //Non-trivial SAT test case.
        TEST_CASES.put(getInstance(new String[]{
                        "-DATA-FOLDERNAME",
                        "./src/test/resources/data/021814SC3M",
                        "-DOMAINS",
                        "243:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;659:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;770:2,3,4,5,6,7,8,9,10,11,12,13;510:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1867:7,8,9,10,11,12,13;647:7,8,9,10,11,12,13;372:7,8,9,10,11,12,13;1557:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;384:2,3,4,5,6;64:7,8,9,10,11,12,13;1641:7,8,9,10,11,12,13;1086:7,8,9,10,11,12,13;1835:7,8,9,10,11,12,13;684:2,3,4,5,6;626:7,8,9,10,11,12,13;137:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;569:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;522:7,8,9,10,11,12,13;1045:7,8,9,10,11,12,13;1592:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;78:2,3,4,5,6,7,8,9,10,11,12,13;2044:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;528:7,8,9,10,11,12,13;320:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;71:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1356:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;864:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1443:7,8,9,10,11,12,13;1180:7,8,9,10,11,12,13;690:2,3,4,5,6,7,8,9,10,11,12,13;1260:7,8,9,10,11,12,13;1461:7,8,9,10,11,12,13;1310:2,3,4,5,6,7,8,9,10,11,12,13;324:7,8,9,10,11,12,13;59:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;599:7,8,9,10,11,12,13;1268:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;541:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;480:7,8,9,10,11,12,13;815:7,8,9,10,11,12,13;228:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1069:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;949:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;565:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1482:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;840:7,8,9,10,11,12,13;275:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2133:7,8,9,10,11,12,13;646:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1162:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1237:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;84:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;897:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;297:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;19:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1864:7,8,9,10,11,12,13;100:7,8,9,10,11,12,13;1907:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1862:7,8,9,10,11,12,13;1620:7,8,9,10,11,12,13;955:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1373:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1890:7,8,9,10,11,12,13;1752:7,8,9,10,11,12,13;1390:2,3,4,5,6,7,8,9,10,11,12,13;1496:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1510:7,8,9,10,11,12,13;1546:2,3,4,5,6,7,8,9,10,11,12,13;1095:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1100:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;680:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1431:2,3,4,5,6,7,8,9,10,11,12,13;518:7,8,9,10,11,12,13;1657:7,8,9,10,11,12,13;1925:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1340:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1474:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2082:7,8,9,10,11,12,13;1696:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;48:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1729:2,3,4,5,6,7,8,9,10,11,12,13;651:7,8,9,10,11,12,13;263:7,8,9,10,11,12,13;1689:7,8,9,10,11,12,13;505:7,8,9,10,11,12,13;968:7,8,9,10,11,12,13;673:7,8,9,10,11,12,13;2055:7,8,9,10,11,12,13;970:7,8,9,10,11,12,13;2029:2,3,4,5,6,7,8,9,10,11,12,13;170:7,8,9,10,11,12,13;1115:7,8,9,10,11,12,13;728:7,8,9,10,11,12,13;507:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;63:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;439:2,3,4,5,6;1172:7,8,9,10,11,12,13;341:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2113:7,8,9,10,11,12,13;1111:7,8,9,10,11,12,13;449:7,8,9,10,11,12,13;986:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2165:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;379:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2072:7,8,9,10,11,12,13;490:7,8,9,10,11,12,13;1975:7,8,9,10,11,12,13;1783:7,8,9,10,11,12,13;1150:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2060:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1193:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;890:7,8,9,10,11,12,13;1266:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;775:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1247:7,8,9,10,11,12,13;392:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1072:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;784:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1377:7,8,9,10,11,12,13;2010:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1176:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;205:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;845:7,8,9,10,11,12,13;1976:2,3,4,5,6;298:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;352:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2068:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;387:7,8,9,10,11,12,13;1234:7,8,9,10,11,12,13;1587:7,8,9,10,11,12,13;966:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;154:7,8,9,10,11,12,13;459:2,3,4,5,6,7,8,9,10,11,12,13;1651:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2130:7,8,9,10,11,12,13;1566:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;828:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;118:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;994:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1132:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;271:7,8,9,10,11,12,13;918:7,8,9,10,11,12,13;441:7,8,9,10,11,12,13;1667:7,8,9,10,11,12,13;766:7,8,9,10,11,12,13;512:7,8,9,10,11,12,13;1997:2,3,4,5,6;1081:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1358:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1099:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;846:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;533:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;487:7,8,9,10,11,12,13;281:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1413:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;430:7,8,9,10,11,12,13;508:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1188:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1486:2,3,4,5,6,7,8,9,10,11,12,13;279:7,8,9,10,11,12,13;882:7,8,9,10,11,12,13;1882:7,8,9,10,11,12,13;1256:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1019:7,8,9,10,11,12,13;148:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;725:7,8,9,10,11,12,13;1974:7,8,9,10,11,12,13;470:7,8,9,10,11,12,13;867:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;469:7,8,9,10,11,12,13;285:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1929:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2046:7,8,9,10,11,12,13;52:7,8,9,10,11,12,13;915:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1866:7,8,9,10,11,12,13;1263:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2097:7,8,9,10,11,12,13;332:7,8,9,10,11,12,13;422:7,8,9,10,11,12,13;236:7,8,9,10,11,12,13;600:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;328:2,3,4,5,6;1055:7,8,9,10,11,12,13;1982:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1847:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1672:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;254:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1678:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;546:7,8,9,10,11,12,13;1311:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1840:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;374:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;560:7,8,9,10,11,12,13;665:7,8,9,10,11,12,13;2092:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;16:7,8,9,10,11,12,13;708:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1470:7,8,9,10,11,12,13;1030:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1466:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1834:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;6:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;715:7,8,9,10,11,12,13;1653:7,8,9,10,11,12,13;2116:7,8,9,10,11,12,13;107:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1297:2,3,4,5,6,7,8,9,10,11,12,13;942:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1918:2,3,4,5,6,7,8,9,10,11,12,13;1154:7,8,9,10,11,12,13;1769:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;283:7,8,9,10,11,12,13;906:7,8,9,10,11,12,13;577:7,8,9,10,11,12,13;1159:2,3,4,5,6;532:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;950:7,8,9,10,11,12,13;538:7,8,9,10,11,12,13;1582:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1414:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2056:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1198:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1995:7,8,9,10,11,12,13;181:2,3,4,5,6;1556:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;511:7,8,9,10,11,12,13;2140:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1264:7,8,9,10,11,12,13;817:7,8,9,10,11,12,13;81:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2024:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;23:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1151:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;819:2,3,4,5,6;1353:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1865:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;767:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;317:7,8,9,10,11,12,13;1190:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;927:7,8,9,10,11,12,13;1859:7,8,9,10,11,12,13;884:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;645:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;937:7,8,9,10,11,12,13;1758:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1192:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;975:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1547:7,8,9,10,11,12,13;1426:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;603:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1322:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;911:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1451:7,8,9,10,11,12,13;1327:2,3,4,5,6,7,8,9,10,11,12,13;1841:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;891:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1258:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;879:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1318:7,8,9,10,11,12,13;616:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1108:7,8,9,10,11,12,13;2128:7,8,9,10,11,12,13;489:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2170:7,8,9,10,11,12,13;952:2,3,4,5,6,7,8,9,10,11,12,13;1071:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2074:7,8,9,10,11,12,13;42:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1144:2,3,4,5,6;1497:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1585:2,3,4,5,6;1255:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;901:7,8,9,10,11,12,13;591:7,8,9,10,11,12,13;550:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;453:7,8,9,10,11,12,13;58:7,8,9,10,11,12,13;1495:7,8,9,10,11,12,13;400:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;323:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;13:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1521:7,8,9,10,11,12,13;1203:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;98:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1911:7,8,9,10,11,12,13;91:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1683:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;839:7,8,9,10,11,12,13;931:7,8,9,10,11,12,13;523:7,8,9,10,11,12,13;397:2,3,4,5,6,7,8,9,10,11,12,13;408:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;842:7,8,9,10,11,12,13;2005:7,8,9,10,11,12,13;940:7,8,9,10,11,12,13;2096:7,8,9,10,11,12,13;1350:7,8,9,10,11,12,13;2163:2,3,4,5,6,7,8,9,10,11,12,13;1362:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;735:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1594:7,8,9,10,11,12,13;200:7,8,9,10,11,12,13;978:7,8,9,10,11,12,13;1816:7,8,9,10,11,12,13;2038:7,8,9,10,11,12,13;2091:7,8,9,10,11,12,13;1308:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1998:7,8,9,10,11,12,13;1336:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1291:2,3,4,5,6;553:7,8,9,10,11,12,13;92:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;800:7,8,9,10,11,12,13;1406:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;530:7,8,9,10,11,12,13;1183:7,8,9,10,11,12,13;1035:7,8,9,10,11,12,13;1622:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1617:7,8,9,10,11,12,13;935:7,8,9,10,11,12,13;810:7,8,9,10,11,12,13;1947:7,8,9,10,11,12,13;1057:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;75:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;695:2,3,4,5,6,7,8,9,10,11,12,13;1457:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1664:7,8,9,10,11,12,13;1675:7,8,9,10,11,12,13;1775:7,8,9,10,11,12,13;109:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1477:7,8,9,10,11,12,13;1774:7,8,9,10,11,12,13;2158:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1401:7,8,9,10,11,12,13;478:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1004:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1518:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;883:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;7:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;824:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1844:2,3,4,5,6,7,8,9,10,11,12,13;111:7,8,9,10,11,12,13;1378:7,8,9,10,11,12,13;1951:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1942:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;923:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;930:7,8,9,10,11,12,13;801:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1117:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1052:2,3,4,5,6,7,8,9,10,11,12,13;1409:7,8,9,10,11,12,13;2119:7,8,9,10,11,12,13;1550:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;554:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1033:7,8,9,10,11,12,13;2064:7,8,9,10,11,12,13;1643:2,3,4,5,6;1579:7,8,9,10,11,12,13;605:2,3,4,5,6,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;925:2,3,4,5,6;1924:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1363:7,8,9,10,11,12,13;1014:7,8,9,10,11,12,13;1500:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;131:7,8,9,10,11,12,13;1094:7,8,9,10,11,12,13;685:2,3,4,5,6;501:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;77:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2011:7,8,9,10,11,12,13;496:7,8,9,10,11,12,13;1777:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1952:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1627:7,8,9,10,11,12,13;1039:7,8,9,10,11,12,13;1416:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;230:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1647:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;417:7,8,9,10,11,12,13;971:7,8,9,10,11,12,13;1562:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1088:7,8,9,10,11,12,13;1435:2,3,4,5,6;1087:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1139:7,8,9,10,11,12,13;1996:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;468:2,3,4,5,6,7,8,9,10,11,12,13;850:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1803:7,8,9,10,11,12,13;768:7,8,9,10,11,12,13;953:7,8,9,10,11,12,13;1127:7,8,9,10,11,12,13;1059:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1374:7,8,9,10,11,12,13;1166:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2070:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;140:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2030:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1288:7,8,9,10,11,12,13;1748:7,8,9,10,11,12,13;1492:7,8,9,10,11,12,13;873:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1807:7,8,9,10,11,12,13;524:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2047:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;492:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;247:7,8,9,10,11,12,13;545:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2085:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1236:2,3,4,5,6,7,8,9,10,11,12,13;190:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1638:7,8,9,10,11,12,13;957:7,8,9,10,11,12,13;1209:7,8,9,10,11,12,13;403:7,8,9,10,11,12,13;1779:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;437:7,8,9,10,11,12,13;246:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;809:7,8,9,10,11,12,13;1945:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2169:7,8,9,10,11,12,13;2017:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2090:2,3,4,5,6;1174:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;499:7,8,9,10,11,12,13;1493:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;41:7,8,9,10,11,12,13;262:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;450:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;110:7,8,9,10,11,12,13;1104:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1958:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1719:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;836:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;256:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;705:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2168:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;207:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1345:7,8,9,10,11,12,13;1233:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;18:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;936:7,8,9,10,11,12,13;1754:7,8,9,10,11,12,13;87:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1677:7,8,9,10,11,12,13;169:7,8,9,10,11,12,13;1191:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;516:7,8,9,10,11,12,13;1170:7,8,9,10,11,12,13;1330:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1823:7,8,9,10,11,12,13;1633:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;574:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1760:7,8,9,10,11,12,13;1271:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2028:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1354:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1636:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1621:7,8,9,10,11,12,13;1902:2,3,4,5,6,7,8,9,10,11,12,13;675:7,8,9,10,11,12,13;293:7,8,9,10,11,12,13;795:2,3,4,5,6;557:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1694:7,8,9,10,11,12,13;1098:7,8,9,10,11,12,13;1455:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;233:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;814:7,8,9,10,11,12,13;1686:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;756:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1450:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1830:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;976:7,8,9,10,11,12,13;926:2,3,4,5,6;241:7,8,9,10,11,12,13;1282:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;979:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;62:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;83:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1141:7,8,9,10,11,12,13;264:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2089:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1519:7,8,9,10,11,12,13;580:7,8,9,10,11,12,13;862:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1682:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;696:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1580:7,8,9,10,11,12,13;722:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;106:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;826:7,8,9,10,11,12,13;1875:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;25:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;991:7,8,9,10,11,12,13;1734:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;309:7,8,9,10,11,12,13;1910:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;993:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1597:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1376:2,3,4,5,6,7,8,9,10,11,12,13;683:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1831:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2019:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1619:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2080:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;172:7,8,9,10,11,12,13;1423:7,8,9,10,11,12,13;1877:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;881:7,8,9,10,11,12,13;353:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;956:7,8,9,10,11,12,13;2032:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;751:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1444:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;821:7,8,9,10,11,12,13;904:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1855:2,3,4,5,6;644:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1440:2,3,4,5,6,7,8,9,10,11,12,13;1407:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1464:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1228:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2156:7,8,9,10,11,12,13;390:7,8,9,10,11,12,13;1871:7,8,9,10,11,12,13;120:2,3,4,5,6,7,8,9,10,11,12,13;196:7,8,9,10,11,12,13;1761:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1523:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;791:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1250:7,8,9,10,11,12,13;471:2,3,4,5,6,7,8,9,10,11,12,13;1281:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;484:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1421:7,8,9,10,11,12,13;1079:7,8,9,10,11,12,13;248:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;370:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1375:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;399:7,8,9,10,11,12,13;1317:7,8,9,10,11,12,13;45:7,8,9,10,11,12,13;1892:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1299:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1765:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;943:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1802:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;151:7,8,9,10,11,12,13;796:2,3,4,5,6,7,8,9,10,11,12,13;1909:7,8,9,10,11,12,13;649:7,8,9,10,11,12,13;133:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2150:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2131:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;472:7,8,9,10,11,12,13;2127:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1142:7,8,9,10,11,12,13;330:7,8,9,10,11,12,13;1611:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1883:7,8,9,10,11,12,13;1392:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;431:7,8,9,10,11,12,13;1737:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1077:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2094:2,3,4,5,6;1819:2,3,4,5,6;1644:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1824:7,8,9,10,11,12,13;1483:7,8,9,10,11,12,13;284:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2053:7,8,9,10,11,12,13;339:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;395:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;96:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;694:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2118:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1697:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1371:2,3,4,5,6,7,8,9,10,11,12,13;1848:7,8,9,10,11,12,13;491:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;568:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1442:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;3:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1436:7,8,9,10,11,12,13;1815:7,8,9,10,11,12,13;209:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;638:7,8,9,10,11,12,13;674:7,8,9,10,11,12,13;820:7,8,9,10,11,12,13;1293:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2059:7,8,9,10,11,12,13;216:7,8,9,10,11,12,13;729:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;539:7,8,9,10,11,12,13;237:7,8,9,10,11,12,13;40:7,8,9,10,11,12,13;1845:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;481:2,3,4,5,6;1437:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1016:7,8,9,10,11,12,13;1490:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1776:7,8,9,10,11,12,13;1604:7,8,9,10,11,12,13;231:2,3,4,5,6,7,8,9,10,11,12,13;198:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1804:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;833:7,8,9,10,11,12,13;1290:2,3,4,5,6,7,8,9,10,11,12,13;1109:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;701:2,3,4,5,6;1278:7,8,9,10,11,12,13;234:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1164:7,8,9,10,11,12,13;723:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1481:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1333:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;601:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1427:7,8,9,10,11,12,13;878:7,8,9,10,11,12,13;2009:7,8,9,10,11,12,13;983:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1537:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2067:7,8,9,10,11,12,13;946:7,8,9,10,11,12,13;1287:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;870:7,8,9,10,11,12,13;113:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;939:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1948:7,8,9,10,11,12,13;1606:7,8,9,10,11,12,13;1125:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1113:2,3,4,5,6,7,8,9,10,11,12,13;155:7,8,9,10,11,12,13;1028:7,8,9,10,11,12,13;1155:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;33:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;718:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;802:2,3,4,5,6;635:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;592:7,8,9,10,11,12,13;1140:2,3,4,5,6,7,8,9,10,11,12,13;1826:7,8,9,10,11,12,13;404:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1565:7,8,9,10,11,12,13;423:7,8,9,10,11,12,13;899:7,8,9,10,11,12,13;1445:7,8,9,10,11,12,13;2083:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1027:7,8,9,10,11,12,13;1980:2,3,4,5,6,7,8,9,10,11,12,13;1957:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;594:7,8,9,10,11,12,13;1618:7,8,9,10,11,12,13;1720:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;419:7,8,9,10,11,12,13;1917:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1177:7,8,9,10,11,12,13;807:7,8,9,10,11,12,13;335:2,3,4,5,6,7,8,9,10,11,12,13;1858:7,8,9,10,11,12,13;811:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;653:7,8,9,10,11,12,13;1420:7,8,9,10,11,12,13;761:7,8,9,10,11,12,13;365:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1944:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2173:2,3,4,5,6;920:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;834:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1106:7,8,9,10,11,12,13;218:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;299:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;168:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2006:7,8,9,10,11,12,13;147:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1749:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2050:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;929:7,8,9,10,11,12,13;183:7,8,9,10,11,12,13;396:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1799:2,3,4,5,6,7,8,9,10,11,12,13;562:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31"
                }),
                new Pair<SATResult, Double>(SATResult.SAT, 5.0));

        //Non-trivial UNSAT test case.
        TEST_CASES.put(getInstance(new String[]{
                        "-DATA-FOLDERNAME",
                        "./src/test/resources/data/021814SC3M",
                        "-DOMAINS",
                        "243:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;659:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;770:2,3,4,5,6,7,8,9,10,11,12,13;510:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1867:7,8,9,10,11,12,13;647:7,8,9,10,11,12,13;372:7,8,9,10,11,12,13;606:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1557:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;384:2,3,4,5,6;64:7,8,9,10,11,12,13;1641:7,8,9,10,11,12,13;1086:7,8,9,10,11,12,13;1835:7,8,9,10,11,12,13;684:2,3,4,5,6;626:7,8,9,10,11,12,13;137:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;569:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;522:7,8,9,10,11,12,13;1045:7,8,9,10,11,12,13;1592:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;78:2,3,4,5,6,7,8,9,10,11,12,13;2044:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;528:7,8,9,10,11,12,13;320:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;71:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1356:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;864:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1443:7,8,9,10,11,12,13;1180:7,8,9,10,11,12,13;690:2,3,4,5,6,7,8,9,10,11,12,13;1260:7,8,9,10,11,12,13;1461:7,8,9,10,11,12,13;1310:2,3,4,5,6,7,8,9,10,11,12,13;324:7,8,9,10,11,12,13;1188:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;599:7,8,9,10,11,12,13;1268:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;541:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;480:7,8,9,10,11,12,13;815:7,8,9,10,11,12,13;1069:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;565:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1482:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;840:7,8,9,10,11,12,13;275:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2133:7,8,9,10,11,12,13;646:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1162:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;950:7,8,9,10,11,12,13;84:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;897:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;19:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1864:7,8,9,10,11,12,13;100:7,8,9,10,11,12,13;1907:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1862:7,8,9,10,11,12,13;1620:7,8,9,10,11,12,13;955:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1373:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1890:7,8,9,10,11,12,13;1752:7,8,9,10,11,12,13;1390:2,3,4,5,6,7,8,9,10,11,12,13;1510:7,8,9,10,11,12,13;1546:2,3,4,5,6,7,8,9,10,11,12,13;1095:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1100:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;680:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1431:2,3,4,5,6,7,8,9,10,11,12,13;518:7,8,9,10,11,12,13;1657:7,8,9,10,11,12,13;1925:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1340:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1474:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2082:7,8,9,10,11,12,13;1696:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;48:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1729:2,3,4,5,6,7,8,9,10,11,12,13;651:2,3,4,5,6,7,8,9,10,11,12,13;263:7,8,9,10,11,12,13;1689:7,8,9,10,11,12,13;505:7,8,9,10,11,12,13;968:7,8,9,10,11,12,13;673:2,3,4,5,6,7,8,9,10,11,12,13;2055:7,8,9,10,11,12,13;970:7,8,9,10,11,12,13;2029:2,3,4,5,6,7,8,9,10,11,12,13;170:7,8,9,10,11,12,13;1115:7,8,9,10,11,12,13;728:7,8,9,10,11,12,13;507:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;63:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;439:2,3,4,5,6;1172:7,8,9,10,11,12,13;2113:7,8,9,10,11,12,13;1111:7,8,9,10,11,12,13;449:7,8,9,10,11,12,13;986:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2165:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;379:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2072:7,8,9,10,11,12,13;490:7,8,9,10,11,12,13;1975:7,8,9,10,11,12,13;1783:7,8,9,10,11,12,13;1150:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1193:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;890:7,8,9,10,11,12,13;775:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1247:7,8,9,10,11,12,13;392:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1072:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;784:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1377:7,8,9,10,11,12,13;2010:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1176:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;205:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;845:7,8,9,10,11,12,13;1976:2,3,4,5,6;352:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2068:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;387:7,8,9,10,11,12,13;1234:7,8,9,10,11,12,13;1587:7,8,9,10,11,12,13;966:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;154:7,8,9,10,11,12,13;459:2,3,4,5,6,7,8,9,10,11,12,13;1651:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2130:7,8,9,10,11,12,13;1566:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;828:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;118:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;994:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1132:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;271:7,8,9,10,11,12,13;918:7,8,9,10,11,12,13;441:7,8,9,10,11,12,13;1667:7,8,9,10,11,12,13;766:7,8,9,10,11,12,13;512:7,8,9,10,11,12,13;1997:2,3,4,5,6;1081:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1358:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1099:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;846:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;533:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;487:7,8,9,10,11,12,13;281:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1413:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;430:7,8,9,10,11,12,13;508:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;59:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1486:2,3,4,5,6,7,8,9,10,11,12,13;279:7,8,9,10,11,12,13;882:7,8,9,10,11,12,13;1882:7,8,9,10,11,12,13;1256:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1019:7,8,9,10,11,12,13;148:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;725:7,8,9,10,11,12,13;1974:7,8,9,10,11,12,13;470:7,8,9,10,11,12,13;867:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;469:7,8,9,10,11,12,13;285:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1929:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2046:7,8,9,10,11,12,13;52:7,8,9,10,11,12,13;915:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1866:7,8,9,10,11,12,13;1263:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2097:7,8,9,10,11,12,13;332:7,8,9,10,11,12,13;422:7,8,9,10,11,12,13;236:7,8,9,10,11,12,13;600:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;328:2,3,4,5,6;1055:7,8,9,10,11,12,13;1982:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1847:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1672:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;254:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1678:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;546:7,8,9,10,11,12,13;1311:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1840:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;374:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;560:7,8,9,10,11,12,13;665:7,8,9,10,11,12,13;2092:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;16:7,8,9,10,11,12,13;708:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1470:7,8,9,10,11,12,13;1030:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1466:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1834:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;6:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;715:7,8,9,10,11,12,13;1653:7,8,9,10,11,12,13;2116:7,8,9,10,11,12,13;107:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1297:2,3,4,5,6,7,8,9,10,11,12,13;942:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1918:2,3,4,5,6,7,8,9,10,11,12,13;1154:7,8,9,10,11,12,13;1769:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;283:7,8,9,10,11,12,13;906:7,8,9,10,11,12,13;577:7,8,9,10,11,12,13;1159:2,3,4,5,6;532:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1237:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;538:7,8,9,10,11,12,13;1582:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1414:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2056:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1198:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1995:7,8,9,10,11,12,13;181:2,3,4,5,6;1556:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;511:7,8,9,10,11,12,13;2140:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1264:7,8,9,10,11,12,13;817:7,8,9,10,11,12,13;2024:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;23:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1151:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;819:2,3,4,5,6;1353:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1865:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;767:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;317:7,8,9,10,11,12,13;1190:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;927:7,8,9,10,11,12,13;1859:7,8,9,10,11,12,13;884:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;645:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;937:7,8,9,10,11,12,13;1758:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1192:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;975:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1547:7,8,9,10,11,12,13;1426:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;603:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1322:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;911:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1451:7,8,9,10,11,12,13;1327:2,3,4,5,6,7,8,9,10,11,12,13;1841:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1258:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;879:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1318:7,8,9,10,11,12,13;616:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1108:7,8,9,10,11,12,13;2128:7,8,9,10,11,12,13;489:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2170:7,8,9,10,11,12,13;952:2,3,4,5,6,7,8,9,10,11,12,13;1071:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2074:7,8,9,10,11,12,13;1144:2,3,4,5,6;1497:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1585:2,3,4,5,6;1255:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;901:7,8,9,10,11,12,13;591:7,8,9,10,11,12,13;550:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;453:7,8,9,10,11,12,13;58:7,8,9,10,11,12,13;1495:7,8,9,10,11,12,13;400:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;323:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;13:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1521:7,8,9,10,11,12,13;1203:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;98:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1911:7,8,9,10,11,12,13;91:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1683:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;839:7,8,9,10,11,12,13;931:7,8,9,10,11,12,13;523:2,3,4,5,6,7,8,9,10,11,12,13;397:2,3,4,5,6,7,8,9,10,11,12,13;408:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;842:7,8,9,10,11,12,13;2005:7,8,9,10,11,12,13;940:7,8,9,10,11,12,13;2096:7,8,9,10,11,12,13;1350:7,8,9,10,11,12,13;2163:2,3,4,5,6,7,8,9,10,11,12,13;1362:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;735:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1594:7,8,9,10,11,12,13;200:7,8,9,10,11,12,13;978:7,8,9,10,11,12,13;1816:7,8,9,10,11,12,13;2038:7,8,9,10,11,12,13;2091:7,8,9,10,11,12,13;1308:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1998:7,8,9,10,11,12,13;1336:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1291:2,3,4,5,6;553:7,8,9,10,11,12,13;92:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;800:7,8,9,10,11,12,13;1406:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;530:7,8,9,10,11,12,13;1183:7,8,9,10,11,12,13;1035:7,8,9,10,11,12,13;1622:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1617:7,8,9,10,11,12,13;935:7,8,9,10,11,12,13;810:7,8,9,10,11,12,13;1947:7,8,9,10,11,12,13;1057:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;75:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;695:2,3,4,5,6,7,8,9,10,11,12,13;1457:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1664:7,8,9,10,11,12,13;1675:7,8,9,10,11,12,13;1775:7,8,9,10,11,12,13;109:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1477:7,8,9,10,11,12,13;1774:7,8,9,10,11,12,13;2158:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1401:7,8,9,10,11,12,13;478:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1004:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1518:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;883:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;7:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1844:2,3,4,5,6,7,8,9,10,11,12,13;111:7,8,9,10,11,12,13;1378:7,8,9,10,11,12,13;1951:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1942:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;923:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;930:7,8,9,10,11,12,13;801:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1117:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1052:2,3,4,5,6,7,8,9,10,11,12,13;1409:7,8,9,10,11,12,13;2119:7,8,9,10,11,12,13;1550:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;554:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1033:7,8,9,10,11,12,13;2064:7,8,9,10,11,12,13;1643:2,3,4,5,6;1579:7,8,9,10,11,12,13;605:2,3,4,5,6,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;925:2,3,4,5,6;1924:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1363:7,8,9,10,11,12,13;1014:7,8,9,10,11,12,13;1500:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;131:7,8,9,10,11,12,13;1094:7,8,9,10,11,12,13;685:2,3,4,5,6;501:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;77:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2011:7,8,9,10,11,12,13;496:7,8,9,10,11,12,13;1952:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1627:7,8,9,10,11,12,13;1039:7,8,9,10,11,12,13;1416:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;230:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1647:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;417:7,8,9,10,11,12,13;971:7,8,9,10,11,12,13;1562:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1088:7,8,9,10,11,12,13;1435:2,3,4,5,6;1087:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1139:7,8,9,10,11,12,13;1996:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;468:2,3,4,5,6,7,8,9,10,11,12,13;850:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1803:7,8,9,10,11,12,13;768:7,8,9,10,11,12,13;953:7,8,9,10,11,12,13;1127:7,8,9,10,11,12,13;1059:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1374:7,8,9,10,11,12,13;1166:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2070:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;140:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2030:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1288:2,3,4,5,6,7,8,9,10,11,12,13;1748:7,8,9,10,11,12,13;1492:7,8,9,10,11,12,13;873:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1807:7,8,9,10,11,12,13;524:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;492:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;247:7,8,9,10,11,12,13;545:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2085:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;190:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1638:7,8,9,10,11,12,13;957:7,8,9,10,11,12,13;1209:7,8,9,10,11,12,13;403:7,8,9,10,11,12,13;1779:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;437:7,8,9,10,11,12,13;246:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;809:7,8,9,10,11,12,13;1945:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2169:7,8,9,10,11,12,13;2017:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2090:2,3,4,5,6;1174:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;499:7,8,9,10,11,12,13;1493:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;41:7,8,9,10,11,12,13;262:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;450:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;110:7,8,9,10,11,12,13;1104:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1958:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1719:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;836:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;256:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;705:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2168:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;207:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1345:7,8,9,10,11,12,13;1233:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;18:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;936:7,8,9,10,11,12,13;1754:7,8,9,10,11,12,13;1677:7,8,9,10,11,12,13;169:7,8,9,10,11,12,13;1191:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;516:7,8,9,10,11,12,13;1170:7,8,9,10,11,12,13;1330:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1823:7,8,9,10,11,12,13;1633:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;574:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1760:7,8,9,10,11,12,13;2028:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1354:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1636:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1621:7,8,9,10,11,12,13;1902:2,3,4,5,6,7,8,9,10,11,12,13;675:7,8,9,10,11,12,13;293:7,8,9,10,11,12,13;795:2,3,4,5,6;557:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1694:7,8,9,10,11,12,13;1098:7,8,9,10,11,12,13;1455:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;233:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;814:7,8,9,10,11,12,13;1686:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;756:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1450:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;976:7,8,9,10,11,12,13;926:2,3,4,5,6;241:7,8,9,10,11,12,13;1282:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;979:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;83:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1141:7,8,9,10,11,12,13;264:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2089:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1519:7,8,9,10,11,12,13;580:7,8,9,10,11,12,13;862:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1682:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;696:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1580:7,8,9,10,11,12,13;722:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;106:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;826:7,8,9,10,11,12,13;1875:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;25:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;991:7,8,9,10,11,12,13;1734:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;309:7,8,9,10,11,12,13;1910:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;993:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1597:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1376:2,3,4,5,6,7,8,9,10,11,12,13;683:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1831:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2019:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1619:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2080:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;172:7,8,9,10,11,12,13;1423:7,8,9,10,11,12,13;1877:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;881:7,8,9,10,11,12,13;353:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;956:7,8,9,10,11,12,13;2032:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;751:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1444:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;821:7,8,9,10,11,12,13;904:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1855:2,3,4,5,6;1440:2,3,4,5,6,7,8,9,10,11,12,13;1407:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1464:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1228:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2156:7,8,9,10,11,12,13;390:7,8,9,10,11,12,13;1871:7,8,9,10,11,12,13;120:2,3,4,5,6,7,8,9,10,11,12,13;196:7,8,9,10,11,12,13;1761:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1523:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;791:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1250:7,8,9,10,11,12,13;471:2,3,4,5,6,7,8,9,10,11,12,13;1281:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;484:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1421:7,8,9,10,11,12,13;1079:7,8,9,10,11,12,13;248:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;370:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1375:7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;399:7,8,9,10,11,12,13;1317:7,8,9,10,11,12,13;45:7,8,9,10,11,12,13;1892:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1299:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1765:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;943:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1802:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;151:7,8,9,10,11,12,13;796:2,3,4,5,6,7,8,9,10,11,12,13;1909:7,8,9,10,11,12,13;649:7,8,9,10,11,12,13;133:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2150:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2131:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;472:7,8,9,10,11,12,13;2127:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1142:7,8,9,10,11,12,13;330:7,8,9,10,11,12,13;1611:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1883:7,8,9,10,11,12,13;1392:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;431:7,8,9,10,11,12,13;1737:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1077:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2094:2,3,4,5,6;1819:2,3,4,5,6;1644:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1824:7,8,9,10,11,12,13;1483:7,8,9,10,11,12,13;284:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2053:7,8,9,10,11,12,13;339:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;395:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;96:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;694:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2118:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1371:2,3,4,5,6,7,8,9,10,11,12,13;1848:7,8,9,10,11,12,13;491:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;568:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1442:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;3:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1436:7,8,9,10,11,12,13;1815:7,8,9,10,11,12,13;209:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;674:7,8,9,10,11,12,13;820:7,8,9,10,11,12,13;1293:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2059:7,8,9,10,11,12,13;216:7,8,9,10,11,12,13;729:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;539:7,8,9,10,11,12,13;237:7,8,9,10,11,12,13;40:7,8,9,10,11,12,13;1845:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;481:2,3,4,5,6;1437:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1016:7,8,9,10,11,12,13;1490:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1776:7,8,9,10,11,12,13;1604:7,8,9,10,11,12,13;231:2,3,4,5,6,7,8,9,10,11,12,13;198:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1804:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;833:7,8,9,10,11,12,13;1290:2,3,4,5,6,7,8,9,10,11,12,13;1109:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;701:2,3,4,5,6;1278:7,8,9,10,11,12,13;234:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1164:7,8,9,10,11,12,13;723:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1481:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1333:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1427:7,8,9,10,11,12,13;878:7,8,9,10,11,12,13;2009:7,8,9,10,11,12,13;983:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1537:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2067:7,8,9,10,11,12,13;946:7,8,9,10,11,12,13;870:7,8,9,10,11,12,13;113:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;939:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1948:7,8,9,10,11,12,13;1606:7,8,9,10,11,12,13;1125:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1113:2,3,4,5,6,7,8,9,10,11,12,13;155:7,8,9,10,11,12,13;1028:7,8,9,10,11,12,13;1155:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;718:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;802:2,3,4,5,6;635:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;592:7,8,9,10,11,12,13;1140:2,3,4,5,6,7,8,9,10,11,12,13;1826:7,8,9,10,11,12,13;404:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1565:7,8,9,10,11,12,13;423:7,8,9,10,11,12,13;899:7,8,9,10,11,12,13;1445:7,8,9,10,11,12,13;1027:7,8,9,10,11,12,13;1980:2,3,4,5,6,7,8,9,10,11,12,13;1957:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;594:2,3,4,5,6,7,8,9,10,11,12,13;1618:7,8,9,10,11,12,13;1720:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;419:7,8,9,10,11,12,13;1177:7,8,9,10,11,12,13;807:7,8,9,10,11,12,13;335:2,3,4,5,6,7,8,9,10,11,12,13;1858:7,8,9,10,11,12,13;811:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;653:7,8,9,10,11,12,13;1420:7,8,9,10,11,12,13;761:7,8,9,10,11,12,13;365:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1944:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2173:2,3,4,5,6;920:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;834:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1106:7,8,9,10,11,12,13;218:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;299:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;168:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2006:7,8,9,10,11,12,13;147:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1749:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;2050:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;929:7,8,9,10,11,12,13;183:7,8,9,10,11,12,13;396:14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31;1799:2,3,4,5,6,7,8,9,10,11,12,13"
                }),
                new Pair<SATResult, Double>(SATResult.UNSAT, 5.0));

    }

    /**
     * Parse instance parameters from command line arguments.
     */
    private static InstanceParameters getInstance(String[] aArguments) {
        InstanceParameters instance = new InstanceParameters();
        JCommanderHelper.parseCheckingForHelpAndVersion(aArguments, instance);
        return instance;
    }

    /**
     * Create SATFC Facade Executor command line arguments from data folder name and domains arguments.
     */
    private static String[] createArguments(String aDataFoldername, Map<Integer, Set<Integer>> aDomains) {
        List<String> arguments = new ArrayList<String>();

        arguments.add("-DATA-FOLDERNAME");
        arguments.add(aDataFoldername);

        arguments.add("-DOMAINS");
        StringBuilder domainsBuilder = new StringBuilder();
        Iterator<Integer> stationsIterator = aDomains.keySet().iterator();
        while (stationsIterator.hasNext()) {
            Integer station = stationsIterator.next();
            domainsBuilder.append(station);
            domainsBuilder.append(":");
            domainsBuilder.append(StringUtils.join(aDomains.get(station), ","));
            if (stationsIterator.hasNext()) {
                domainsBuilder.append(";");
            }
        }
        arguments.add(domainsBuilder.toString());

        return arguments.toArray(new String[arguments.size()]);
    }

    /**
     * Runs the SATFC facade executor main method on all the test cases.
     */
    @Test
    public void testFacadeExecution() {
        for (InstanceParameters testCase : TEST_CASES.keySet()) {
            String dataFoldername = testCase.fDataFoldername;
            SATFCFacadeExecutor.main(createArguments(dataFoldername, testCase.getDomains()));
        }
    }

    private SATFCFacade buildFacade() {
        return new SATFCFacadeBuilder().build();
    }

    /**
     * Test the facade on all test cases.
     */
    @Test
    public void testFacade() throws Exception {
        @Cleanup
        SATFCFacade facade = buildFacade();
        int i = 0;
        log.info("Solving " + TEST_CASES.size() + " problems");
        for (Entry<InstanceParameters, Pair<SATResult, Double>> entry : TEST_CASES.entrySet()) {
            i++;
            log.info("Starting problem " + i);
            InstanceParameters testCase = entry.getKey();
            Pair<SATResult, Double> expectedResult = entry.getValue();

            SATFCResult result = facade.solve(testCase.getDomains(), testCase.getPreviousAssignment(), testCase.Cutoff, testCase.Seed, testCase.fDataFoldername);

            assertEquals(expectedResult.getFirst(), result.getResult());
            if (result.getRuntime() > expectedResult.getSecond()) {
                log.warn("[WARNING] Test case " + testCase.toString() + " took more time (" + result.getRuntime() + ") than expected (" + expectedResult.getSecond() + ").");
            }
        }
        System.out.println("DONE TEST");
    }

    @Test
    public void testInterrupt() throws Exception {
        @Cleanup
        SATFCFacade facade = buildFacade();
        int i = 0;

        for (Entry<InstanceParameters, Pair<SATResult, Double>> entry : TEST_CASES.entrySet()) {
        	i++;
            log.info("Starting problem " + i);
            InstanceParameters testCase = entry.getKey();
            final InterruptibleSATFCResult interruptibleSATFCResult = facade.solveInterruptibly(testCase.getDomains(), testCase.getPreviousAssignment(), testCase.Cutoff, testCase.Seed, testCase.fDataFoldername);
            new Thread() {

                @Override
                public void run() {
                    try {
                        Thread.sleep(100);
                    } catch (InterruptedException e) {
                        throw new RuntimeException(e);
                    }
                    log.info("interrupting problem");
                    interruptibleSATFCResult.interrupt();
                }

            }.start();
            final SATFCResult result = interruptibleSATFCResult.computeResult();
            assertEquals(SATResult.TIMEOUT, result.getResult());
        }
    }

}
