PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-noswot.opb
MD5SUM	64bde1e66dd22efb34c363a61fb9a0ef
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-41
Optimality of the best value was proved	NO
Number of terms in the objective function	425
Biggest coefficient in the objective function	65536
Number of bits for the biggest coefficient in the objective function	17
Sum of the numbers in the objective function	3276775
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	2275540926464
Number of bits of the biggest number in a constraint	42
Biggest sum of numbers in a constraint	4715313641679
Number of bits of the biggest sum of numbers	43
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	139.56
Number of variables	1060
Total number of constraints	282
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	75
Number of constraints which are nor clauses,nor cardinality constraints	207
Minimum length of a constraint	1
Maximum length of a constraint	425
Trace number 32300

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-05-27 09:15:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23728 boxname=wulflinc25 idbench=1372 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  64bde1e66dd22efb34c363a61fb9a0ef  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-noswot.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-noswot.opb
IDLAUNCH: 23728
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        901368 kB
Buffers:           144 kB
Cached:         113604 kB
SwapCached:        900 kB
Active:          18620 kB
Inactive:        97072 kB
HighTotal:      131008 kB
HighFree:        14476 kB
LowTotal:       903652 kB
LowFree:        886892 kB
SwapTotal:     2097892 kB
SwapFree:      2095960 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4916 kB
Slab:            11876 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 09:17:39 (client local time) WITH STATUS 30 IN 139.56 SECONDS
stats: 23728 0 139.56 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 209 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###
c   -- Clauses(.)/Splits(s): .........................
c ---[ 183]---> BDD-cost:  808
c ---[ 182]---> BDD-cost:    6
c ---[ 181]---> BDD-cost:  592
c ---[ 180]---> BDD-cost:  230
c ---[ 179]---> BDD-cost:  519
c ---[ 177]---> BDD-cost:   49
c ---[ 176]---> BDD-cost:   43
c ---[ 175]---> BDD-cost:   43
c ---[ 174]---> BDD-cost:   43
c ---[ 173]---> BDD-cost:   43
c ---[ 172]---> BDD-cost:   43
c ---[ 169]---> BDD-cost:    2
c ---[ 167]---> BDD-cost:    2
c ---[ 165]---> BDD-cost:    2
c ---[ 163]---> BDD-cost:    2
c ---[ 161]---> BDD-cost:    2
c ---[ 160]---> BDD-cost:    6
c ---[ 159]---> BDD-cost:  169
c ---[ 158]---> BDD-cost:  272
c ---[ 157]---> BDD-cost:  169
c ---[ 156]---> BDD-cost:  272
c ---[ 155]---> BDD-cost:  169
c ---[ 154]---> BDD-cost:  272
c ---[ 153]---> BDD-cost:  169
c ---[ 152]---> BDD-cost:  272
c ---[ 151]---> BDD-cost:  169
c ---[ 150]---> BDD-cost:  272
c ---[ 148]---> BDD-cost:  249
c ---[ 147]---> BDD-cost:  241
c ---[ 146]---> BDD-cost:  249
c ---[ 145]---> BDD-cost:  241
c ---[ 144]---> BDD-cost:  249
c ---[ 143]---> BDD-cost:  241
c ---[ 142]---> BDD-cost:  249
c ---[ 141]---> BDD-cost:  241
c ---[ 140]---> BDD-cost:  249
c ---[ 139]---> BDD-cost:  241
c ---[ 138]---> BDD-cost:    6
c ---[ 137]---> BDD-cost:   19
c ---[ 136]---> BDD-cost:   24
c ---[ 135]---> BDD-cost:   24
c ---[ 134]---> BDD-cost:   24
c ---[ 133]---> BDD-cost:   24
c ---[ 132]---> BDD-cost:   24
c ---[ 129]---> BDD-cost:   12
c ---[ 126]---> BDD-cost:   12
c ---[ 123]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:    4
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:  249
c ---[ 117]---> BDD-cost:  102
c ---[ 116]---> BDD-cost:  249
c ---[ 115]---> BDD-cost:  102
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:  249
c ---[ 112]---> BDD-cost:  102
c ---[ 111]---> BDD-cost:  249
c ---[ 110]---> BDD-cost:  102
c ---[ 109]---> BDD-cost:  249
c ---[ 108]---> BDD-cost:  102
c ---[ 107]---> BDD-cost:    7
c ---[ 106]---> BDD-cost:   42
c ---[ 105]---> BDD-cost:   42
c ---[ 104]---> BDD-cost:   42
c ---[ 103]---> BDD-cost:  592
c ---[ 102]---> BDD-cost:   42
c ---[ 101]---> BDD-cost:   40
c ---[  99]---> BDD-cost:    2
c ---[  97]---> BDD-cost:    2
c ---[  95]---> BDD-cost:    2
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:  493
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:  592
c ---[  87]---> BDD-cost:   80
c ---[  86]---> BDD-cost:  493
c ---[  85]---> BDD-cost:  592
c ---[  84]---> BDD-cost:  493
c ---[  83]---> BDD-cost:  592
c ---[  82]---> BDD-cost:  493
c ---[  81]---> BDD-cost:  592
c ---[  80]---> BDD-cost:  308
c ---[  79]---> BDD-cost:  322
c ---[  78]---> BDD-cost:  521
c ---[  77]---> BDD-cost:  322
c ---[  76]---> BDD-cost:   80
c ---[  75]---> BDD-cost:  521
c ---[  74]---> BDD-cost:  322
c ---[  73]---> BDD-cost:  521
c ---[  72]---> BDD-cost:  322
c ---[  71]---> BDD-cost:  521
c ---[  70]---> BDD-cost:  322
c ---[  69]---> BDD-cost:  314
c ---[  68]---> BDD-cost:  123
c ---[  67]---> BDD-cost:  526
c ---[  66]---> BDD-cost:  123
c ---[  65]---> BDD-cost:   80
c ---[  64]---> BDD-cost:  526
c ---[  63]---> BDD-cost:  123
c ---[  62]---> BDD-cost:  526
c ---[  61]---> BDD-cost:  123
c ---[  60]---> BDD-cost:  526
c ---[  59]---> BDD-cost:  123
c ---[  58]---> BDD-cost:  352
c ---[  57]---> BDD-cost:  249
c ---[  56]---> BDD-cost:  487
c ---[  55]---> BDD-cost:  249
c ---[  54]---> BDD-cost:   80
c ---[  53]---> BDD-cost:  487
c ---[  52]---> BDD-cost:  249
c ---[  51]---> BDD-cost:  487
c ---[  50]---> BDD-cost:  249
c ---[  49]---> BDD-cost:  487
c ---[  48]---> BDD-cost:  249
c ---[  47]---> BDD-cost:  313
c ---[  46]---> BDD-cost:   66
c ---[  45]---> BDD-cost:   75
c ---[  44]---> BDD-cost:   75
c ---[  43]---> BDD-cost:   62
c ---[  42]---> BDD-cost:   75
c ---[  41]---> BDD-cost:   75
c ---[  40]---> BDD-cost:   63
c ---[  38]---> BDD-cost:    5
c ---[  36]---> BDD-cost:    5
c ---[  34]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    4
c ---[  28]---> BDD-cost:  272
c ---[  27]---> BDD-cost:  516
c ---[  26]---> BDD-cost:  272
c ---[  25]---> BDD-cost:  516
c ---[  24]---> BDD-cost:  272
c ---[  23]---> BDD-cost:  516
c ---[  22]---> BDD-cost:  272
c ---[  21]---> BDD-cost:    6
c ---[  20]---> BDD-cost:  516
c ---[  19]---> BDD-cost:  272
c ---[  18]---> BDD-cost:  516
c ---[  17]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  561
c ---[  15]---> BDD-cost:  131
c ---[  14]---> BDD-cost:  561
c ---[  13]---> BDD-cost:  131
c ---[  12]---> BDD-cost:  561
c ---[  11]---> BDD-cost:  131
c ---[   9]---> BDD-cost:  561
c ---[   8]---> BDD-cost:  131
c ---[   7]---> BDD-cost:  561
c ---[   6]---> BDD-cost:  230
c ---[   5]---> BDD-cost:  519
c ---[   4]---> BDD-cost:  230
c ---[   3]---> BDD-cost:  519
c ---[   2]---> BDD-cost:  230
c ---[   1]---> BDD-cost:  519
c ---[   0]---> BDD-cost:  157
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   74445   208250 |   24815       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -20[0m
c ---[   0]---> Sorter-cost: 1157     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        16 |   76742   213621 |   25580      15       89     5.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: -28[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        62 |   76628   213375 |   25542      53      307     5.8 |  0.000 % |
c ==============================================================================
c [1mFound solution: -35[0m
c ---[   0]---> Sorter-cost:    1     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        91 |   76647   213430 |   25549      82      513     6.3 |  0.000 % |
c ==============================================================================
c [1mFound solution: -36[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       143 |   76651   213443 |   25550     134      921     6.9 |  0.000 % |
c |       246 |   76651   213443 |   28105     237     2367    10.0 |  6.706 % |
c |       396 |   76651   213443 |   30915     387     3783     9.8 |  6.706 % |
c |       621 |   76409   212898 |   34007     547     6291    11.5 |  6.951 % |
c |       959 |   76401   212880 |   37407     882    11344    12.9 |  6.957 % |
c ==============================================================================
c [1mFound solution: -39[0m
c ---[   0]---> Sorter-cost:    1     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       987 |   76405   212892 |   25468     910    11576    12.7 |  6.957 % |
c |      1088 |   76405   212892 |   28014    1011    13182    13.0 |  6.959 % |
c |      1238 |   76332   212725 |   30816    1159    16129    13.9 |  7.041 % |
c |      1463 |   76332   212725 |   33897    1384    19907    14.4 |  7.041 % |
c |      1801 |   76303   212658 |   37287    1714    24577    14.3 |  7.074 % |
c |      2308 |   76303   212658 |   41016    2221    32326    14.6 |  7.074 % |
c |      3068 |   76293   212635 |   45118    2977    44491    14.9 |  7.083 % |
c |      4209 |   76293   212635 |   49629    4118    64496    15.7 |  7.083 % |
c |      5917 |   76293   212635 |   54592    5826    93101    16.0 |  7.083 % |
c |      8479 |   76293   212635 |   60052    8388   138809    16.5 |  7.083 % |
c ==============================================================================
c [1mFound solution: -40[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11396 |   76288   212624 |   25429   11300   191241    16.9 |  7.083 % |
c |     11497 |   76288   212624 |   27971   11401   193817    17.0 |  7.092 % |
c |     11648 |   76275   212597 |   30769   11547   197444    17.1 |  7.113 % |
c |     11875 |   76275   212597 |   33845   11774   202269    17.2 |  7.113 % |
c ==============================================================================
c [1mFound solution: -41[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12051 |   76279   212617 |   25426   11950   206301    17.3 |  7.113 % |
c |     12151 |   76279   212617 |   27968   12050   208210    17.3 |  7.115 % |
c |     12301 |   76279   212617 |   30765   12200   211309    17.3 |  7.115 % |
c |     12527 |   76279   212617 |   33842   12426   215188    17.3 |  7.115 % |
c |     12867 |   76279   212617 |   37226   12766   221268    17.3 |  7.115 % |
c |     13375 |   76279   212617 |   40948   13274   230349    17.4 |  7.115 % |
c |     14134 |   76279   212617 |   45043   14033   247520    17.6 |  7.115 % |
c |     15273 |   76279   212617 |   49548   15172   270413    17.8 |  7.115 % |
c |     16982 |   76279   212617 |   54502   16881   305187    18.1 |  7.115 % |
c |     19545 |   76279   212617 |   59953   19444   350686    18.0 |  7.115 % |
c |     23390 |   76279   212617 |   65948   23289   425377    18.3 |  7.115 % |
c |     29157 |   76240   212528 |   72543   29052   543682    18.7 |  7.155 % |
c |     37807 |   76194   212405 |   79797    8304   125526    15.1 |  7.176 % |
c ==============================================================================
c [1mOptimal solution: -41[0m
s OPTIMUM FOUND
v x52_bit0 x52_bit1 x52_bit2 -x52_bit3 -x52_bit4 -x52_bit5 -x52_bit6 -x52_bit7 -x52_bit8 -x52_bit9 -x52_bit10 -x52_bit11 -x52_bit12 -x52_bit13 -x52_bit14 -x52_bit15 -x52_bit16 x54_bit0 -x54_bit1 -x54_bit2 x54_bit3 -x54_bit4 -x54_bit5 -x54_bit6 -x54_bit7 -x54_bit8 -x54_bit9 -x54_bit10 -x54_bit11 -x54_bit12 -x54_bit13 -x54_bit14 -x54_bit15 -x54_bit16 -x56_bit0 x56_bit1 -x56_bit2 -x56_bit3 -x56_bit4 -x56_bit5 -x56_bit6 -x56_bit7 -x56_bit8 -x56_bit9 -x56_bit10 -x56_bit11 -x56_bit12 -x56_bit13 -x56_bit14 -x56_bit15 -x56_bit16 -x58_bit0 -x58_bit1 -x58_bit2 x58_bit3 -x58_bit4 -x58_bit5 -x58_bit6 -x58_bit7 -x58_bit8 -x58_bit9 -x58_bit10 -x58_bit11 -x58_bit12 -x58_bit13 -x58_bit14 -x58_bit15 -x58_bit16 x60_bit0 x60_bit1 x60_bit2 -x60_bit3 -x60_bit4 -x60_bit5 -x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 -x60_bit10 -x60_bit11 -x60_bit12 -x60_bit13 -x60_bit14 -x60_bit15 -x60_bit16 -x62_bit0 -x62_bit1 -x62_bit2 -x62_bit3 -x62_bit4 -x62_bit5 -x62_bit6 -x62_bit7 -x62_bit8 -x62_bit9 -x62_bit10 -x62_bit11 -x62_bit12 -x62_bit13 -x62_bit14 -x62_bit15 -x62_bit16 -x64_bit0 -x64_bit1 -x64_bit2 -x64_bit3 -x64_bit4 -x64_bit5 -x64_bit6 -x64_bit7 -x64_bit8 -x64_bit9 -x64_bit10 -x64_bit11 -x64_bit12 -x64_bit13 -x64_bit14 -x64_bit15 -x64_bit16 x66_bit0 -x66_bit1 x66_bit2 -x66_bit3 -x66_bit4 -x66_bit5 -x66_bit6 -x66_bit7 -x66_bit8 -x66_bit9 -x66_bit10 -x66_bit11 -x66_bit12 -x66_bit13 -x66_bit14 -x66_bit15 -x66_bit16 -x68_bit0 -x68_bit1 -x68_bit2 -x68_bit3 -x68_bit4 -x68_bit5 -x68_bit6 -x68_bit7 -x68_bit8 -x68_bit9 -x68_bit10 -x68_bit11 -x68_bit12 -x68_bit13 -x68_bit14 -x68_bit15 -x68_bit16 -x70_bit0 -x70_bit1 -x70_bit2 -x70_bit3 -x70_bit4 -x70_bit5 -x70_bit6 -x70_bit7 -x70_bit8 -x70_bit9 -x70_bit10 -x70_bit11 -x70_bit12 -x70_bit13 -x70_bit14 -x70_bit15 -x70_bit16 -x72_bit0 -x72_bit1 -x72_bit2 -x72_bit3 -x72_bit4 -x72_bit5 -x72_bit6 -x72_bit7 -x72_bit8 -x72_bit9 -x72_bit10 -x72_bit11 -x72_bit12 -x72_bit13 -x72_bit14 -x72_bit15 -x72_bit16 -x74_bit0 -x74_bit1 -x74_bit2 -x74_bit3 -x74_bit4 -x74_bit5 -x74_bit6 -x74_bit7 -x74_bit8 -x74_bit9 -x74_bit10 -x74_bit11 -x74_bit12 -x74_bit13 -x74_bit14 -x74_bit15 -x74_bit16 -x76_bit0 -x76_bit1 -x76_bit2 -x76_bit3 -x76_bit4 -x76_bit5 -x76_bit6 -x76_bit7 -x76_bit8 -x76_bit9 -x76_bit10 -x76_bit11 -x76_bit12 -x76_bit13 -x76_bit14 -x76_bit15 -x76_bit16 -x78_bit0 -x78_bit1 -x78_bit2 -x78_bit3 -x78_bit4 -x78_bit5 -x78_bit6 -x78_bit7 -x78_bit8 -x78_bit9 -x78_bit10 -x78_bit11 -x78_bit12 -x78_bit13 -x78_bit14 -x78_bit15 -x78_bit16 -x80_bit0 -x80_bit1 -x80_bit2 -x80_bit3 -x80_bit4 -x80_bit5 -x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 -x80_bit10 -x80_bit11 -x80_bit12 -x80_bit13 -x80_bit14 -x80_bit15 -x80_bit16 -x82_bit0 -x82_bit1 -x82_bit2 -x82_bit3 -x82_bit4 -x82_bit5 -x82_bit6 -x82_bit7 -x82_bit8 -x82_bit9 -x82_bit10 -x82_bit11 -x82_bit12 -x82_bit13 -x82_bit14 -x82_bit15 -x82_bit16 -x84_bit0 -x84_bit1 -x84_bit2 -x84_bit3 -x84_bit4 -x84_bit5 -x84_bit6 -x84_bit7 -x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 -x84_bit13 -x84_bit14 -x84_bit15 -x84_bit16 -x86_bit0 -x86_bit1 -x86_bit2 -x86_bit3 -x86_bit4 -x86_bit5 -x86_bit6 -x86_bit7 -x86_bit8 -x86_bit9 -x86_bit10 -x86_bit11 -x86_bit12 -x86_bit13 -x86_bit14 -x86_bit15 -x86_bit16 x88_bit0 -x88_bit1 -x88_bit2 -x88_bit3 -x88_bit4 -x88_bit5 -x88_bit6 -x88_bit7 -x88_bit8 -x88_bit9 -x88_bit10 -x88_bit11 -x88_bit12 -x88_bit13 -x88_bit14 -x88_bit15 -x88_bit16 -x90_bit0 -x90_bit1 -x90_bit2 -x90_bit3 -x90_bit4 -x90_bit5 -x90_bit6 -x90_bit7 -x90_bit8 -x90_bit9 -x90_bit10 -x90_bit11 -x90_bit12 -x90_bit13 -x90_bit14 -x90_bit15 -x90_bit16 -x92_bit0 x92_bit1 -x92_bit2 -x92_bit3 -x92_bit4 -x92_bit5 -x92_bit6 -x92_bit7 -x92_bit8 -x92_bit9 -x92_bit10 -x92_bit11 -x92_bit12 -x92_bit13 -x92_bit14 -x92_bit15 -x92_bit16 -x94_bit0 -x94_bit1 -x94_bit2 -x94_bit3 -x94_bit4 -x94_bit5 -x94_bit6 -x94_bit7 -x94_bit8 -x94_bit9 -x94_bit10 -x94_bit11 -x94_bit12 -x94_bit13 -x94_bit14 -x94_bit15 -x94_bit16 -x96_bit0 -x96_bit1 -x96_bit2 -x96_bit3 -x96_bit4 -x96_bit5 -x96_bit6 -x96_bit7 -x96_bit8 -x96_bit9 -x96_bit10 -x96_bit11 -x96_bit12 -x96_bit13 -x96_bit14 -x96_bit15 -x96_bit16 -x98_bit0 -x98_bit1 -x98_bit2 -x98_bit3 -x98_bit4 -x98_bit5 -x98_bit6 -x98_bit7 -x98_bit8 -x98_bit9 -x98_bit10 -x98_bit11 -x98_bit12 -x98_bit13 -x98_bit14 -x98_bit15 -x98_bit16 -x100_bit0 -x100_bit1 -x100_bit2 -x100_bit3 -x100_bit4 -x100_bit5 -x100_bit6 -x100_bit7 -x100_bit8 -x100_bit9 -x100_bit10 -x100_bit11 -x100_bit12 -x100_bit13 -x100_bit14 -x100_bit15 -x100_bit16 -x1_bit0 -x2_bit0 x3_bit0 -x4_bit0 -x5_bit0 -x6_bit0 -x7_bit0 -x8_bit0 -x9_bit0 -x10_bit0 -x11_bit0 -x12_bit0 -x13_bit0 -x14_bit0 -x15_bit0 -x16_bit0 -x17_bit0 -x18_bit0 -x19_bit0 -x20_bit0 x21_bit0 x22_bit0 -x23_bit0 -x24_bit0 x25_bit0 x26_bit0 -x27_bit0 -x28_bit0 x29_bit0 -x30_bit0 x31_bit0 x32_bit0 -x33_bit0 -x34_bit0 x35_bit0 x36_bit0 -x37_bit0 x38_bit0 x39_bit0 -x40_bit0 x41_bit0 -x42_bit0 x43_bit0 -x44_bit0 -x45_bit0 x46_bit0 -x47_bit0 -x48_bit0 -x49_bit0 -x50_bit0 x51_bit0 x53_bit0 x55_bit0 x57_bit0 x59_bit0 -x61_bit0 -x63_bit0 x65_bit0 -x67_bit0 -x69_bit0 -x71_bit0 -x73_bit0 -x75_bit0 -x77_bit0 -x79_bit0 -x81_bit0 -x83_bit0 -x85_bit0 x87_bit0 -x89_bit0 x91_bit0 -x93_bit0 -x95_bit0 -x97_bit0 -x99_bit0 -x109_bit_7 -x109_bit_6 -x109_bit_5 -x109_bit_4 -x109_bit_3 -x109_bit_2 -x109_bit_1 -x109_bit0 -x109_bit1 -x109_bit2 -x109_bit3 -x109_bit4 -x109_bit5 -x109_bit6 -x109_bit7 -x109_bit8 -x109_bit9 -x109_bit10 -x109_bit11 -x109_bit12 -x124_bit_7 -x124_bit_6 -x124_bit_5 -x124_bit_4 -x124_bit_3 -x124_bit_2 -x124_bit_1 -x124_bit0 -x124_bit1 -x124_bit2 -x124_bit3 -x124_bit4 -x124_bit5 -x124_bit6 -x124_bit7 -x124_bit8 -x124_bit9 -x124_bit10 -x124_bit11 -x124_bit12 -x110_bit_7 -x110_bit_6 -x110_bit_5 -x110_bit_4 -x110_bit_3 -x110_bit_2 -x110_bit_1 -x110_bit0 -x110_bit1 -x110_bit2 -x110_bit3 -x110_bit4 -x110_bit5 -x110_bit6 -x110_bit7 -x110_bit8 -x110_bit9 -x110_bit10 -x110_bit11 -x110_bit12 -x125_bit_7 -x125_bit_6 -x125_bit_5 -x125_bit_4 -x125_bit_3 -x125_bit_2 -x125_bit_1 -x125_bit0 -x125_bit1 -x125_bit2 -x125_bit3 -x125_bit4 -x125_bit5 -x125_bit6 -x125_bit7 -x125_bit8 -x125_bit9 -x125_bit10 -x125_bit11 -x125_bit12 -x111_bit_7 -x111_bit_6 -x111_bit_5 -x111_bit_4 -x111_bit_3 -x111_bit_2 -x111_bit_1 -x111_bit0 -x111_bit1 -x111_bit2 -x111_bit3 -x111_bit4 -x111_bit5 -x111_bit6 -x111_bit7 -x111_bit8 -x111_bit9 -x111_bit10 -x111_bit11 -x111_bit12 -x112_bit_7 -x112_bit_6 -x112_bit_5 -x112_bit_4 -x112_bit_3 -x112_bit_2 -x112_bit_1 -x112_bit0 -x112_bit1 -x112_bit2 -x112_bit3 -x112_bit4 -x112_bit5 -x112_bit6 -x112_bit7 -x112_bit8 -x112_bit9 -x112_bit10 -x112_bit11 -x112_bit12 -x113_bit_7 -x113_bit_6 -x113_bit_5 -x113_bit_4 -x113_bit_3 -x113_bit_2 -x113_bit_1 -x113_bit0 -x113_bit1 -x113_bit2 -x113_bit3 -x113_bit4 -x113_bit5 -x113_bit6 -x113_bit7 -x113_bit8 -x113_bit9 -x113_bit10 -x113_bit11 -x113_bit12 -x114_bit_7 -x114_bit_6 -x114_bit_5 -x114_bit_4 -x114_bit_3 -x114_bit_2 -x114_bit_1 -x114_bit0 -x114_bit1 -x114_bit2 -x114_bit3 -x114_bit4 -x114_bit5 -x114_bit6 -x114_bit7 -x114_bit8 -x114_bit9 -x114_bit10 -x114_bit11 -x114_bit12 -x115_bit_7 -x115_bit_6 -x115_bit_5 -x115_bit_4 -x115_bit_3 -x115_bit_2 -x115_bit_1 -x115_bit0 -x115_bit1 -x115_bit2 -x115_bit3 -x115_bit4 -x115_bit5 -x115_bit6 -x115_bit7 -x115_bit8 -x115_bit9 -x115_bit10 -x115_bit11 -x115_bit12 -x116_bit_7 -x116_bit_6 -x116_bit_5 -x116_bit_4 -x116_bit_3 -x116_bit_2 -x116_bit_1 -x116_bit0 -x116_bit1 -x116_bit2 -x116_bit3 -x116_bit4 -x116_bit5 -x116_bit6 -x116_bit7 -x116_bit8 -x116_bit9 -x116_bit10 -x116_bit11 -x116_bit12 -x117_bit_7 -x117_bit_6 -x117_bit_5 -x117_bit_4 -x117_bit_3 -x117_bit_2 -x117_bit_1 -x117_bit0 -x117_bit1 -x117_bit2 -x117_bit3 -x117_bit4 -x117_bit5 -x117_bit6 -x117_bit7 -x117_bit8 -x117_bit9 -x117_bit10 -x117_bit11 -x117_bit12 -x118_bit_7 -x118_bit_6 -x118_bit_5 -x118_bit_4 -x118_bit_3 -x118_bit_2 -x118_bit_1 -x118_bit0 -x118_bit1 -x118_bit2 -x118_bit3 -x118_bit4 -x118_bit5 -x118_bit6 -x118_bit7 -x118_bit8 -x118_bit9 -x118_bit10 -x118_bit11 -x118_bit12 -x119_bit_7 -x119_bit_6 -x119_bit_5 -x119_bit_4 -x119_bit_3 -x119_bit_2 -x119_bit_1 -x119_bit0 -x119_bit1 -x119_bit2 -x119_bit3 -x119_bit4 -x119_bit5 -x119_bit6 -x119_bit7 -x119_bit8 -x119_bit9 -x119_bit10 -x119_bit11 -x119_bit12 -x120_bit_7 -x120_bit_6 -x120_bit_5 -x120_bit_4 -x120_bit_3 -x120_bit_2 -x120_bit_1 -x120_bit0 -x120_bit1 -x120_bit2 -x120_bit3 -x120_bit4 -x120_bit5 -x120_bit6 -x120_bit7 -x120_bit8 -x120_bit9 -x120_bit10 -x120_bit11 -x120_bit12 -x121_bit_7 -x121_bit_6 -x121_bit_5 -x121_bit_4 -x121_bit_3 -x121_bit_2 -x121_bit_1 -x121_bit0 -x121_bit1 -x121_bit2 -x121_bit3 -x121_bit4 -x121_bit5 -x121_bit6 -x121_bit7 -x121_bit8 -x121_bit9 -x121_bit10 -x121_bit11 -x121_bit12 -x122_bit_7 -x122_bit_6 -x122_bit_5 -x122_bit_4 -x122_bit_3 -x122_bit_2 -x122_bit_1 -x122_bit0 -x122_bit1 -x122_bit2 -x122_bit3 -x122_bit4 -x122_bit5 -x122_bit6 -x122_bit7 -x122_bit8 -x122_bit9 -x122_bit10 -x122_bit11 -x122_bit12 -x123_bit_7 -x123_bit_6 -x123_bit_5 -x123_bit_4 -x123_bit_3 -x123_bit_2 -x123_bit_1 -x123_bit0 -x123_bit1 -x123_bit2 -x123_bit3 -x123_bit4 -x123_bit5 -x123_bit6 -x123_bit7 -x123_bit8 -x123_bit9 -x123_bit10 -x123_bit11 -x123_bit12 -x127_bit_7 -x127_bit_6 -x127_bit_5 -x127_bit_4 -x127_bit_3 -x127_bit_2 -x127_bit_1 -x127_bit0 -x127_bit1 -x127_bit2 -x127_bit3 -x127_bit4 -x127_bit5 -x127_bit6 -x127_bit7 -x127_bit8 -x127_bit9 -x127_bit10 -x127_bit11 -x127_bit12 -x126_bit_7 -x126_bit_6 -x126_bit_5 -x126_bit_4 -x126_bit_3 -x126_bit_2 -x126_bit_1 -x126_bit0 -x126_bit1 -x126_bit2 -x126_bit3 -x126_bit4 -x126_bit5 -x126_bit6 -x126_bit7 -x126_bit8 -x126_bit9 -x126_bit10 -x126_bit11 -x126_bit12 -x128_bit_7 -x128_bit_6 -x128_bit_5 -x128_bit_4 -x128_bit_3 -x128_bit_2 -x128_bit_1 -x128_bit0 -x128_bit1 -x128_bit2 -x128_bit3 -x128_bit4 -x128_bit5 -x128_bit6 -x128_bit7 -x128_bit8 -x128_bit9 -x128_bit10 -x128_bit11 -x128_bit12 -x101_bit_7 -x101_bit_6 -x101_bit_5 -x101_bit_4 -x101_bit_3 -x101_bit_2 -x101_bit_1 x101_bit0 -x101_bit1 x101_bit2 -x101_bit3 -x101_bit4 -x101_bit5 -x101_bit6 -x101_bit7 -x101_bit8 -x101_bit9 -x101_bit10 -x101_bit11 -x101_bit12 -x106_bit_7 -x106_bit_6 -x106_bit_5 -x106_bit_4 -x106_bit_3 -x106_bit_2 -x106_bit_1 -x106_bit0 -x106_bit1 -x106_bit2 -x106_bit3 -x106_bit4 -x106_bit5 -x106_bit6 -x106_bit7 -x106_bit8 -x106_bit9 -x106_bit10 -x106_bit11 -x106_bit12 -x102_bit_7 -x102_bit_6 -x102_bit_5 x102_bit_4 x102_bit_3 -x102_bit_2 -x102_bit_1 x102_bit0 -x102_bit1 -x102_bit2 -x102_bit3 -x102_bit4 -x102_bit5 -x102_bit6 -x102_bit7 -x102_bit8 -x102_bit9 -x102_bit10 -x102_bit11 -x102_bit12 -x107_bit_7 -x107_bit_6 -x107_bit_5 -x107_bit_4 -x107_bit_3 -x107_bit_2 -x107_bit_1 -x107_bit0 -x107_bit1 -x107_bit2 -x107_bit3 -x107_bit4 -x107_bit5 -x107_bit6 -x107_bit7 -x107_bit8 -x107_bit9 -x107_bit10 -x107_bit11 -x107_bit12 -x103_bit_7 -x103_bit_6 -x103_bit_5 -x103_bit_4 -x103_bit_3 -x103_bit_2 -x103_bit_1 -x103_bit0 -x103_bit1 -x103_bit2 -x103_bit3 -x103_bit4 -x103_bit5 -x103_bit6 -x103_bit7 -x103_bit8 -x103_bit9 -x103_bit10 -x103_bit11 -x103_bit12 -x108_bit_7 x108_bit_6 x108_bit_5 -x108_bit_4 x108_bit_3 x108_bit_2 x108_bit_1 -x108_bit0 -x108_bit1 x108_bit2 -x108_bit3 -x108_bit4 -x108_bit5 -x108_bit6 -x108_bit7 -x108_bit8 -x108_bit9 -x108_bit10 -x108_bit11 -x108_bit12 x104_bit_7 x104_bit_6 x104_bit_5 x104_bit_4 x104_bit_3 x104_bit_2 -x104_bit_1 -x104_bit0 x104_bit1 -x104_bit2 -x104_bit3 -x104_bit4 -x104_bit5 -x104_bit6 -x104_bit7 -x104_bit8 -x104_bit9 -x104_bit10 -x104_bit11 -x104_bit12 x105_bit_7 x105_bit_6 x105_bit_5 x105_bit_4 x105_bit_3 -x105_bit_2 -x105_bit_1 -x105_bit0 -x105_bit1 -x105_bit2 -x105_bit3 -x105_bit4 -x105_bit5 -x105_bit6 -x105_bit7 -x105_bit8 -x105_bit9 -x105_bit10 -x105_bit11 -x105_bit12
c _______________________________________________________________________________
c 
c restarts              : 36
c conflicts             : 49035          (352 /sec)
c decisions             : 149074         (1070 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 139.342 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.91 2/54 29161
Raw data (stat): 29161 (runsolver) R 29160 1586 1585 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855018712 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+139.564 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 29165
Raw data (stat): 29161 (minisat+_script) S 29160 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855018712 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 139.563
CPU time (s): 139.56
CPU user time (s): 139.356
CPU system time (s): 0.203968
CPU usage (%): 99.9975
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-41
#### END VERIFIER DATA ####