Solving article example.cnf
#Satisfiable. Variable values from HSS route
#Mon Nov 15 10:14:25 MSK 2010
ImplementationVersion=1.0.3
InitialFormulaLoadTime=38
InitialFormulaVarCount=8
InitialFormulaClausesCount=44
CTFCreationTime=10
CTFCount=5
CTSCreationTime=5
CTSUnificationTime=13
BasicCTSInitialClausesCount=11
BasicCTSFinalClausesCount=11
HSSCreationTime=62
NumberOfHSSTiersBuilt=6
SearchHSSRouteTime=3
1=true
2=false
3=true
4=true
5=true
6=true
7=false
8=false
Note: File contents were reformatted for better reading.
See How to read output files wiki page for details.
With log4j level set to DEBUG (see lib\3-sat-core-1.0.3.jar\log4j.properties) and '-p' option.
C:\3-sat-experiment-1.0.3>solve -p examples/article-example.cnf
*******************************************************
* Java classpath: lib\3-sat-core-1.0.3.jar;lib\3-sat-experiment-1.0.3.jar;lib\colt-1.2.0.jar;
lib\commons-cli-1.2.jar;lib\concurrent-1.3.4.jar;lib\log4j-1.2.12.jar;lib\slf4j-api-1.6.1.jar;lib\slf4j-log4j12-1.6.1.jar
*******************************************************
* Running program
Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem
Copyright (c) 2010 AnjLab
This program comes with ABSOLUTELY NO WARRANTY.
This is free software, and you are welcome to redistribute it under certain conditions.
See LICENSE.txt file or visit <http://www.gnu.org/copyleft/lesser.html> for details.
10:14:24,376|0 DEBUG [Program] - Reading version number from manifest
Version: 1.0.3
10:14:24,400|24 INFO [Helper] - **********************************************************************
10:14:24,400|24 INFO [StopWatch] - Load formula...
Original VarCount: 8. Final VarCount: 8. Added: 0
10:14:24,438|62 INFO [Helper] - --------------------------------------------------
10:14:24,446|70 INFO [Helper] -
x1 x2 x3 x5 x6 x4 x8 x7
0 0 0
0 1 0
0 1 1
1 0 0
1 1 1
0 1 0
1 0 1
1 1 0
0 0 0
0 0 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 1 0
0 1 0
1 0 1
1 1 1
0 0 1
0 1 0
1 0 0
1 1 0
1 1 1
0 0 0
0 0 1
1 0 0
1 1 1
0 0 0
1 1 1
0 0 0
1 0 0
1 0 1
0 0 0
1 0 0
1 0 0
1 0 1
0 1 1
1 0 0
0 0 0
1 0 0
1 1 1
0 0 1
1 1 0
VarCount: 8; ClausesCount: 44; TiersCount: 15
10:14:24,449|73 INFO [StopWatch] - Load formula: 38ms; overall: 38ms
10:14:24,450|74 INFO [Helper] - **********************************************************************
10:14:24,450|74 INFO [StopWatch] - Clone initial formula...
10:14:24,450|74 INFO [StopWatch] - Clone initial formula: 0ms; overall: 38ms
10:14:24,450|74 INFO [Helper] - **********************************************************************
10:14:24,450|74 INFO [StopWatch] - Create CTF...
10:14:24,460|84 INFO [Helper] - --------------------------------------------------
10:14:24,460|84 INFO [Helper] -
x4 x6 x3 x1 x2 x5 x7
0 0 0
0 0 1
0 1 0
1 0 1
1 1 1
0 1 0
0 0 0
0 1 1
1 0 0
1 0 1
0 0 0
0 0 1
1 0 0
1 1 1
0 0 0
0 0 1
VarCount: 7; ClausesCount: 16; TiersCount: 5
10:14:24,460|84 INFO [Helper] - --------------------------------------------------
10:14:24,461|85 INFO [Helper] -
x5 x1 x6 x4 x2 x8 x7
0 1 1
1 1 0
0 1 0
0 1 1
1 0 0
1 1 0
0 0 1
0 1 0
1 0 0
1 1 0
1 1 1
VarCount: 7; ClausesCount: 11; TiersCount: 3
10:14:24,461|85 INFO [Helper] - --------------------------------------------------
10:14:24,461|85 INFO [Helper] -
x1 x3 x8 x2 x5 x6 x4
0 1 0
1 0 1
1 1 1
0 0 0
1 1 1
0 1 1
1 0 0
VarCount: 7; ClausesCount: 7; TiersCount: 3
10:14:24,461|85 INFO [Helper] - --------------------------------------------------
10:14:24,462|86 INFO [Helper] -
x4 x3 x5 x8 x6 x7
0 0 0
0 1 0
1 1 0
1 0 0
1 0 1
0 0 1
1 1 0
VarCount: 6; ClausesCount: 7; TiersCount: 3
10:14:24,462|86 INFO [Helper] - --------------------------------------------------
10:14:24,462|86 INFO [Helper] -
x5 x6 x7
0 0 0
1 0 0
1 1 1
VarCount: 3; ClausesCount: 3; TiersCount: 1
10:14:24,462|86 INFO [StopWatch] - Create CTF: 10ms; overall: 48ms
10:14:24,463|87 INFO [Program] - CTF count: 5
10:14:24,463|87 INFO [Helper] - **********************************************************************
10:14:24,464|88 INFO [StopWatch] - Create CTS...
10:14:24,469|93 INFO [Helper] - --------------------------------------------------
10:14:24,470|94 INFO [Helper] -
x4 x6 x3 x1 x2 x5 x7 x8
0 1 1
1 0 0
1 0 1
1 1 1
0 0 1
0 1 0
1 1 0
1 1 1
0 1 1
1 0 0
1 1 0
0 0 1
1 0 1
1 1 0
1 1 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 8; ClausesCount: 25; TiersCount: 6
10:14:24,470|94 INFO [Helper] - --------------------------------------------------
10:14:24,473|97 INFO [Helper] -
x5 x1 x6 x4 x2 x8 x7 x3
0 0 0
0 1 0
1 0 0
1 1 1
0 0 0
0 0 1
1 0 1
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
1 0 0
1 0 1
1 1 0
0 0 0
0 1 1
1 0 1
0 0 0
0 0 1
0 1 0
0 1 1
1 1 0
1 1 1
VarCount: 8; ClausesCount: 29; TiersCount: 6
10:14:24,473|97 INFO [Helper] - --------------------------------------------------
10:14:24,475|99 INFO [Helper] -
x1 x3 x8 x2 x5 x6 x4 x7
0 0 0
0 0 1
0 1 1
1 0 0
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 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
1 0 1
1 1 0
1 1 1
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: 8; ClausesCount: 41; TiersCount: 6
10:14:24,475|99 INFO [Helper] - --------------------------------------------------
10:14:24,480|104 INFO [Helper] -
x4 x3 x5 x8 x6 x7 x1 x2
0 0 1
0 1 1
1 0 0
1 0 1
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
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: 8; ClausesCount: 41; TiersCount: 6
10:14:24,480|104 INFO [Helper] - --------------------------------------------------
10:14:24,481|105 INFO [Helper] -
x5 x6 x7 x1 x2 x3 x4 x8
0 0 1
0 1 0
0 1 1
1 0 1
1 1 0
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
VarCount: 8; ClausesCount: 43; TiersCount: 6
10:14:24,481|105 INFO [StopWatch] - Create CTS: 5ms; overall: 53ms
10:14:24,481|105 INFO [Helper] - **********************************************************************
10:14:24,481|105 INFO [StopWatch] - Unify all CTS...
10:14:24,481|105 DEBUG [Helper] - Building pairs index...
10:14:24,486|110 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,486|110 DEBUG [Helper] - Running unify routine...
10:14:24,491|115 DEBUG [Helper] - Some clauses removed during unification
10:14:24,491|115 DEBUG [Helper] - Running unify routine...
10:14:24,493|117 DEBUG [Helper] - Some clauses removed during unification
10:14:24,493|117 DEBUG [Helper] - Running unify routine...
10:14:24,494|118 DEBUG [Helper] - No clauses removed during unification
10:14:24,494|118 INFO [Helper] - --------------------------------------------------
10:14:24,495|119 INFO [Helper] -
x4 x6 x3 x1 x2 x5 x7 x8
1 0 1
1 1 1
0 1 0
1 1 1
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 0
1 1 1
VarCount: 8; ClausesCount: 12; TiersCount: 6
10:14:24,495|119 INFO [Helper] - --------------------------------------------------
10:14:24,495|119 INFO [Helper] -
x5 x1 x6 x4 x2 x8 x7 x3
1 0 0
1 1 1
0 0 1
1 1 1
0 1 0
1 1 0
1 0 0
1 0 1
0 0 0
0 1 1
0 0 1
1 1 1
VarCount: 8; ClausesCount: 12; TiersCount: 6
10:14:24,495|119 INFO [Helper] - --------------------------------------------------
10:14:24,495|119 INFO [Helper] -
x1 x3 x8 x2 x5 x6 x4 x7
0 1 1
1 1 0
1 0 0
1 1 0
0 0 1
1 0 1
0 1 0
0 1 1
1 0 1
1 1 1
0 1 1
1 1 0
VarCount: 8; ClausesCount: 12; TiersCount: 6
10:14:24,495|119 INFO [Helper] - --------------------------------------------------
10:14:24,495|119 INFO [Helper] -
x4 x3 x5 x8 x6 x7 x1 x2
1 1 1
1 1 0
1 1 1
1 0 1
1 1 0
0 1 0
1 0 1
0 1 0
1 0 1
0 1 0
1 0 0
VarCount: 8; ClausesCount: 11; TiersCount: 6
10:14:24,495|119 INFO [Helper] - --------------------------------------------------
10:14:24,496|120 INFO [Helper] -
x5 x6 x7 x1 x2 x3 x4 x8
1 0 1
1 1 0
0 1 0
1 0 1
0 1 0
1 0 0
0 0 1
1 0 1
0 1 1
1 1 0
1 1 1
VarCount: 8; ClausesCount: 11; TiersCount: 6
10:14:24,496|120 INFO [StopWatch] - Unify all CTS: 13ms; overall: 66ms
10:14:24,496|120 INFO [Program] - CTF: 5
10:14:24,496|120 INFO [Helper] - **********************************************************************
10:14:24,496|120 INFO [StopWatch] - Create HSS...
10:14:24,496|120 INFO [Helper] - Building HSS tier #1 of 6
10:14:24,498|122 DEBUG [Helper] - Tier #1 of HSS contained 1 vertices before unification: 111
10:14:24,498|122 DEBUG [Helper] - Building pairs index...
10:14:24,499|123 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,499|123 DEBUG [Helper] - Running unify routine...
10:14:24,499|123 DEBUG [Helper] - No clauses removed during unification
10:14:24,500|124 DEBUG [Helper] - Tier #1 of HSS contained 1 vertices after unification: 111
10:14:24,500|124 INFO [Helper] - Building HSS tier #2 of 6
10:14:24,500|124 DEBUG [Helper] - HSS tier #1 is: 111
10:14:24,500|124 DEBUG [Helper] - Basic tier #1 is: 111
10:14:24,500|124 DEBUG [Helper] - Basic tier #2 is: 110, 111
10:14:24,501|125 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #1 of 6 total
10:14:24,501|125 DEBUG [Helper] - Building pairs index...
10:14:24,501|125 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,501|125 DEBUG [Helper] - Running unify routine...
10:14:24,502|126 DEBUG [Helper] - Some clauses removed during unification
10:14:24,502|126 DEBUG [Helper] - Running unify routine...
10:14:24,503|127 DEBUG [Helper] - No clauses removed during unification
10:14:24,503|127 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #1 of 6 total
10:14:24,503|127 DEBUG [Helper] - Building pairs index...
10:14:24,504|128 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,504|128 DEBUG [Helper] - Running unify routine...
10:14:24,505|129 DEBUG [Helper] - Some clauses removed during unification
10:14:24,505|129 DEBUG [Helper] - Running unify routine...
10:14:24,506|130 DEBUG [Helper] - No clauses removed during unification
10:14:24,506|130 DEBUG [Helper] - 0 leaf-vertices (vertices that were not shifted) were removed from tier #1
10:14:24,506|130 DEBUG [Helper] - Tier #2 of HSS contained 2 vertices before unification: 110, 111
10:14:24,506|130 DEBUG [Helper] - Building pairs index...
10:14:24,506|130 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,507|131 DEBUG [Helper] - Running unify routine...
10:14:24,507|131 DEBUG [Helper] - No clauses removed during unification
10:14:24,507|131 DEBUG [Helper] - Building pairs index...
10:14:24,508|132 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,508|132 DEBUG [Helper] - Running unify routine...
10:14:24,508|132 DEBUG [Helper] - No clauses removed during unification
10:14:24,509|133 DEBUG [Helper] - Tier #2 of HSS contained 2 vertices after unification: 110, 111
10:14:24,509|133 INFO [Helper] - Building HSS tier #3 of 6
10:14:24,509|133 DEBUG [Helper] - HSS tier #2 is: 110, 111
10:14:24,509|133 DEBUG [Helper] - Basic tier #2 is: 110, 111
10:14:24,509|133 DEBUG [Helper] - Basic tier #3 is: 101, 110
10:14:24,509|133 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #2 of 6 total
10:14:24,509|133 DEBUG [Helper] - Building pairs index...
10:14:24,510|134 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,510|134 DEBUG [Helper] - Running unify routine...
10:14:24,511|135 DEBUG [Helper] - No clauses removed during unification
10:14:24,511|135 DEBUG [Helper] - Building pairs index...
10:14:24,511|135 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,511|135 DEBUG [Helper] - Running unify routine...
10:14:24,512|136 DEBUG [Helper] - No clauses removed during unification
10:14:24,512|136 INFO [Helper] - Unify unions: s = 0, nextTierIndex = 2 of 5
10:14:24,512|136 DEBUG [Helper] - Building pairs index...
10:14:24,512|136 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,512|136 DEBUG [Helper] - Running unify routine...
10:14:24,513|137 DEBUG [Helper] - No clauses removed during unification
10:14:24,513|137 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 111 tier #2 of 6 total
10:14:24,513|137 DEBUG [Helper] - Building pairs index...
10:14:24,513|137 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,513|137 DEBUG [Helper] - Running unify routine...
10:14:24,514|138 DEBUG [Helper] - No clauses removed during unification
10:14:24,514|138 DEBUG [Helper] - Building pairs index...
10:14:24,514|138 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,514|138 DEBUG [Helper] - Running unify routine...
10:14:24,515|139 DEBUG [Helper] - No clauses removed during unification
10:14:24,515|139 INFO [Helper] - Unify unions: s = 0, nextTierIndex = 2 of 5
10:14:24,515|139 DEBUG [Helper] - Building pairs index...
10:14:24,515|139 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,515|139 DEBUG [Helper] - Running unify routine...
10:14:24,516|140 DEBUG [Helper] - No clauses removed during unification
10:14:24,516|140 DEBUG [Helper] - 0 leaf-vertices (vertices that were not shifted) were removed from tier #2
10:14:24,516|140 DEBUG [Helper] - Tier #3 of HSS contained 2 vertices before unification: 101, 110
10:14:24,516|140 DEBUG [Helper] - Building pairs index...
10:14:24,516|140 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,517|141 DEBUG [Helper] - Running unify routine...
10:14:24,517|141 DEBUG [Helper] - No clauses removed during unification
10:14:24,517|141 DEBUG [Helper] - Building pairs index...
10:14:24,517|141 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,517|141 DEBUG [Helper] - Running unify routine...
10:14:24,518|142 DEBUG [Helper] - No clauses removed during unification
10:14:24,518|142 DEBUG [Helper] - Tier #3 of HSS contained 2 vertices after unification: 101, 110
10:14:24,518|142 INFO [Helper] - Building HSS tier #4 of 6
10:14:24,518|142 DEBUG [Helper] - HSS tier #3 is: 101, 110
10:14:24,518|142 DEBUG [Helper] - Basic tier #3 is: 101, 110
10:14:24,518|142 DEBUG [Helper] - Basic tier #4 is: 010, 101
10:14:24,518|142 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #3 of 6 total
10:14:24,518|142 DEBUG [Helper] - Building pairs index...
10:14:24,519|143 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,519|143 DEBUG [Helper] - Running unify routine...
10:14:24,519|143 DEBUG [Helper] - No clauses removed during unification
10:14:24,519|143 DEBUG [Helper] - Building pairs index...
10:14:24,520|144 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,520|144 DEBUG [Helper] - Running unify routine...
10:14:24,520|144 DEBUG [Helper] - No clauses removed during unification
10:14:24,520|144 INFO [Helper] - Unify unions: s = 0, nextTierIndex = 3 of 5
10:14:24,520|144 DEBUG [Helper] - Building pairs index...
10:14:24,520|144 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,520|144 DEBUG [Helper] - Running unify routine...
10:14:24,521|145 DEBUG [Helper] - No clauses removed during unification
10:14:24,521|145 DEBUG [Helper] - Building pairs index...
10:14:24,521|145 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,521|145 DEBUG [Helper] - Running unify routine...
10:14:24,522|146 DEBUG [Helper] - No clauses removed during unification
10:14:24,522|146 DEBUG [Helper] - Building pairs index...
10:14:24,522|146 INFO [Helper] - Unify unions: s = 1, nextTierIndex = 3 of 5
10:14:24,522|146 DEBUG [Helper] - Building pairs index...
10:14:24,522|146 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,522|146 DEBUG [Helper] - Running unify routine...
10:14:24,523|147 DEBUG [Helper] - No clauses removed during unification
10:14:24,523|147 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 110 tier #3 of 6 total
10:14:24,523|147 DEBUG [Helper] - Building pairs index...
10:14:24,523|147 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,523|147 DEBUG [Helper] - Running unify routine...
10:14:24,523|147 DEBUG [Helper] - No clauses removed during unification
10:14:24,524|148 DEBUG [Helper] - Building pairs index...
10:14:24,524|148 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,524|148 DEBUG [Helper] - Running unify routine...
10:14:24,524|148 DEBUG [Helper] - No clauses removed during unification
10:14:24,524|148 INFO [Helper] - Unify unions: s = 0, nextTierIndex = 3 of 5
10:14:24,524|148 DEBUG [Helper] - Building pairs index...
10:14:24,525|149 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,525|149 DEBUG [Helper] - Running unify routine...
10:14:24,525|149 DEBUG [Helper] - No clauses removed during unification
10:14:24,525|149 DEBUG [Helper] - Building pairs index...
10:14:24,530|154 DEBUG [Helper] - Building pairs index...
10:14:24,531|155 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,531|155 DEBUG [Helper] - Running unify routine...
10:14:24,531|155 DEBUG [Helper] - No clauses removed during unification
10:14:24,531|155 INFO [Helper] - Unify unions: s = 1, nextTierIndex = 3 of 5
10:14:24,531|155 DEBUG [Helper] - Building pairs index...
10:14:24,531|155 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,531|155 DEBUG [Helper] - Running unify routine...
10:14:24,532|156 DEBUG [Helper] - No clauses removed during unification
10:14:24,532|156 DEBUG [Helper] - 0 leaf-vertices (vertices that were not shifted) were removed from tier #3
10:14:24,532|156 DEBUG [Helper] - Tier #4 of HSS contained 2 vertices before unification: 010, 101
10:14:24,532|156 DEBUG [Helper] - Building pairs index...
10:14:24,532|156 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,532|156 DEBUG [Helper] - Running unify routine...
10:14:24,532|156 DEBUG [Helper] - No clauses removed during unification
10:14:24,532|156 DEBUG [Helper] - Building pairs index...
10:14:24,533|157 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,533|157 DEBUG [Helper] - Running unify routine...
10:14:24,533|157 DEBUG [Helper] - No clauses removed during unification
10:14:24,533|157 DEBUG [Helper] - Tier #4 of HSS contained 2 vertices after unification: 010, 101
10:14:24,533|157 INFO [Helper] - Building HSS tier #5 of 6
10:14:24,533|157 DEBUG [Helper] - HSS tier #4 is: 010, 101
10:14:24,533|157 DEBUG [Helper] - Basic tier #4 is: 010, 101
10:14:24,534|158 DEBUG [Helper] - Basic tier #5 is: 010, 101
10:14:24,534|158 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #4 of 6 total
10:14:24,534|158 DEBUG [Helper] - Building pairs index...
10:14:24,534|158 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,534|158 DEBUG [Helper] - Running unify routine...
10:14:24,534|158 DEBUG [Helper] - No clauses removed during unification
10:14:24,534|158 DEBUG [Helper] - Building pairs index...
10:14:24,535|159 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,535|159 DEBUG [Helper] - Running unify routine...
10:14:24,535|159 DEBUG [Helper] - No clauses removed during unification
10:14:24,535|159 INFO [Helper] - Unify unions: s = 0, nextTierIndex = 4 of 5
10:14:24,535|159 DEBUG [Helper] - Building pairs index...
10:14:24,535|159 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,535|159 DEBUG [Helper] - Running unify routine...
10:14:24,535|159 DEBUG [Helper] - No clauses removed during unification
10:14:24,536|160 DEBUG [Helper] - Building pairs index...
10:14:24,536|160 DEBUG [Helper] - Building pairs index...
10:14:24,536|160 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,536|160 DEBUG [Helper] - Running unify routine...
10:14:24,536|160 DEBUG [Helper] - No clauses removed during unification
10:14:24,536|160 INFO [Helper] - Unify unions: s = 1, nextTierIndex = 4 of 5
10:14:24,537|161 DEBUG [Helper] - Building pairs index...
10:14:24,537|161 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,537|161 DEBUG [Helper] - Running unify routine...
10:14:24,537|161 DEBUG [Helper] - No clauses removed during unification
10:14:24,537|161 DEBUG [Helper] - Building pairs index...
10:14:24,537|161 DEBUG [Helper] - Building pairs index...
10:14:24,537|161 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,538|162 DEBUG [Helper] - Running unify routine...
10:14:24,538|162 DEBUG [Helper] - No clauses removed during unification
10:14:24,538|162 INFO [Helper] - Unify unions: s = 2, nextTierIndex = 4 of 5
10:14:24,538|162 DEBUG [Helper] - Building pairs index...
10:14:24,538|162 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,538|162 DEBUG [Helper] - Running unify routine...
10:14:24,538|162 DEBUG [Helper] - No clauses removed during unification
10:14:24,539|163 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #4 of 6 total
10:14:24,539|163 DEBUG [Helper] - Building pairs index...
10:14:24,539|163 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,539|163 DEBUG [Helper] - Running unify routine...
10:14:24,539|163 DEBUG [Helper] - No clauses removed during unification
10:14:24,539|163 DEBUG [Helper] - Building pairs index...
10:14:24,540|164 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,540|164 DEBUG [Helper] - Running unify routine...
10:14:24,540|164 DEBUG [Helper] - No clauses removed during unification
10:14:24,540|164 INFO [Helper] - Unify unions: s = 0, nextTierIndex = 4 of 5
10:14:24,540|164 DEBUG [Helper] - Building pairs index...
10:14:24,540|164 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,540|164 DEBUG [Helper] - Running unify routine...
10:14:24,540|164 DEBUG [Helper] - No clauses removed during unification
10:14:24,541|165 DEBUG [Helper] - Building pairs index...
10:14:24,541|165 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,541|165 DEBUG [Helper] - Running unify routine...
10:14:24,541|165 DEBUG [Helper] - No clauses removed during unification
10:14:24,541|165 DEBUG [Helper] - Building pairs index...
10:14:24,541|165 INFO [Helper] - Unify unions: s = 1, nextTierIndex = 4 of 5
10:14:24,541|165 DEBUG [Helper] - Building pairs index...
10:14:24,542|166 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,542|166 DEBUG [Helper] - Running unify routine...
10:14:24,542|166 DEBUG [Helper] - No clauses removed during unification
10:14:24,542|166 DEBUG [Helper] - Building pairs index...
10:14:24,542|166 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,542|166 DEBUG [Helper] - Running unify routine...
10:14:24,543|167 DEBUG [Helper] - No clauses removed during unification
10:14:24,543|167 DEBUG [Helper] - Building pairs index...
10:14:24,543|167 INFO [Helper] - Unify unions: s = 2, nextTierIndex = 4 of 5
10:14:24,543|167 DEBUG [Helper] - Building pairs index...
10:14:24,543|167 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,543|167 DEBUG [Helper] - Running unify routine...
10:14:24,543|167 DEBUG [Helper] - No clauses removed during unification
10:14:24,544|168 DEBUG [Helper] - 0 leaf-vertices (vertices that were not shifted) were removed from tier #4
10:14:24,544|168 DEBUG [Helper] - Tier #5 of HSS contained 2 vertices before unification: 010, 101
10:14:24,544|168 DEBUG [Helper] - Building pairs index...
10:14:24,544|168 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,544|168 DEBUG [Helper] - Running unify routine...
10:14:24,544|168 DEBUG [Helper] - No clauses removed during unification
10:14:24,544|168 DEBUG [Helper] - Building pairs index...
10:14:24,544|168 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,544|168 DEBUG [Helper] - Running unify routine...
10:14:24,545|169 DEBUG [Helper] - No clauses removed during unification
10:14:24,545|169 DEBUG [Helper] - Tier #5 of HSS contained 2 vertices after unification: 010, 101
10:14:24,545|169 INFO [Helper] - Building HSS tier #6 of 6
10:14:24,545|169 DEBUG [Helper] - HSS tier #5 is: 010, 101
10:14:24,545|169 DEBUG [Helper] - Basic tier #5 is: 010, 101
10:14:24,545|169 DEBUG [Helper] - Basic tier #6 is: 010, 100
10:14:24,545|169 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 101 tier #5 of 6 total
10:14:24,545|169 DEBUG [Helper] - Building pairs index...
10:14:24,546|170 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,546|170 DEBUG [Helper] - Running unify routine...
10:14:24,546|170 DEBUG [Helper] - No clauses removed during unification
10:14:24,546|170 DEBUG [Helper] - Building pairs index...
10:14:24,546|170 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,546|170 DEBUG [Helper] - Running unify routine...
10:14:24,546|170 DEBUG [Helper] - No clauses removed during unification
10:14:24,547|171 INFO [Helper] - Unify unions: s = 0, nextTierIndex = 5 of 5
10:14:24,547|171 DEBUG [Helper] - Building pairs index...
10:14:24,547|171 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,547|171 DEBUG [Helper] - Running unify routine...
10:14:24,547|171 DEBUG [Helper] - No clauses removed during unification
10:14:24,547|171 DEBUG [Helper] - Building pairs index...
10:14:24,547|171 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,547|171 DEBUG [Helper] - Running unify routine...
10:14:24,548|172 DEBUG [Helper] - No clauses removed during unification
10:14:24,548|172 DEBUG [Helper] - Building pairs index...
10:14:24,548|172 INFO [Helper] - Unify unions: s = 1, nextTierIndex = 5 of 5
10:14:24,548|172 DEBUG [Helper] - Building pairs index...
10:14:24,548|172 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,548|172 DEBUG [Helper] - Running unify routine...
10:14:24,548|172 DEBUG [Helper] - No clauses removed during unification
10:14:24,549|173 DEBUG [Helper] - Building pairs index...
10:14:24,549|173 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,549|173 DEBUG [Helper] - Running unify routine...
10:14:24,549|173 DEBUG [Helper] - No clauses removed during unification
10:14:24,549|173 DEBUG [Helper] - Building pairs index...
10:14:24,549|173 INFO [Helper] - Unify unions: s = 2, nextTierIndex = 5 of 5
10:14:24,549|173 DEBUG [Helper] - Building pairs index...
10:14:24,549|173 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,549|173 DEBUG [Helper] - Running unify routine...
10:14:24,550|174 DEBUG [Helper] - No clauses removed during unification
10:14:24,550|174 DEBUG [Helper] - Building pairs index...
10:14:24,550|174 DEBUG [Helper] - Building pairs index...
10:14:24,550|174 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,550|174 DEBUG [Helper] - Running unify routine...
10:14:24,550|174 DEBUG [Helper] - No clauses removed during unification
10:14:24,551|175 INFO [Helper] - Unify unions: s = 3, nextTierIndex = 5 of 5
10:14:24,551|175 DEBUG [Helper] - Building pairs index...
10:14:24,551|175 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,551|175 DEBUG [Helper] - Running unify routine...
10:14:24,551|175 DEBUG [Helper] - No clauses removed during unification
10:14:24,551|175 DEBUG [Helper] - Unify intermediate structures after concretization during concordant shift of 010 tier #5 of 6 total
10:14:24,551|175 DEBUG [Helper] - Building pairs index...
10:14:24,551|175 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,551|175 DEBUG [Helper] - Running unify routine...
10:14:24,552|176 DEBUG [Helper] - No clauses removed during unification
10:14:24,552|176 DEBUG [Helper] - Building pairs index...
10:14:24,552|176 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,552|176 DEBUG [Helper] - Running unify routine...
10:14:24,552|176 DEBUG [Helper] - No clauses removed during unification
10:14:24,552|176 INFO [Helper] - Unify unions: s = 0, nextTierIndex = 5 of 5
10:14:24,552|176 DEBUG [Helper] - Building pairs index...
10:14:24,552|176 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,552|176 DEBUG [Helper] - Running unify routine...
10:14:24,553|177 DEBUG [Helper] - No clauses removed during unification
10:14:24,553|177 DEBUG [Helper] - Building pairs index...
10:14:24,553|177 DEBUG [Helper] - Building pairs index...
10:14:24,553|177 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,553|177 DEBUG [Helper] - Running unify routine...
10:14:24,554|178 DEBUG [Helper] - No clauses removed during unification
10:14:24,554|178 INFO [Helper] - Unify unions: s = 1, nextTierIndex = 5 of 5
10:14:24,554|178 DEBUG [Helper] - Building pairs index...
10:14:24,554|178 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,554|178 DEBUG [Helper] - Running unify routine...
10:14:24,554|178 DEBUG [Helper] - No clauses removed during unification
10:14:24,554|178 DEBUG [Helper] - Building pairs index...
10:14:24,555|179 DEBUG [Helper] - Building pairs index...
10:14:24,555|179 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,555|179 DEBUG [Helper] - Running unify routine...
10:14:24,555|179 DEBUG [Helper] - No clauses removed during unification
10:14:24,555|179 INFO [Helper] - Unify unions: s = 2, nextTierIndex = 5 of 5
10:14:24,555|179 DEBUG [Helper] - Building pairs index...
10:14:24,555|179 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,555|179 DEBUG [Helper] - Running unify routine...
10:14:24,556|180 DEBUG [Helper] - No clauses removed during unification
10:14:24,556|180 DEBUG [Helper] - Building pairs index...
10:14:24,556|180 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,556|180 DEBUG [Helper] - Running unify routine...
10:14:24,556|180 DEBUG [Helper] - No clauses removed during unification
10:14:24,556|180 DEBUG [Helper] - Building pairs index...
10:14:24,556|180 INFO [Helper] - Unify unions: s = 3, nextTierIndex = 5 of 5
10:14:24,556|180 DEBUG [Helper] - Building pairs index...
10:14:24,557|181 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,557|181 DEBUG [Helper] - Running unify routine...
10:14:24,557|181 DEBUG [Helper] - No clauses removed during unification
10:14:24,557|181 DEBUG [Helper] - 0 leaf-vertices (vertices that were not shifted) were removed from tier #5
10:14:24,557|181 DEBUG [Helper] - Tier #6 of HSS contained 2 vertices before unification: 010, 100
10:14:24,557|181 DEBUG [Helper] - Building pairs index...
10:14:24,557|181 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,557|181 DEBUG [Helper] - Running unify routine...
10:14:24,557|181 DEBUG [Helper] - No clauses removed during unification
10:14:24,558|182 DEBUG [Helper] - Building pairs index...
10:14:24,558|182 DEBUG [Helper] - Removed 7 triplet permutations from index
10:14:24,558|182 DEBUG [Helper] - Running unify routine...
10:14:24,558|182 DEBUG [Helper] - No clauses removed during unification
10:14:24,558|182 DEBUG [Helper] - Tier #6 of HSS contained 2 vertices after unification: 010, 100
10:14:24,558|182 INFO [StopWatch] - Create HSS: 62ms; overall: 128ms
10:14:24,558|182 INFO [Helper] - **********************************************************************
10:14:24,558|182 INFO [StopWatch] - Find HSS(0) route...
10:14:24,561|185 INFO [StopWatch] - Find HSS(0) route: 3ms; overall: 131ms
10:14:24,561|185 INFO [Helper] - **********************************************************************
10:14:24,561|185 INFO [StopWatch] - Verify formula is satisfiable using variable values from HSS route...
10:14:24,561|185 INFO [Program] - Initial formula verified as satisfiable with variables from HSS route
10:14:24,562|186 INFO [Program] - CTF verified as satisfiable with variables from HSS route
10:14:24,562|186 INFO [StopWatch] - Verify formula is satisfiable using variable values from HSS route: 1ms; overall: 132ms
10:14:24,562|186 INFO [Helper] - **********************************************************************
10:14:24,562|186 INFO [StopWatch] - Write HSS as image to examples\article-example.cnf-hss-0.png...
10:14:25,260|884 INFO [StopWatch] - Write HSS as image to examples\article-example.cnf-hss-0.png: 698ms; overall: 830ms
10:14:25,261|885 INFO [Helper] - **********************************************************************
10:14:25,261|885 INFO [StopWatch] - Write HSS route to examples\article-example.cnf-results.txt...
10:14:25,267|891 INFO [StopWatch] - Write HSS route to examples\article-example.cnf-results.txt: 6ms; overall: 836ms
Program completed