Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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