Skip to content

Instantly share code, notes, and snippets.

@dmitrygusev
Created January 22, 2011 11:36
Show Gist options
  • Save dmitrygusev/791064 to your computer and use it in GitHub Desktop.
Save dmitrygusev/791064 to your computer and use it in GitHub Desktop.
package com.anjlab.sat3;
import java.util.Properties;
import org.junit.BeforeClass;
import org.junit.Test;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
import cern.colt.list.ObjectArrayList;
public class TestExamples
{
private static final Logger LOGGER = LoggerFactory.getLogger(TestExamples.class);
@BeforeClass
public static void setup()
{
Helper.UsePrettyPrint = true;
Helper.EnableAssertions = true;
System.out.println(TestExamples.class.getName());
}
@Test
public void testHabr() throws Exception
{
ObjectArrayList ct = new ObjectArrayList(
new ITabularFormula[] {
Helper.createFormula(1, 2, -6,
1, -2, 6,
-1, 2, 6,
-1, -2, -6),
Helper.createFormula(3, 4, -7,
3, -4, 7,
-3, 4, 7,
-3, -4, -7),
Helper.createFormula(5, 6, -7,
5, -6, 7,
-5, 6, 7,
-5, -6, -7),
Helper.createFormula(1, 2, -8,
1, -2, 8,
-1, 2, 8,
-1, -2, -8),
Helper.createFormula(3, 4, -9,
3, -4, 9,
-3, 4, 9,
-3, -4, -9),
Helper.createFormula(5, 8, 9,
5, -8, -9,
-5, 8, -9,
-5, -8, 9),
Helper.createFormula(10, 11, 12),
}
);
LOGGER.info("Initial CTF set");
Helper.printFormulas(ct);
IPermutation permutation = new SimplePermutation();
for (int varName = 1; varName <= 12; varName++)
{
permutation.add(varName);
}
LOGGER.info("CTF -> CTS");
Helper.completeToCTS(ct, permutation);
LOGGER.info("CTS set");
Helper.printFormulas(ct);
LOGGER.info("Unify all CTS");
Helper.unify(ct);
try
{
Properties statistics = new Properties();
Helper.createHyperStructuresSystem(ct, (ICompactTripletsStructure) ct.get(ct.size() - 1), statistics);
}
catch (EmptyStructureException e)
{
LOGGER.info("Formula not satisfiable", e);
}
}
}
com.anjlab.sat3.TestExamples
17:12:28,756|0 INFO [TestExamples] - Initial CTF set
17:12:28,757|1 INFO [Helper] - --------------------------------------------------
17:12:28,764|8 INFO [Helper] -
x1 x2 x6
0 0 1
0 1 0
1 0 0
1 1 1
VarCount: 3; ClausesCount: 4; TiersCount: 1
17:12:28,765|9 INFO [Helper] - --------------------------------------------------
17:12:28,765|9 INFO [Helper] -
x3 x4 x7
0 0 1
0 1 0
1 0 0
1 1 1
VarCount: 3; ClausesCount: 4; TiersCount: 1
17:12:28,765|9 INFO [Helper] - --------------------------------------------------
17:12:28,766|10 INFO [Helper] -
x5 x6 x7
0 0 1
0 1 0
1 0 0
1 1 1
VarCount: 3; ClausesCount: 4; TiersCount: 1
17:12:28,766|10 INFO [Helper] - --------------------------------------------------
17:12:28,766|10 INFO [Helper] -
x1 x2 x8
0 0 1
0 1 0
1 0 0
1 1 1
VarCount: 3; ClausesCount: 4; TiersCount: 1
17:12:28,766|10 INFO [Helper] - --------------------------------------------------
17:12:28,766|10 INFO [Helper] -
x3 x4 x9
0 0 1
0 1 0
1 0 0
1 1 1
VarCount: 3; ClausesCount: 4; TiersCount: 1
17:12:28,766|10 INFO [Helper] - --------------------------------------------------
17:12:28,766|10 INFO [Helper] -
x5 x8 x9
0 0 0
0 1 1
1 0 1
1 1 0
VarCount: 3; ClausesCount: 4; TiersCount: 1
17:12:28,766|10 INFO [Helper] - --------------------------------------------------
17:12:28,767|11 INFO [Helper] -
x10 x11 x12
0 0 0
VarCount: 3; ClausesCount: 1; TiersCount: 1
17:12:28,768|12 INFO [TestExamples] - CTF -> CTS
17:12:28,770|14 INFO [Helper] - Completing CTF-0 of 6 to CTS
17:12:28,774|18 INFO [Helper] - Completing CTF-1 of 6 to CTS
17:12:28,774|18 INFO [Helper] - Completing CTF-2 of 6 to CTS
17:12:28,775|19 INFO [Helper] - Completing CTF-3 of 6 to CTS
17:12:28,775|19 INFO [Helper] - Completing CTF-4 of 6 to CTS
17:12:28,775|19 INFO [Helper] - Completing CTF-5 of 6 to CTS
17:12:28,775|19 INFO [Helper] - Completing CTF-6 of 6 to CTS
17:12:28,776|20 INFO [TestExamples] - CTS set
17:12:28,776|20 INFO [Helper] - --------------------------------------------------
17:12:28,778|22 INFO [Helper] -
x1 x2 x6 x3 x4 x5 x7 x8 x9 x10 x11 x12
0 0 0
0 1 1
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 76; TiersCount: 10
17:12:28,778|22 INFO [Helper] - --------------------------------------------------
17:12:28,780|24 INFO [Helper] -
x3 x4 x7 x1 x2 x5 x6 x8 x9 x10 x11 x12
0 0 0
0 1 1
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 76; TiersCount: 10
17:12:28,780|24 INFO [Helper] - --------------------------------------------------
17:12:28,782|26 INFO [Helper] -
x5 x6 x7 x1 x2 x3 x4 x8 x9 x10 x11 x12
0 0 0
0 1 1
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 76; TiersCount: 10
17:12:28,783|27 INFO [Helper] - --------------------------------------------------
17:12:28,785|29 INFO [Helper] -
x1 x2 x8 x3 x4 x5 x6 x7 x9 x10 x11 x12
0 0 0
0 1 1
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 76; TiersCount: 10
17:12:28,785|29 INFO [Helper] - --------------------------------------------------
17:12:28,786|30 INFO [Helper] -
x3 x4 x9 x1 x2 x5 x6 x7 x8 x10 x11 x12
0 0 0
0 1 1
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 76; TiersCount: 10
17:12:28,786|30 INFO [Helper] - --------------------------------------------------
17:12:28,787|31 INFO [Helper] -
x5 x8 x9 x1 x2 x3 x4 x6 x7 x10 x11 x12
0 0 1
0 1 0
1 0 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 76; TiersCount: 10
17:12:28,787|31 INFO [Helper] - --------------------------------------------------
17:12:28,788|32 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 79; TiersCount: 10
17:12:28,788|32 INFO [TestExamples] - Unify all CTS
17:12:28,791|35 DEBUG [VarPairsIndexFactory] - Building pairs index...
17:12:28,796|40 DEBUG [VarPairsIndexFactory] - Removed 10 triplet permutations from index
17:12:28,796|40 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,796|40 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,803|47 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,804|48 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,806|50 DEBUG [Helper] - Building HSS tier #1 of 10
17:12:28,817|61 DEBUG [Helper] - Tier #1 of HSS contained 7 vertices before unification: 001, 010, 011, 100, 101, 110, 111
17:12:28,817|61 DEBUG [VarPairsIndexFactory] - Building pairs index...
17:12:28,818|62 DEBUG [VarPairsIndexFactory] - Removed 7 triplet permutations from index
17:12:28,818|62 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,818|62 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,820|64 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,820|64 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,820|64 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,820|64 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,821|65 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,821|65 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,821|65 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,822|66 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,822|66 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,823|67 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,823|67 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,823|67 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,823|67 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,823|67 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,824|68 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,824|68 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,824|68 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,824|68 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,825|69 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,825|69 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,825|69 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,825|69 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,825|69 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,825|69 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,826|70 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,826|70 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,826|70 DEBUG [Helper] - Tier #1 of HSS contained 7 vertices after unification: 001, 010, 011, 100, 101, 110, 111
17:12:28,827|71 DEBUG [Helper] - Building HSS tier #2 of 10
17:12:28,827|71 DEBUG [Helper] - HSS tier #1 is: 001, 010, 011, 100, 101, 110, 111
17:12:28,827|71 DEBUG [Helper] - Basic tier #1 is: 001, 010, 011, 100, 101, 110, 111
17:12:28,828|72 DEBUG [Helper] - Basic tier #2 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:28,829|73 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #1 of 10 total
17:12:28,830|74 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,830|74 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,833|77 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,833|77 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,833|77 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #1 of 10 total
17:12:28,834|78 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,834|78 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,834|78 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,834|78 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,834|78 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 100 tier #1 of 10 total
17:12:28,834|78 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,835|79 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,835|79 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,835|79 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,835|79 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 100 tier #1 of 10 total
17:12:28,835|79 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,836|80 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,837|81 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,837|81 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,837|81 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #1 of 10 total
17:12:28,840|84 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,851|95 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,852|96 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,852|96 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,852|96 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #1 of 10 total
17:12:28,852|96 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,852|96 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,852|96 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,852|96 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,853|97 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #1 of 10 total
17:12:28,853|97 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,853|97 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,853|97 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,853|97 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,853|97 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #1 of 10 total
17:12:28,853|97 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,853|97 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,854|98 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,854|98 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,854|98 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 011 tier #1 of 10 total
17:12:28,854|98 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,854|98 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,854|98 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,854|98 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,854|98 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 011 tier #1 of 10 total
17:12:28,855|99 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,855|99 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,855|99 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,855|99 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,855|99 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #1 of 10 total
17:12:28,856|100 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,856|100 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,856|100 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,856|100 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,856|100 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #1 of 10 total
17:12:28,857|101 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,857|101 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,857|101 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,857|101 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,858|102 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 001 tier #1 of 10 total
17:12:28,858|102 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,858|102 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,858|102 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,858|102 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,858|102 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 001 tier #1 of 10 total
17:12:28,858|102 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,858|102 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,858|102 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,859|103 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,859|103 DEBUG [Helper] - 0 leaf-vertices (vertices that were not shifted) were removed from tier #1
17:12:28,859|103 DEBUG [Helper] - Tier #2 of HSS contained 8 vertices before unification: 000, 001, 010, 011, 100, 101, 110, 111
17:12:28,859|103 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,859|103 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,859|103 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,859|103 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,859|103 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,859|103 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,860|104 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,860|104 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,860|104 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,860|104 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,860|104 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,860|104 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,861|105 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,861|105 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,861|105 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,861|105 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,861|105 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,861|105 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,861|105 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,861|105 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,861|105 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,861|105 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,862|106 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,862|106 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,862|106 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,862|106 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,862|106 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,862|106 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,862|106 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,862|106 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,862|106 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,862|106 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,862|106 DEBUG [Helper] - Tier #2 of HSS contained 8 vertices after unification: 000, 001, 010, 011, 100, 101, 110, 111
17:12:28,863|107 DEBUG [Helper] - Building HSS tier #3 of 10
17:12:28,863|107 DEBUG [Helper] - HSS tier #2 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:28,864|108 DEBUG [Helper] - Basic tier #2 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:28,864|108 DEBUG [Helper] - Basic tier #3 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:28,864|108 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 000 tier #2 of 10 total
17:12:28,864|108 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,864|108 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,865|109 DEBUG [Helper] - 39 clauses removed during this recursion level
17:12:28,868|112 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,868|112 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,869|113 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,869|113 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,872|116 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,872|116 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,873|117 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,873|117 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,873|117 INFO [Helper] - Unify unions after parallel filtration: vertexIndex = 0 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:28,873|117 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,873|117 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,874|118 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,874|118 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,875|119 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 000 tier #2 of 10 total
17:12:28,875|119 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,875|119 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,876|120 DEBUG [Helper] - 39 clauses removed during this recursion level
17:12:28,876|120 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,876|120 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,876|120 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,876|120 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,877|121 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,877|121 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,877|121 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,877|121 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,877|121 INFO [Helper] - Unify unions after parallel filtration: vertexIndex = 0 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:28,877|121 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,895|139 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,895|139 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,895|139 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,895|139 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #2 of 10 total
17:12:28,895|139 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,895|139 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,897|141 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:28,897|141 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,897|141 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,897|141 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,897|141 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,898|142 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,898|142 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,898|142 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,898|142 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,898|142 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,898|142 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,899|143 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,899|143 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,899|143 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 1 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:28,899|143 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,901|145 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,901|145 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,901|145 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,901|145 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #2 of 10 total
17:12:28,901|145 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,901|145 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,902|146 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:28,902|146 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,902|146 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,902|146 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,902|146 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,905|149 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,905|149 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,905|149 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,905|149 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,905|149 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,905|149 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,905|149 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,905|149 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,906|150 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 1 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:28,906|150 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,906|150 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,906|150 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,906|150 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,906|150 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 100 tier #2 of 10 total
17:12:28,906|150 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,906|150 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,907|151 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:28,907|151 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,907|151 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,907|151 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,907|151 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,908|152 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,908|152 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,908|152 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,908|152 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,908|152 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,908|152 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,909|153 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,909|153 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,909|153 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 2 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:28,909|153 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,909|153 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,909|153 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,909|153 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,909|153 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 100 tier #2 of 10 total
17:12:28,910|154 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,910|154 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,912|156 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:28,912|156 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,912|156 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,912|156 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,912|156 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,913|157 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,913|157 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,913|157 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,913|157 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,914|158 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,915|159 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,915|159 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,915|159 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,915|159 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 2 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:28,915|159 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,916|160 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,916|160 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,916|160 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,916|160 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 011 tier #2 of 10 total
17:12:28,916|160 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,916|160 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,917|161 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:28,917|161 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,917|161 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,917|161 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,918|162 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,919|163 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,919|163 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,919|163 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,919|163 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,919|163 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,919|163 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,920|164 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,920|164 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,920|164 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 3 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:28,920|164 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,920|164 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,921|165 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,921|165 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,921|165 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 011 tier #2 of 10 total
17:12:28,921|165 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,921|165 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,922|166 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:28,922|166 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,922|166 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,923|167 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,923|167 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,923|167 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,923|167 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,924|168 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,924|168 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,924|168 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,924|168 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,925|169 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,925|169 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,926|170 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 3 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:28,926|170 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,926|170 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,926|170 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,926|170 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,927|171 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #2 of 10 total
17:12:28,927|171 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,927|171 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,927|171 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:28,927|171 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,928|172 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,928|172 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,928|172 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,929|173 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,929|173 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,934|178 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,934|178 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,934|178 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,934|178 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,935|179 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,935|179 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,935|179 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 4 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:28,935|179 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,935|179 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,936|180 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,936|180 DEBUG [Helper] - Unification completed on recursion level 1
17:12:28,936|180 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #2 of 10 total
17:12:28,936|180 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,937|181 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,986|230 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:28,994|238 DEBUG [Helper] - Running unify routine (2 level)...
17:12:28,994|238 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:28,995|239 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:28,995|239 DEBUG [Helper] - Unification completed on recursion level 2
17:12:28,995|239 DEBUG [Helper] - Running unify routine (1 level)...
17:12:28,995|239 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:28,995|239 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,007|251 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,007|251 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,008|252 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,008|252 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,008|252 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,009|253 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 4 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:29,009|253 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,009|253 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,009|253 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,009|253 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,009|253 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #2 of 10 total
17:12:29,009|253 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,009|253 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,010|254 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:29,010|254 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,010|254 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:29,010|254 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,010|254 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,011|255 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,011|255 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,011|255 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,011|255 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,030|274 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,030|274 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,030|274 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,030|274 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,030|274 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 5 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:29,030|274 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,030|274 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,031|275 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,031|275 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,031|275 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #2 of 10 total
17:12:29,031|275 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,031|275 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,032|276 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:29,032|276 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,032|276 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:29,032|276 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,032|276 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,033|277 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,033|277 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,033|277 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,033|277 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,033|277 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,033|277 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,033|277 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,034|278 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,034|278 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 5 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:29,034|278 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,034|278 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,034|278 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,034|278 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,034|278 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #2 of 10 total
17:12:29,035|279 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,035|279 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,035|279 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:29,035|279 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,035|279 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:29,036|280 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,036|280 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,036|280 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,036|280 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,036|280 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,036|280 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,036|280 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,037|281 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,037|281 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,037|281 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,037|281 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 6 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:29,037|281 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,037|281 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,037|281 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,037|281 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,038|282 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #2 of 10 total
17:12:29,038|282 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,038|282 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,038|282 DEBUG [Helper] - 50 clauses removed during this recursion level
17:12:29,038|282 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,038|282 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:29,039|283 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,039|283 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,039|283 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,039|283 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,040|284 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,040|284 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,040|284 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,040|284 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,040|284 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,040|284 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,040|284 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 6 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:29,040|284 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,040|284 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,041|285 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,041|285 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,042|286 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 001 tier #2 of 10 total
17:12:29,042|286 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,042|286 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,043|287 DEBUG [Helper] - 39 clauses removed during this recursion level
17:12:29,043|287 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,043|287 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:29,043|287 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,043|287 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,043|287 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,044|288 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,044|288 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,044|288 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,044|288 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 7 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:29,044|288 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,044|288 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,044|288 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,045|289 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,045|289 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 001 tier #2 of 10 total
17:12:29,045|289 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,045|289 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,045|289 DEBUG [Helper] - 39 clauses removed during this recursion level
17:12:29,045|289 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,045|289 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 10
17:12:29,046|290 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,046|290 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,046|290 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,046|290 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,047|291 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,047|291 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,047|291 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 7 of 7, sTierIndex = 0 of 0, nextTierIndex = 2 of 9
17:12:29,047|291 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,047|291 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,047|291 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,048|292 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,048|292 DEBUG [Helper] - 0 leaf-vertices (vertices that were not shifted) were removed from tier #2
17:12:29,048|292 DEBUG [Helper] - Tier #3 of HSS contained 8 vertices before unification: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,048|292 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,048|292 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,048|292 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,048|292 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,049|293 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,049|293 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,049|293 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,049|293 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,049|293 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,049|293 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,050|294 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,050|294 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,050|294 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,050|294 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,050|294 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,050|294 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,050|294 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,051|295 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,051|295 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,051|295 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,051|295 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,051|295 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,051|295 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,051|295 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,052|296 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,052|296 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,052|296 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,052|296 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,052|296 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,052|296 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,053|297 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,053|297 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,053|297 DEBUG [Helper] - Tier #3 of HSS contained 8 vertices after unification: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,053|297 DEBUG [Helper] - Building HSS tier #4 of 10
17:12:29,053|297 DEBUG [Helper] - HSS tier #3 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,053|297 DEBUG [Helper] - Basic tier #3 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,053|297 DEBUG [Helper] - Basic tier #4 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,053|297 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 000 tier #3 of 10 total
17:12:29,053|297 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,053|297 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,054|298 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,054|298 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,054|298 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,054|298 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,054|298 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,055|299 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,055|299 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,055|299 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,055|299 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,055|299 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,056|300 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,056|300 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,056|300 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,056|300 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,056|300 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,056|300 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,057|301 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,057|301 INFO [Helper] - Unify unions after parallel filtration: vertexIndex = 0 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,057|301 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,057|301 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,058|302 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,058|302 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,058|302 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,058|302 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,059|303 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,059|303 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,059|303 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,059|303 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,059|303 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,059|303 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,059|303 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 0 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,059|303 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,059|303 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,060|304 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,060|304 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,060|304 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 000 tier #3 of 10 total
17:12:29,060|304 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,060|304 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,060|304 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,061|305 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,061|305 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,061|305 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,061|305 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,061|305 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,061|305 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,062|306 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,062|306 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,062|306 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,062|306 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,062|306 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,062|306 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,062|306 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,062|306 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,063|307 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,063|307 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,063|307 INFO [Helper] - Unify unions after parallel filtration: vertexIndex = 0 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,063|307 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,063|307 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,063|307 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,063|307 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,064|308 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,064|308 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,064|308 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,064|308 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,064|308 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,064|308 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,064|308 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,065|309 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,065|309 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 0 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,065|309 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,065|309 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,065|309 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,065|309 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,065|309 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #3 of 10 total
17:12:29,065|309 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,065|309 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,066|310 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,066|310 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,066|310 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,066|310 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,066|310 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,067|311 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,067|311 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,067|311 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,067|311 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,067|311 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,067|311 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,067|311 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,067|311 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,068|312 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,068|312 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,068|312 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,068|312 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,068|312 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,068|312 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,068|312 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,068|312 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,069|313 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 1 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,069|313 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,069|313 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,069|313 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,069|313 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,069|313 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,070|314 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,070|314 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,070|314 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,070|314 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,070|314 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,070|314 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,070|314 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,071|315 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 1 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,071|315 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,071|315 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,071|315 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,071|315 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,071|315 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #3 of 10 total
17:12:29,071|315 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,071|315 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,072|316 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,072|316 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,072|316 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,072|316 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,072|316 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,073|317 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,073|317 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,074|318 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,074|318 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,074|318 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,074|318 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,074|318 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,074|318 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,074|318 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,075|319 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,075|319 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,075|319 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,075|319 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,075|319 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,075|319 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,075|319 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,076|320 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 1 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,076|320 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,076|320 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,076|320 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,076|320 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,076|320 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,077|321 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,077|321 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,077|321 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,077|321 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,077|321 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,077|321 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,077|321 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,077|321 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 1 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,078|322 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,078|322 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,078|322 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,078|322 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,078|322 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 100 tier #3 of 10 total
17:12:29,078|322 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,078|322 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,079|323 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,079|323 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,079|323 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,079|323 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,079|323 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,079|323 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,079|323 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,080|324 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,080|324 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,080|324 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,080|324 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,080|324 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,080|324 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,080|324 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,080|324 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,081|325 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,081|325 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,081|325 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,081|325 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,081|325 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,081|325 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,081|325 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 2 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,081|325 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,081|325 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,082|326 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,082|326 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,082|326 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,082|326 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,082|326 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,082|326 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,083|327 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,083|327 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,083|327 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,083|327 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,083|327 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 2 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,083|327 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,083|327 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,083|327 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,084|328 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,084|328 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 100 tier #3 of 10 total
17:12:29,084|328 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,084|328 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,085|329 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,085|329 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,085|329 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,085|329 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,085|329 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,085|329 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,086|330 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,086|330 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,086|330 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,086|330 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,086|330 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,086|330 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,086|330 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,086|330 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,086|330 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,087|331 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,087|331 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,087|331 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,087|331 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,087|331 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,087|331 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,087|331 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 2 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,087|331 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,088|332 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,088|332 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,088|332 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,088|332 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,088|332 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,089|333 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,089|333 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,089|333 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,089|333 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,089|333 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,089|333 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,089|333 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 2 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,089|333 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,089|333 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,090|334 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,090|334 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,091|335 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 011 tier #3 of 10 total
17:12:29,091|335 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,091|335 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,091|335 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,091|335 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,091|335 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,091|335 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,092|336 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,092|336 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,092|336 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,092|336 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,092|336 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,092|336 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,092|336 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,093|337 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,093|337 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,093|337 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,093|337 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,093|337 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,093|337 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,093|337 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 3 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,094|338 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,094|338 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,094|338 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,094|338 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,094|338 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,094|338 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,095|339 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,095|339 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,095|339 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,095|339 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,095|339 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,095|339 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,095|339 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 3 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,095|339 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,095|339 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,096|340 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,096|340 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,096|340 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 011 tier #3 of 10 total
17:12:29,096|340 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,096|340 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,096|340 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,096|340 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,097|341 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,097|341 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,097|341 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,097|341 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,097|341 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,097|341 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,097|341 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,098|342 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,098|342 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,098|342 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,098|342 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,098|342 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,098|342 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,098|342 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,098|342 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,099|343 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 3 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,099|343 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,099|343 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,100|344 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,100|344 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,101|345 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,101|345 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,101|345 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,101|345 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,101|345 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,101|345 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,102|346 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,102|346 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,102|346 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 3 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,102|346 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,102|346 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,102|346 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,102|346 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,102|346 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #3 of 10 total
17:12:29,103|347 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,103|347 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,103|347 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,103|347 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,103|347 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,103|347 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,103|347 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,104|348 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,104|348 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,104|348 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,104|348 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,104|348 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,104|348 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,105|349 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,105|349 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,105|349 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,105|349 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,105|349 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,105|349 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,106|350 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 4 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,107|351 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,107|351 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,107|351 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,107|351 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,107|351 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,107|351 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,108|352 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,108|352 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,108|352 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,108|352 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,108|352 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,108|352 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,109|353 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 4 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,109|353 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,109|353 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,109|353 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,109|353 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,109|353 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #3 of 10 total
17:12:29,109|353 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,109|353 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,110|354 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,110|354 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,110|354 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,110|354 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,111|355 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,111|355 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,111|355 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,111|355 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,111|355 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,112|356 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,112|356 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,112|356 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,112|356 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,112|356 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,112|356 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,113|357 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,113|357 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,113|357 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 4 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,113|357 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,113|357 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,114|358 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,114|358 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,114|358 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,115|359 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,115|359 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,115|359 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,115|359 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,115|359 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,115|359 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,117|361 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,117|361 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 4 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,117|361 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,117|361 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,118|362 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,118|362 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,118|362 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #3 of 10 total
17:12:29,118|362 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,118|362 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,119|363 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,119|363 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,119|363 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,119|363 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,119|363 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,120|364 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,120|364 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,120|364 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,120|364 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,120|364 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,120|364 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,121|365 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,121|365 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,121|365 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,121|365 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,121|365 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,131|375 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,131|375 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,131|375 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,131|375 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,131|375 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,131|375 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 5 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,132|376 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,132|376 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,132|376 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,132|376 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,132|376 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,132|376 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,133|377 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,133|377 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,133|377 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,133|377 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,133|377 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,133|377 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,134|378 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 5 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,134|378 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,134|378 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,134|378 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,134|378 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,134|378 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #3 of 10 total
17:12:29,134|378 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,135|379 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,135|379 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,135|379 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,135|379 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,135|379 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,135|379 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,136|380 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,136|380 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,136|380 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,136|380 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,136|380 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,136|380 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,137|381 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,137|381 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,137|381 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,137|381 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,137|381 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,137|381 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,137|381 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,137|381 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,138|382 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,138|382 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,138|382 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 5 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,138|382 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,138|382 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,138|382 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,138|382 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,139|383 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,139|383 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,139|383 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,139|383 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,139|383 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,139|383 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,140|384 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,140|384 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,140|384 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 5 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,140|384 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,140|384 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,140|384 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,140|384 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,141|385 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #3 of 10 total
17:12:29,141|385 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,141|385 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,141|385 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,141|385 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,141|385 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,142|386 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,142|386 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,142|386 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,142|386 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,142|386 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,142|386 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,143|387 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,143|387 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,143|387 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,143|387 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,143|387 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,143|387 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,144|388 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,144|388 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,144|388 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,144|388 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,144|388 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,144|388 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,144|388 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 6 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,144|388 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,144|388 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,145|389 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,145|389 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,145|389 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,145|389 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,146|390 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,146|390 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,146|390 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,146|390 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,146|390 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,146|390 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,146|390 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 6 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,146|390 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,147|391 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,147|391 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,147|391 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,147|391 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #3 of 10 total
17:12:29,147|391 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,147|391 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,148|392 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,148|392 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,148|392 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,148|392 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,148|392 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,149|393 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,149|393 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,149|393 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,149|393 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,149|393 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,149|393 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,150|394 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,150|394 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,150|394 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,150|394 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,150|394 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,150|394 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,150|394 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,150|394 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,151|395 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,151|395 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,151|395 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 6 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,151|395 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,151|395 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,151|395 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,152|396 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,152|396 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,152|396 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,152|396 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,152|396 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,152|396 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,153|397 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,153|397 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,153|397 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,154|398 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 6 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,154|398 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,154|398 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,154|398 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,154|398 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,154|398 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 001 tier #3 of 10 total
17:12:29,154|398 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,155|399 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,155|399 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,155|399 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,155|399 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,155|399 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,155|399 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,156|400 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,156|400 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,156|400 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,156|400 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,156|400 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,156|400 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,157|401 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,157|401 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,157|401 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,157|401 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,157|401 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,157|401 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,157|401 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 7 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,157|401 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,158|402 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,158|402 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,158|402 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,158|402 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,158|402 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,159|403 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,159|403 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,159|403 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,159|403 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,159|403 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,159|403 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,159|403 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 7 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,159|403 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,160|404 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,160|404 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,160|404 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,160|404 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 001 tier #3 of 10 total
17:12:29,160|404 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,160|404 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,161|405 DEBUG [Helper] - 4 clauses removed during this recursion level
17:12:29,161|405 DEBUG [Helper] - Running unify routine (2 level)...
17:12:29,161|405 DEBUG [Helper] - # of pairs in index: 28; # of varNames in index: 5
17:12:29,161|405 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,161|405 DEBUG [Helper] - Unification completed on recursion level 2
17:12:29,161|405 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,162|406 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,162|406 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,162|406 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,162|406 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,162|406 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,162|406 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,162|406 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,162|406 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,162|406 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,163|407 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,163|407 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,163|407 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 7 of 7, sTierIndex = 0 of 1, nextTierIndex = 3 of 9
17:12:29,163|407 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,163|407 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,163|407 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,163|407 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,164|408 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,164|408 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,164|408 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,164|408 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,164|408 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,164|408 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,165|409 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,165|409 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,165|409 DEBUG [Helper] - Unify unions after parallel filtration: vertexIndex = 7 of 7, sTierIndex = 1 of 1, nextTierIndex = 3 of 9
17:12:29,165|409 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,165|409 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,165|409 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,165|409 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,165|409 DEBUG [Helper] - 0 leaf-vertices (vertices that were not shifted) were removed from tier #3
17:12:29,165|409 DEBUG [Helper] - Tier #4 of HSS contained 8 vertices before unification: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,166|410 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,166|410 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,167|411 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,167|411 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,167|411 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,167|411 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,167|411 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,167|411 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,167|411 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,167|411 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,168|412 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,168|412 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,168|412 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,168|412 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,168|412 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,168|412 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,168|412 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,168|412 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,169|413 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,169|413 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,169|413 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,169|413 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,169|413 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,169|413 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,169|413 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,169|413 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,169|413 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,170|414 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,170|414 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,170|414 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,170|414 DEBUG [Helper] - 0 clauses removed during this recursion level
17:12:29,170|414 DEBUG [Helper] - Unification completed on recursion level 1
17:12:29,170|414 DEBUG [Helper] - Tier #4 of HSS contained 8 vertices after unification: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,170|414 DEBUG [Helper] - Building HSS tier #5 of 10
17:12:29,170|414 DEBUG [Helper] - HSS tier #4 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,171|415 DEBUG [Helper] - Basic tier #4 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,171|415 DEBUG [Helper] - Basic tier #5 is: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,171|415 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 000 tier #4 of 10 total
17:12:29,171|415 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,171|415 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,171|415 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 000 tier #4 of 10 total
17:12:29,171|415 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,171|415 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,172|416 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #4 of 10 total
17:12:29,172|416 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,172|416 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,172|416 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #4 of 10 total
17:12:29,172|416 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,172|416 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,173|417 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 100 tier #4 of 10 total
17:12:29,173|417 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,173|417 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,173|417 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 100 tier #4 of 10 total
17:12:29,173|417 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,173|417 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,173|417 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 011 tier #4 of 10 total
17:12:29,173|417 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,174|418 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,174|418 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 011 tier #4 of 10 total
17:12:29,174|418 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,174|418 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,174|418 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #4 of 10 total
17:12:29,174|418 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,174|418 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,175|419 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #4 of 10 total
17:12:29,175|419 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,175|419 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,175|419 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #4 of 10 total
17:12:29,175|419 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,175|419 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,176|420 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #4 of 10 total
17:12:29,176|420 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,176|420 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,176|420 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #4 of 10 total
17:12:29,176|420 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,176|420 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,176|420 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #4 of 10 total
17:12:29,176|420 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,176|420 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,177|421 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 001 tier #4 of 10 total
17:12:29,177|421 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,177|421 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,178|422 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 001 tier #4 of 10 total
17:12:29,178|422 DEBUG [Helper] - Running unify routine (1 level)...
17:12:29,178|422 DEBUG [Helper] - # of pairs in index: 39; # of varNames in index: 12
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 000 on tier #4 of HSS(0)
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 111 on tier #4 of HSS(0)
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 100 on tier #4 of HSS(0)
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 011 on tier #4 of HSS(0)
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 010 on tier #4 of HSS(0)
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 110 on tier #4 of HSS(0)
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 101 on tier #4 of HSS(0)
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 001 on tier #4 of HSS(0)
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 000 on tier #4 of HSS(1)
17:12:29,178|422 DEBUG [Helper] - Clearing leaf-vertex 111 on tier #4 of HSS(1)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 100 on tier #4 of HSS(1)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 011 on tier #4 of HSS(1)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 010 on tier #4 of HSS(1)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 110 on tier #4 of HSS(1)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 101 on tier #4 of HSS(1)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 001 on tier #4 of HSS(1)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 000 on tier #4 of HSS(2)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 111 on tier #4 of HSS(2)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 100 on tier #4 of HSS(2)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 011 on tier #4 of HSS(2)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 010 on tier #4 of HSS(2)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 110 on tier #4 of HSS(2)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 101 on tier #4 of HSS(2)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 001 on tier #4 of HSS(2)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 000 on tier #4 of HSS(3)
17:12:29,179|423 DEBUG [Helper] - Clearing leaf-vertex 111 on tier #4 of HSS(3)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 100 on tier #4 of HSS(3)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 011 on tier #4 of HSS(3)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 010 on tier #4 of HSS(3)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 110 on tier #4 of HSS(3)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 101 on tier #4 of HSS(3)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 001 on tier #4 of HSS(3)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 000 on tier #4 of HSS(4)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 111 on tier #4 of HSS(4)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 100 on tier #4 of HSS(4)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 011 on tier #4 of HSS(4)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 010 on tier #4 of HSS(4)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 110 on tier #4 of HSS(4)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 101 on tier #4 of HSS(4)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 001 on tier #4 of HSS(4)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 000 on tier #4 of HSS(5)
17:12:29,180|424 DEBUG [Helper] - Clearing leaf-vertex 111 on tier #4 of HSS(5)
17:12:29,181|425 DEBUG [Helper] - Clearing leaf-vertex 100 on tier #4 of HSS(5)
17:12:29,181|425 DEBUG [Helper] - Clearing leaf-vertex 011 on tier #4 of HSS(5)
17:12:29,181|425 DEBUG [Helper] - Clearing leaf-vertex 010 on tier #4 of HSS(5)
17:12:29,181|425 DEBUG [Helper] - Clearing leaf-vertex 110 on tier #4 of HSS(5)
17:12:29,181|425 DEBUG [Helper] - Clearing leaf-vertex 101 on tier #4 of HSS(5)
17:12:29,181|425 DEBUG [Helper] - Clearing leaf-vertex 001 on tier #4 of HSS(5)
17:12:29,181|425 DEBUG [Helper] - 48 leaf-vertices (vertices that were not shifted) were removed from tier #4
17:12:29,181|425 DEBUG [Helper] - Running unification of coincident substructures for tier #4
17:12:29,181|425 DEBUG [Helper] - Tier #4 of HSS contained 8 vertices before unification: 000, 001, 010, 011, 100, 101, 110, 111
17:12:29,181|425 DEBUG [Helper] - Found empty substructure-vertex assigned to vertex 000 of tier #4
17:12:29,181|425 DEBUG [Helper] - Vertex 000 removed from tier #4 of HSS(0): 001, 010, 011, 100, 101, 110, 111
17:12:29,181|425 DEBUG [Helper] - Coincident vertex 000 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110, 111
17:12:29,181|425 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,181|425 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,182|426 INFO [Helper] - --------------------------------------------------
17:12:29,182|426 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,182|426 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,182|426 INFO [Helper] - --------------------------------------------------
17:12:29,183|427 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,183|427 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,183|427 DEBUG [Helper] - Vertex 000 removed from tier #4 of HSS(1): 001, 010, 011, 100, 101, 110, 111
17:12:29,183|427 DEBUG [Helper] - Coincident vertex 000 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110, 111
17:12:29,183|427 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,183|427 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,183|427 INFO [Helper] - --------------------------------------------------
17:12:29,183|427 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,184|428 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,184|428 INFO [Helper] - --------------------------------------------------
17:12:29,184|428 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,184|428 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,184|428 DEBUG [Helper] - Vertex 000 removed from tier #4 of HSS(2): 001, 010, 011, 100, 101, 110, 111
17:12:29,184|428 DEBUG [Helper] - Coincident vertex 000 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110, 111
17:12:29,184|428 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,184|428 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,184|428 INFO [Helper] - --------------------------------------------------
17:12:29,185|429 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,186|430 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,186|430 INFO [Helper] - --------------------------------------------------
17:12:29,186|430 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,186|430 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,186|430 DEBUG [Helper] - Vertex 000 removed from tier #4 of HSS(3): 001, 010, 011, 100, 101, 110, 111
17:12:29,186|430 DEBUG [Helper] - Coincident vertex 000 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110, 111
17:12:29,186|430 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,186|430 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,186|430 INFO [Helper] - --------------------------------------------------
17:12:29,187|431 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,187|431 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,187|431 INFO [Helper] - --------------------------------------------------
17:12:29,187|431 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,187|431 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,187|431 DEBUG [Helper] - Vertex 000 removed from tier #4 of HSS(4): 001, 010, 011, 100, 101, 110, 111
17:12:29,187|431 DEBUG [Helper] - Coincident vertex 000 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110, 111
17:12:29,187|431 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,188|432 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,188|432 INFO [Helper] - --------------------------------------------------
17:12:29,188|432 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,188|432 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,188|432 INFO [Helper] - --------------------------------------------------
17:12:29,189|433 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,189|433 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,189|433 DEBUG [Helper] - Vertex 000 removed from tier #4 of HSS(5): 001, 010, 011, 100, 101, 110, 111
17:12:29,189|433 DEBUG [Helper] - Coincident vertex 000 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110, 111
17:12:29,189|433 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,189|433 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,189|433 INFO [Helper] - --------------------------------------------------
17:12:29,190|434 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,190|434 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,190|434 INFO [Helper] - --------------------------------------------------
17:12:29,190|434 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 78; TiersCount: 10
17:12:29,190|434 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,190|434 DEBUG [Helper] - Found empty substructure-vertex assigned to vertex 111 of tier #4
17:12:29,190|434 DEBUG [Helper] - Vertex 111 removed from tier #4 of HSS(0): 001, 010, 011, 100, 101, 110
17:12:29,190|434 DEBUG [Helper] - Coincident vertex 111 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110
17:12:29,190|434 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,191|435 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,191|435 INFO [Helper] - --------------------------------------------------
17:12:29,191|435 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,191|435 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,191|435 INFO [Helper] - --------------------------------------------------
17:12:29,191|435 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,192|436 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,192|436 DEBUG [Helper] - Vertex 111 removed from tier #4 of HSS(1): 001, 010, 011, 100, 101, 110
17:12:29,192|436 DEBUG [Helper] - Coincident vertex 111 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110
17:12:29,192|436 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,192|436 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,192|436 INFO [Helper] - --------------------------------------------------
17:12:29,192|436 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,193|437 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,193|437 INFO [Helper] - --------------------------------------------------
17:12:29,193|437 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,193|437 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,193|437 DEBUG [Helper] - Vertex 111 removed from tier #4 of HSS(2): 001, 010, 011, 100, 101, 110
17:12:29,193|437 DEBUG [Helper] - Coincident vertex 111 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110
17:12:29,193|437 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,193|437 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,193|437 INFO [Helper] - --------------------------------------------------
17:12:29,194|438 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,194|438 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,194|438 INFO [Helper] - --------------------------------------------------
17:12:29,194|438 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,194|438 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,194|438 DEBUG [Helper] - Vertex 111 removed from tier #4 of HSS(3): 001, 010, 011, 100, 101, 110
17:12:29,195|439 DEBUG [Helper] - Coincident vertex 111 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110
17:12:29,195|439 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,195|439 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,195|439 INFO [Helper] - --------------------------------------------------
17:12:29,195|439 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,195|439 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,195|439 INFO [Helper] - --------------------------------------------------
17:12:29,196|440 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,196|440 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,196|440 DEBUG [Helper] - Vertex 111 removed from tier #4 of HSS(4): 001, 010, 011, 100, 101, 110
17:12:29,196|440 DEBUG [Helper] - Coincident vertex 111 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110
17:12:29,196|440 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,196|440 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,196|440 INFO [Helper] - --------------------------------------------------
17:12:29,196|440 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,197|441 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,197|441 INFO [Helper] - --------------------------------------------------
17:12:29,197|441 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,197|441 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,197|441 DEBUG [Helper] - Vertex 111 removed from tier #4 of HSS(5): 001, 010, 011, 100, 101, 110
17:12:29,197|441 DEBUG [Helper] - Coincident vertex 111 removed from tier #4 of the BG: 001, 010, 011, 100, 101, 110
17:12:29,197|441 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,197|441 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,197|441 INFO [Helper] - --------------------------------------------------
17:12:29,199|443 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,199|443 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,199|443 INFO [Helper] - --------------------------------------------------
17:12:29,199|443 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 77; TiersCount: 10
17:12:29,199|443 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,199|443 DEBUG [Helper] - Found empty substructure-vertex assigned to vertex 100 of tier #4
17:12:29,200|444 DEBUG [Helper] - Vertex 100 removed from tier #4 of HSS(0): 001, 010, 011, 101, 110
17:12:29,200|444 DEBUG [Helper] - Coincident vertex 100 removed from tier #4 of the BG: 001, 010, 011, 101, 110
17:12:29,200|444 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,200|444 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,200|444 INFO [Helper] - --------------------------------------------------
17:12:29,201|445 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 76; TiersCount: 10
17:12:29,201|445 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,201|445 INFO [Helper] - --------------------------------------------------
17:12:29,201|445 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,202|446 DEBUG [Helper] - 2 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 1 tier(s) below (relatively to tier #4)
17:12:29,203|447 DEBUG [Helper] - Vertex 100 removed from tier #4 of HSS(1): 001, 010, 011, 101, 110
17:12:29,203|447 DEBUG [Helper] - Coincident vertex 100 removed from tier #4 of the BG: 001, 010, 011, 101, 110
17:12:29,203|447 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,203|447 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,204|448 INFO [Helper] - --------------------------------------------------
17:12:29,204|448 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,204|448 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,204|448 INFO [Helper] - --------------------------------------------------
17:12:29,204|448 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,204|448 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,204|448 DEBUG [Helper] - Vertex 100 removed from tier #4 of HSS(2): 001, 010, 011, 101, 110
17:12:29,205|449 DEBUG [Helper] - Coincident vertex 100 removed from tier #4 of the BG: 001, 010, 011, 101, 110
17:12:29,205|449 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,205|449 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,205|449 INFO [Helper] - --------------------------------------------------
17:12:29,205|449 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,205|449 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,205|449 INFO [Helper] - --------------------------------------------------
17:12:29,206|450 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,206|450 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,206|450 DEBUG [Helper] - Vertex 100 removed from tier #4 of HSS(3): 001, 010, 011, 101, 110
17:12:29,206|450 DEBUG [Helper] - Coincident vertex 100 removed from tier #4 of the BG: 001, 010, 011, 101, 110
17:12:29,206|450 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,206|450 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,206|450 INFO [Helper] - --------------------------------------------------
17:12:29,207|451 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,207|451 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,207|451 INFO [Helper] - --------------------------------------------------
17:12:29,207|451 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,207|451 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,207|451 DEBUG [Helper] - Vertex 100 removed from tier #4 of HSS(4): 001, 010, 011, 101, 110
17:12:29,207|451 DEBUG [Helper] - Coincident vertex 100 removed from tier #4 of the BG: 001, 010, 011, 101, 110
17:12:29,207|451 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,207|451 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,207|451 INFO [Helper] - --------------------------------------------------
17:12:29,208|452 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,208|452 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,208|452 INFO [Helper] - --------------------------------------------------
17:12:29,208|452 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,209|453 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,209|453 DEBUG [Helper] - Vertex 100 removed from tier #4 of HSS(5): 001, 010, 011, 101, 110
17:12:29,209|453 DEBUG [Helper] - Coincident vertex 100 removed from tier #4 of the BG: 001, 010, 011, 101, 110
17:12:29,209|453 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,209|453 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,209|453 INFO [Helper] - --------------------------------------------------
17:12:29,210|454 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,210|454 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,210|454 INFO [Helper] - --------------------------------------------------
17:12:29,210|454 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 74; TiersCount: 10
17:12:29,210|454 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,211|455 DEBUG [Helper] - Found empty substructure-vertex assigned to vertex 011 of tier #4
17:12:29,211|455 DEBUG [Helper] - Vertex 011 removed from tier #4 of HSS(0): 001, 010, 101, 110
17:12:29,211|455 DEBUG [Helper] - Coincident vertex 011 removed from tier #4 of the BG: 001, 010, 101, 110
17:12:29,211|455 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,211|455 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,211|455 INFO [Helper] - --------------------------------------------------
17:12:29,211|455 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 73; TiersCount: 10
17:12:29,211|455 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,211|455 INFO [Helper] - --------------------------------------------------
17:12:29,212|456 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,212|456 DEBUG [Helper] - 2 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 1 tier(s) below (relatively to tier #4)
17:12:29,212|456 DEBUG [Helper] - Vertex 011 removed from tier #4 of HSS(1): 001, 010, 101, 110
17:12:29,212|456 DEBUG [Helper] - Coincident vertex 011 removed from tier #4 of the BG: 001, 010, 101, 110
17:12:29,212|456 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,212|456 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,212|456 INFO [Helper] - --------------------------------------------------
17:12:29,212|456 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,212|456 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,213|457 INFO [Helper] - --------------------------------------------------
17:12:29,213|457 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,221|465 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,221|465 DEBUG [Helper] - Vertex 011 removed from tier #4 of HSS(2): 001, 010, 101, 110
17:12:29,221|465 DEBUG [Helper] - Coincident vertex 011 removed from tier #4 of the BG: 001, 010, 101, 110
17:12:29,221|465 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,221|465 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,221|465 INFO [Helper] - --------------------------------------------------
17:12:29,221|465 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,221|465 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,221|465 INFO [Helper] - --------------------------------------------------
17:12:29,222|466 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,301|545 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,301|545 DEBUG [Helper] - Vertex 011 removed from tier #4 of HSS(3): 001, 010, 101, 110
17:12:29,301|545 DEBUG [Helper] - Coincident vertex 011 removed from tier #4 of the BG: 001, 010, 101, 110
17:12:29,302|546 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,302|546 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,302|546 INFO [Helper] - --------------------------------------------------
17:12:29,302|546 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,302|546 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,302|546 INFO [Helper] - --------------------------------------------------
17:12:29,302|546 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,302|546 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,302|546 DEBUG [Helper] - Vertex 011 removed from tier #4 of HSS(4): 001, 010, 101, 110
17:12:29,302|546 DEBUG [Helper] - Coincident vertex 011 removed from tier #4 of the BG: 001, 010, 101, 110
17:12:29,303|547 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,303|547 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,303|547 INFO [Helper] - --------------------------------------------------
17:12:29,303|547 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,303|547 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,303|547 INFO [Helper] - --------------------------------------------------
17:12:29,304|548 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,304|548 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,304|548 DEBUG [Helper] - Vertex 011 removed from tier #4 of HSS(5): 001, 010, 101, 110
17:12:29,304|548 DEBUG [Helper] - Coincident vertex 011 removed from tier #4 of the BG: 001, 010, 101, 110
17:12:29,304|548 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,304|548 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,304|548 INFO [Helper] - --------------------------------------------------
17:12:29,304|548 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,305|549 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,305|549 INFO [Helper] - --------------------------------------------------
17:12:29,305|549 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
0 1 0
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 71; TiersCount: 10
17:12:29,305|549 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,305|549 DEBUG [Helper] - Found empty substructure-vertex assigned to vertex 010 of tier #4
17:12:29,305|549 DEBUG [Helper] - Vertex 010 removed from tier #4 of HSS(0): 001, 101, 110
17:12:29,305|549 DEBUG [Helper] - Coincident vertex 010 removed from tier #4 of the BG: 001, 101, 110
17:12:29,305|549 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,305|549 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,305|549 INFO [Helper] - --------------------------------------------------
17:12:29,305|549 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 70; TiersCount: 10
17:12:29,306|550 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,306|550 INFO [Helper] - --------------------------------------------------
17:12:29,306|550 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,306|550 DEBUG [Helper] - 2 vertices were removed from BG incuding some vertices in 1 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,306|550 DEBUG [Helper] - Vertex 010 removed from tier #4 of HSS(1): 001, 101, 110
17:12:29,306|550 DEBUG [Helper] - Coincident vertex 010 removed from tier #4 of the BG: 001, 101, 110
17:12:29,306|550 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,306|550 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,306|550 INFO [Helper] - --------------------------------------------------
17:12:29,307|551 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,308|552 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,308|552 INFO [Helper] - --------------------------------------------------
17:12:29,308|552 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,308|552 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,308|552 DEBUG [Helper] - Vertex 010 removed from tier #4 of HSS(2): 001, 101, 110
17:12:29,308|552 DEBUG [Helper] - Coincident vertex 010 removed from tier #4 of the BG: 001, 101, 110
17:12:29,308|552 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,308|552 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,308|552 INFO [Helper] - --------------------------------------------------
17:12:29,309|553 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,309|553 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,309|553 INFO [Helper] - --------------------------------------------------
17:12:29,309|553 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,309|553 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,309|553 DEBUG [Helper] - Vertex 010 removed from tier #4 of HSS(3): 001, 101, 110
17:12:29,309|553 DEBUG [Helper] - Coincident vertex 010 removed from tier #4 of the BG: 001, 101, 110
17:12:29,309|553 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,310|554 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,310|554 INFO [Helper] - --------------------------------------------------
17:12:29,310|554 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,310|554 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,310|554 INFO [Helper] - --------------------------------------------------
17:12:29,310|554 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,312|556 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,312|556 DEBUG [Helper] - Vertex 010 removed from tier #4 of HSS(4): 001, 101, 110
17:12:29,312|556 DEBUG [Helper] - Coincident vertex 010 removed from tier #4 of the BG: 001, 101, 110
17:12:29,312|556 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,312|556 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,312|556 INFO [Helper] - --------------------------------------------------
17:12:29,313|557 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,313|557 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,313|557 INFO [Helper] - --------------------------------------------------
17:12:29,313|557 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,313|557 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,313|557 DEBUG [Helper] - Vertex 010 removed from tier #4 of HSS(5): 001, 101, 110
17:12:29,313|557 DEBUG [Helper] - Coincident vertex 010 removed from tier #4 of the BG: 001, 101, 110
17:12:29,313|557 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,313|557 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,314|558 INFO [Helper] - --------------------------------------------------
17:12:29,314|558 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,314|558 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,314|558 INFO [Helper] - --------------------------------------------------
17:12:29,314|558 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 68; TiersCount: 10
17:12:29,314|558 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,314|558 DEBUG [Helper] - Found empty substructure-vertex assigned to vertex 110 of tier #4
17:12:29,314|558 DEBUG [Helper] - Vertex 110 removed from tier #4 of HSS(0): 001, 101
17:12:29,314|558 DEBUG [Helper] - Coincident vertex 110 removed from tier #4 of the BG: 001, 101
17:12:29,314|558 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,314|558 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,315|559 INFO [Helper] - --------------------------------------------------
17:12:29,315|559 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 1 0
1 1 1
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 67; TiersCount: 10
17:12:29,315|559 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,315|559 INFO [Helper] - --------------------------------------------------
17:12:29,315|559 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,315|559 DEBUG [Helper] - 8 vertices were removed from BG incuding some vertices in 1 tier(s) above and in 2 tier(s) below (relatively to tier #4)
17:12:29,317|561 DEBUG [Helper] - Vertex 110 removed from tier #4 of HSS(1): 001, 101
17:12:29,317|561 DEBUG [Helper] - Coincident vertex 110 removed from tier #4 of the BG: 001, 101
17:12:29,317|561 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,317|561 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,317|561 INFO [Helper] - --------------------------------------------------
17:12:29,317|561 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,317|561 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,317|561 INFO [Helper] - --------------------------------------------------
17:12:29,318|562 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,318|562 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,318|562 DEBUG [Helper] - Vertex 110 removed from tier #4 of HSS(2): 001, 101
17:12:29,318|562 DEBUG [Helper] - Coincident vertex 110 removed from tier #4 of the BG: 001, 101
17:12:29,318|562 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,318|562 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,318|562 INFO [Helper] - --------------------------------------------------
17:12:29,318|562 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,318|562 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,318|562 INFO [Helper] - --------------------------------------------------
17:12:29,318|562 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,319|563 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,319|563 DEBUG [Helper] - Vertex 110 removed from tier #4 of HSS(3): 001, 101
17:12:29,319|563 DEBUG [Helper] - Coincident vertex 110 removed from tier #4 of the BG: 001, 101
17:12:29,319|563 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,319|563 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,319|563 INFO [Helper] - --------------------------------------------------
17:12:29,319|563 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,319|563 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,319|563 INFO [Helper] - --------------------------------------------------
17:12:29,319|563 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,319|563 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,319|563 DEBUG [Helper] - Vertex 110 removed from tier #4 of HSS(4): 001, 101
17:12:29,320|564 DEBUG [Helper] - Coincident vertex 110 removed from tier #4 of the BG: 001, 101
17:12:29,320|564 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,320|564 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,320|564 INFO [Helper] - --------------------------------------------------
17:12:29,320|564 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,320|564 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,320|564 INFO [Helper] - --------------------------------------------------
17:12:29,320|564 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,321|565 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,321|565 DEBUG [Helper] - Vertex 110 removed from tier #4 of HSS(5): 001, 101
17:12:29,321|565 DEBUG [Helper] - Coincident vertex 110 removed from tier #4 of the BG: 001, 101
17:12:29,321|565 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,321|565 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,321|565 INFO [Helper] - --------------------------------------------------
17:12:29,321|565 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,321|565 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,321|565 INFO [Helper] - --------------------------------------------------
17:12:29,321|565 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 59; TiersCount: 10
17:12:29,321|565 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,322|566 DEBUG [Helper] - Found empty substructure-vertex assigned to vertex 101 of tier #4
17:12:29,322|566 DEBUG [Helper] - Vertex 101 removed from tier #4 of HSS(0): 001
17:12:29,322|566 DEBUG [Helper] - Coincident vertex 101 removed from tier #4 of the BG: 001
17:12:29,322|566 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,322|566 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,322|566 INFO [Helper] - --------------------------------------------------
17:12:29,322|566 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 58; TiersCount: 10
17:12:29,322|566 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,322|566 INFO [Helper] - --------------------------------------------------
17:12:29,322|566 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,322|566 DEBUG [Helper] - 6 vertices were removed from BG incuding some vertices in 2 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,322|566 DEBUG [Helper] - Vertex 101 removed from tier #4 of HSS(1): 001
17:12:29,322|566 DEBUG [Helper] - Coincident vertex 101 removed from tier #4 of the BG: 001
17:12:29,323|567 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,323|567 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,323|567 INFO [Helper] - --------------------------------------------------
17:12:29,323|567 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,323|567 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,323|567 INFO [Helper] - --------------------------------------------------
17:12:29,324|568 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,324|568 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,324|568 DEBUG [Helper] - Vertex 101 removed from tier #4 of HSS(2): 001
17:12:29,324|568 DEBUG [Helper] - Coincident vertex 101 removed from tier #4 of the BG: 001
17:12:29,324|568 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,324|568 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,324|568 INFO [Helper] - --------------------------------------------------
17:12:29,324|568 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,324|568 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,324|568 INFO [Helper] - --------------------------------------------------
17:12:29,324|568 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,324|568 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,325|569 DEBUG [Helper] - Vertex 101 removed from tier #4 of HSS(3): 001
17:12:29,325|569 DEBUG [Helper] - Coincident vertex 101 removed from tier #4 of the BG: 001
17:12:29,325|569 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,325|569 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,325|569 INFO [Helper] - --------------------------------------------------
17:12:29,325|569 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,325|569 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,325|569 INFO [Helper] - --------------------------------------------------
17:12:29,325|569 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,325|569 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,325|569 DEBUG [Helper] - Vertex 101 removed from tier #4 of HSS(4): 001
17:12:29,326|570 DEBUG [Helper] - Coincident vertex 101 removed from tier #4 of the BG: 001
17:12:29,326|570 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,326|570 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,326|570 INFO [Helper] - --------------------------------------------------
17:12:29,326|570 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,326|570 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,326|570 INFO [Helper] - --------------------------------------------------
17:12:29,326|570 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,326|570 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,326|570 DEBUG [Helper] - Vertex 101 removed from tier #4 of HSS(5): 001
17:12:29,326|570 DEBUG [Helper] - Coincident vertex 101 removed from tier #4 of the BG: 001
17:12:29,326|570 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,326|570 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,326|570 INFO [Helper] - --------------------------------------------------
17:12:29,327|571 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,327|571 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,327|571 INFO [Helper] - --------------------------------------------------
17:12:29,327|571 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 52; TiersCount: 10
17:12:29,327|571 DEBUG [Helper] - 0 vertices were removed from BG incuding some vertices in 0 tier(s) above and in 0 tier(s) below (relatively to tier #4)
17:12:29,327|571 DEBUG [Helper] - Found empty substructure-vertex assigned to vertex 001 of tier #4
17:12:29,327|571 DEBUG [Helper] - Vertex 001 removed from tier #4 of HSS(0):
17:12:29,328|572 DEBUG [Helper] - Coincident vertex 001 removed from tier #4 of the BG:
17:12:29,328|572 DEBUG [Helper] - Executing cleaup procedure on the basic structure...
17:12:29,328|572 DEBUG [Helper] - Basic structure before cleanup:
17:12:29,328|572 INFO [Helper] - --------------------------------------------------
17:12:29,328|572 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
1 0 0
1 1 0
0 0 0
1 0 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 12; ClausesCount: 51; TiersCount: 10
17:12:29,328|572 DEBUG [Helper] - Basic structure after cleanup:
17:12:29,328|572 INFO [Helper] - --------------------------------------------------
17:12:29,328|572 INFO [Helper] -
x10 x11 x12 x1 x2 x3 x4 x5 x6 x7 x8 x9
<empty>
VarCount: 12; ClausesCount: 0; TiersCount: 0
17:12:29,329|573 INFO [TestExamples] - Formula not satisfiable
com.anjlab.sat3.EmptyStructureException
at com.anjlab.sat3.Helper.removeVertexWithEmptySubstructureFromHSSAndBG(Helper.java:1438)
at com.anjlab.sat3.Helper.unifyCoincidentSubstructuresOfATier(Helper.java:1380)
at com.anjlab.sat3.Helper.clearLeafVertices(Helper.java:930)
at com.anjlab.sat3.Helper.createHyperStructuresSystem(Helper.java:852)
at com.anjlab.sat3.TestExamples.testHabr(TestExamples.java:78)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:44)
at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:15)
at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:41)
at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:20)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:76)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:50)
at org.junit.runners.ParentRunner$3.run(ParentRunner.java:193)
at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:52)
at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:191)
at org.junit.runners.ParentRunner.access$000(ParentRunner.java:42)
at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:184)
at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
at org.junit.runners.ParentRunner.run(ParentRunner.java:236)
at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:49)
at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:467)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:683)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:390)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:197)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment