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-vpm2.opb
MD5SUM	8c44064d4224b1d41c28f152218dd39f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	98
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	5
Number of bits for the biggest coefficient in the objective function	3
Sum of the numbers in the objective function	504
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	615983
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05084
Number of variables	2124
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	64
Trace number 18382

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 14:39:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18134 boxname=wulflinc1 idbench=1395 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8c44064d4224b1d41c28f152218dd39f  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-vpm2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-vpm2.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-vpm2.opb
IDLAUNCH: 18134
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        748232 kB
Buffers:          5236 kB
Cached:         256156 kB
SwapCached:          0 kB
Active:          49904 kB
Inactive:       214660 kB
HighTotal:      131008 kB
HighFree:        21420 kB
LowTotal:       903652 kB
LowFree:        726812 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16132 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:59:56 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 18134 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> BDD-cost:10530
c ---[ 272]---> BDD-cost: 3166
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:    7
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:    7
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    6
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    6
c ---[ 236]---> BDD-cost: 2842
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    6
c ---[ 229]---> BDD-cost:    7
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    6
c ---[ 224]---> BDD-cost: 7167
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    7
c ---[ 212]---> BDD-cost: 4105
c ---[ 211]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    6
c ---[ 164]---> BDD-cost: 3441
c ---[ 163]---> BDD-cost:    6
c ---[ 162]---> BDD-cost:    6
c ---[ 161]---> BDD-cost:    6
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    7
c ---[ 158]---> BDD-cost:    6
c ---[ 157]---> BDD-cost:    6
c ---[ 156]---> BDD-cost:    6
c ---[ 155]---> BDD-cost:    6
c ---[ 154]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:10530
c ---[ 150]---> BDD-cost: 8215
c ---[ 149]---> BDD-cost:    7
c ---[ 148]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    5
c ---[ 146]---> BDD-cost:    5
c ---[ 145]---> BDD-cost:    5
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:    7
c ---[ 142]---> BDD-cost:    5
c ---[ 141]---> BDD-cost:    5
c ---[ 140]---> BDD-cost:    5
c ---[ 137]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    7
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    6
c ---[ 132]---> BDD-cost:    6
c ---[ 131]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:    7
c ---[ 128]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:    6
c ---[ 123]---> BDD-cost:    6
c ---[ 121]---> BDD-cost:    7
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    6
c ---[ 118]---> BDD-cost:    6
c ---[ 117]---> BDD-cost:    6
c ---[ 114]---> BDD-cost: 3369
c ---[ 113]---> BDD-cost:    7
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    5
c ---[ 110]---> BDD-cost:    5
c ---[ 109]---> BDD-cost:    5
c ---[ 107]---> BDD-cost: 4733
c ---[ 105]---> BDD-cost: 4964
c ---[ 103]---> BDD-cost: 7397
c ---[ 101]---> BDD-cost: 3944
c ---[  99]---> BDD-cost: 3944
c ---[  97]---> BDD-cost: 3944
c ---[  95]---> BDD-cost: 7522
c ---[  93]---> BDD-cost: 3944
c ---[  91]---> BDD-cost: 3997
c ---[  89]---> BDD-cost: 9563
c ---[  87]---> BDD-cost: 4987
c ---[  85]---> BDD-cost: 4987
c ---[  83]---> BDD-cost: 4987
c ---[  81]---> BDD-cost: 5216
c ---[  73]---> BDD-cost: 7522
c ---[  69]---> BDD-cost: 3154
c ---[  66]---> BDD-cost:  136
c ---[  65]---> BDD-cost:  283
c ---[  64]---> BDD-cost:  282
c ---[  63]---> BDD-cost:  470
c ---[  62]---> BDD-cost:  579
c ---[  61]---> BDD-cost:  572
c ---[  60]---> BDD-cost:  182
c ---[  58]---> BDD-cost:10993
c ---[  57]---> BDD-cost:  387
c ---[  56]---> BDD-cost:  386
c ---[  55]---> BDD-cost:  647
c ---[  54]---> BDD-cost:  805
c ---[  53]---> BDD-cost:  804
c ---[  52]---> BDD-cost:  200
c ---[  51]---> BDD-cost:  446
c ---[  50]---> BDD-cost:  440
c ---[  49]---> BDD-cost:  784
c ---[  48]---> BDD-cost:  985
c ---[  46]---> BDD-cost: 2194
c ---[  45]---> BDD-cost:  982
c ---[  44]---> BDD-cost:   87
c ---[  43]---> BDD-cost:  178
c ---[  42]---> BDD-cost:  174
c ---[  41]---> BDD-cost:  291
c ---[  40]---> BDD-cost:  374
c ---[  39]---> BDD-cost:  369
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  34]---> BDD-cost: 4013
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    7
c ---[  26]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> BDD-cost: 4263
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> BDD-cost: 4263
c ---[   9]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    7
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    7
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  457558  1265621 |  152519       0        0     nan |  0.000 % |
c |       101 |  457558  1265621 |  167770     101     1035    10.2 |  0.549 % |
c |       251 |  457452  1265319 |  184547     235     4169    17.7 |  0.565 % |
c |       478 |  457376  1265101 |  203002     455     9845    21.6 |  0.575 % |
c |       816 |  457350  1265024 |  223303     791    16444    20.8 |  0.579 % |
c |      1322 |  457266  1264793 |  245633    1291    30889    23.9 |  0.590 % |
c |      2081 |  457266  1264793 |  270196    2050    58303    28.4 |  0.590 % |
c |      3220 |  457199  1264612 |  297216    3182    98499    31.0 |  0.601 % |
c |      4928 |  457156  1264487 |  326938    4881   149564    30.6 |  0.610 % |
c |      7491 |  457124  1264394 |  359631    7439   229291    30.8 |  0.616 % |
c |     11335 |  457018  1264094 |  395595   11270   418115    37.1 |  0.637 % |
c |     17101 |  457018  1264094 |  435154   17036   647974    38.0 |  0.637 % |
c |     25750 |  456973  1263964 |  478669   25680   908094    35.4 |  0.647 % |
c |     38724 |  456889  1263725 |  526536   38645  1637252    42.4 |  0.660 % |
c ==============================================================================
c [1mFound solution: 143[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6414     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39880 |  470257  1294935 |  156752   39800  1680425    42.2 |  0.660 % |
c |     39980 |  470215  1294814 |  172427   39895  1684276    42.2 |  0.650 % |
c |     40130 |  470161  1294686 |  189669   40041  1687653    42.1 |  0.655 % |
c |     40356 |  470161  1294686 |  208636   40267  1697260    42.2 |  0.655 % |
c |     40693 |  470151  1294658 |  229500   40603  1709934    42.1 |  0.656 % |
c |     41199 |  470105  1294549 |  252450   41107  1727320    42.0 |  0.661 % |
c |     41958 |  470105  1294549 |  277695   41866  1752549    41.9 |  0.661 % |
c |     43099 |  470089  1294503 |  305465   43003  1785863    41.5 |  0.665 % |
c |     44809 |  470089  1294503 |  336011   44713  1826588    40.9 |  0.665 % |
c |     47371 |  470077  1294469 |  369613   47274  1913086    40.5 |  0.667 % |
c |     51215 |  470054  1294416 |  406574   51117  2018145    39.5 |  0.669 % |
c |     56981 |  470054  1294416 |  447231   56883  2185308    38.4 |  0.669 % |
c |     65630 |  470054  1294416 |  491954   65532  2525905    38.5 |  0.669 % |
c ==============================================================================
c [1mFound solution: 115[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75481 |  470093  1294505 |  156697   75381  3328804    44.2 |  0.669 % |
c |     75582 |  470082  1294473 |  172366   75481  3337237    44.2 |  0.674 % |
c |     75733 |  470082  1294473 |  189603   75632  3339021    44.1 |  0.674 % |
c |     75959 |  470082  1294473 |  208563   75858  3340765    44.0 |  0.674 % |
c |     76297 |  470082  1294473 |  229420   76196  3351703    44.0 |  0.674 % |
c |     76803 |  470082  1294473 |  252362   76702  3369335    43.9 |  0.674 % |
c |     77563 |  470082  1294473 |  277598   77462  3460024    44.7 |  0.674 % |
c |     78703 |  469990  1294272 |  305358   78598  3477722    44.2 |  0.691 % |
c |     80411 |  469793  1293808 |  335893   80221  3539878    44.1 |  0.722 % |
c |     82975 |  469793  1293808 |  369483   82785  3683832    44.5 |  0.722 % |
c |     86819 |  469793  1293808 |  406431   86629  3884323    44.8 |  0.722 % |
c |     92586 |  469654  1293495 |  447074   91727  4139810    45.1 |  0.748 % |
c |    101236 |  469647  1293475 |  491782  100376  4505463    44.9 |  0.749 % |
c ==============================================================================
c [1mFound solution: 113[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 4837     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103199 |  475285  1306698 |  158428  102339  4608803    45.0 |  0.749 % |
c |    103299 |  475285  1306698 |  174270  102439  4611411    45.0 |  0.735 % |
c |    103452 |  475285  1306698 |  191697  102592  4615017    45.0 |  0.735 % |
c |    103677 |  475285  1306698 |  210867  102817  4623894    45.0 |  0.735 % |
c |    104014 |  475285  1306698 |  231954  103154  4637200    45.0 |  0.735 % |
c |    104522 |  475285  1306698 |  255149  103662  4660564    45.0 |  0.735 % |
c |    105281 |  475285  1306698 |  280664  104421  4691283    44.9 |  0.735 % |
c |    106420 |  475285  1306698 |  308731  105560  4725387    44.8 |  0.735 % |
c |    108130 |  475285  1306698 |  339604  107270  4777409    44.5 |  0.735 % |
c |    110698 |  475285  1306698 |  373564  109838  4908084    44.7 |  0.735 % |
c ==============================================================================
c [1mFound solution: 108[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110998 |  480058  1317841 |  160019  110138  4919258    44.7 |  0.735 % |
c |    111098 |  480058  1317841 |  176020  110238  4926262    44.7 |  0.736 % |
c |    111249 |  480058  1317841 |  193622  110389  4929850    44.7 |  0.736 % |
c |    111478 |  480058  1317841 |  212985  110618  4936111    44.6 |  0.736 % |
c |    111815 |  480058  1317841 |  234283  110955  4949127    44.6 |  0.736 % |
c |    112322 |  480058  1317841 |  257712  111462  4973648    44.6 |  0.736 % |
c |    113081 |  480058  1317841 |  283483  112221  5002783    44.6 |  0.736 % |
c |    114222 |  480058  1317841 |  311831  113362  5067501    44.7 |  0.736 % |
c ==============================================================================
c [1mFound solution: 106[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    114844 |  480065  1317941 |  160021  113984  5099651    44.7 |  0.736 % |
c |    114946 |  480065  1317941 |  176023  114086  5101268    44.7 |  0.736 % |
c |    115096 |  480065  1317941 |  193625  114236  5102171    44.7 |  0.736 % |
c |    115321 |  480065  1317941 |  212987  114461  5106340    44.6 |  0.736 % |
c |    115659 |  480065  1317941 |  234286  114799  5113368    44.5 |  0.736 % |
c |    116165 |  480052  1317913 |  257715  115301  5118882    44.4 |  0.739 % |
c |    116926 |  480052  1317913 |  283486  116062  5143563    44.3 |  0.739 % |
c |    118065 |  480052  1317913 |  311835  117201  5181715    44.2 |  0.739 % |
c |    119774 |  480052  1317913 |  343019  118910  5243306    44.1 |  0.739 % |
c |    122336 |  480052  1317913 |  377321  121472  5356913    44.1 |  0.739 % |
c |    126181 |  480023  1317831 |  415053  125316  5489286    43.8 |  0.741 % |
c |    131948 |  480023  1317831 |  456558  131083  5739671    43.8 |  0.741 % |
c ==============================================================================
c [1mFound solution: 105[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133769 |  480027  1317843 |  160009  132904  5920861    44.5 |  0.741 % |
c |    133870 |  480027  1317843 |  176009  133005  5921948    44.5 |  0.741 % |
c |    134020 |  480027  1317843 |  193610  133155  5923660    44.5 |  0.741 % |
c |    134246 |  480027  1317843 |  212971  133381  5925334    44.4 |  0.741 % |
c |    134584 |  479959  1317701 |  234269  133696  5933761    44.4 |  0.758 % |
c |    135091 |  479959  1317701 |  257696  134203  5951920    44.4 |  0.758 % |
c |    135854 |  479959  1317701 |  283465  134966  5986093    44.4 |  0.758 % |
c |    136996 |  479959  1317701 |  311812  136108  6040429    44.4 |  0.758 % |
c |    138704 |  479950  1317683 |  342993  137815  6122223    44.4 |  0.760 % |
c |    141267 |  479950  1317683 |  377292  140378  6261082    44.6 |  0.760 % |
c ==============================================================================
c [1mFound solution: 104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    142561 |  479914  1317612 |  159971  141660  6351995    44.8 |  0.760 % |
c |    142662 |  479914  1317612 |  175968  141761  6353303    44.8 |  0.771 % |
c |    142812 |  479914  1317612 |  193564  141911  6357679    44.8 |  0.771 % |
c |    143037 |  479914  1317612 |  212921  142136  6363544    44.8 |  0.771 % |
c |    143374 |  479914  1317612 |  234213  142473  6375783    44.8 |  0.771 % |
c |    143882 |  479914  1317612 |  257634  142981  6399199    44.8 |  0.771 % |
c |    144644 |  479914  1317612 |  283398  143743  6434810    44.8 |  0.771 % |
c ==============================================================================
c [1mFound solution: 92[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    145331 |  479945  1317687 |  159981  144430  6464774    44.8 |  0.771 % |
c |    145431 |  479945  1317687 |  175979  144530  6467264    44.7 |  0.772 % |
c |    145581 |  479945  1317687 |  193577  144680  6469971    44.7 |  0.772 % |
c |    145806 |  479945  1317687 |  212934  144905  6482685    44.7 |  0.772 % |
c |    146143 |  479945  1317687 |  234228  145242  6498336    44.7 |  0.772 % |
c |    146649 |  479945  1317687 |  257651  145748  6522811    44.8 |  0.772 % |
c |    147408 |  479945  1317687 |  283416  146507  6559756    44.8 |  0.772 % |
c |    148549 |  479945  1317687 |  311757  147648  6640764    45.0 |  0.772 % |
c |    150258 |  479945  1317687 |  342933  149357  6777073    45.4 |  0.772 % |
c |    152820 |  479945  1317687 |  377226  151919  6886476    45.3 |  0.772 % |
c |    156666 |  479945  1317687 |  414949  155765  7355928    47.2 |  0.772 % |
c ==============================================================================
c [1mFound solution: 91[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    158382 |  479952  1317706 |  159984  157481  7422946    47.1 |  0.772 % |
c |    158484 |  479952  1317706 |  175982  157583  7425964    47.1 |  0.772 % |
c |    158635 |  479952  1317706 |  193580  157734  7430276    47.1 |  0.772 % |
c |    158860 |  479952  1317706 |  212938  157959  7441004    47.1 |  0.772 % |
c |    159198 |  479952  1317706 |  234232  158297  7452593    47.1 |  0.772 % |
c |    159705 |  479952  1317706 |  257655  158804  7465972    47.0 |  0.772 % |
c |    160465 |  479952  1317706 |  283421  159564  7506171    47.0 |  0.772 % |
c |    161612 |  479944  1317684 |  311763  160710  7608850    47.3 |  0.773 % |
c |    163320 |  479944  1317684 |  342939  162418  7652982    47.1 |  0.773 % |
c |    165882 |  479944  1317684 |  377233  164980  7770131    47.1 |  0.773 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    168881 |  479949  1317695 |  159983  167979  8004153    47.6 |  0.773 % |
c |    168981 |  479949  1317695 |  175981   21530   828029    38.5 |  0.774 % |
c |    169131 |  479949  1317695 |  193579   21680   829301    38.3 |  0.774 % |
c |    169356 |  479949  1317695 |  212937   21905   831721    38.0 |  0.774 % |
c |    169695 |  479949  1317695 |  234231   22244   837360    37.6 |  0.774 % |
c |    170201 |  479849  1317477 |  257654   22746   861336    37.9 |  0.792 % |
c |    170960 |  479849  1317477 |  283419   23505   909830    38.7 |  0.792 % |
c |    172099 |  479849  1317477 |  311761   24644   983990    39.9 |  0.792 % |
c |    173808 |  479849  1317477 |  342937   26353  1075388    40.8 |  0.792 % |
c |    176372 |  479849  1317477 |  377231   28917  1158372    40.1 |  0.792 % |
c |    180216 |  479849  1317477 |  414954   32761  1550642    47.3 |  0.792 % |
c |    185983 |  479839  1317457 |  456450   38527  1919264    49.8 |  0.794 % |
c ==============================================================================
c [1mFound solution: 88[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    189621 |  479845  1317473 |  159948   42165  2160633    51.2 |  0.794 % |
c |    189723 |  479845  1317473 |  175942   42267  2161896    51.1 |  0.794 % |
c |    189874 |  479845  1317473 |  193537   42418  2164254    51.0 |  0.794 % |
c |    190100 |  479845  1317473 |  212890   42644  2168463    50.9 |  0.794 % |
c |    190437 |  479845  1317473 |  234179   42981  2182103    50.8 |  0.794 % |
c |    190944 |  479845  1317473 |  257597   43488  2196148    50.5 |  0.794 % |
c |    191703 |  479845  1317473 |  283357   44247  2210889    50.0 |  0.794 % |
c |    192843 |  479845  1317473 |  311693   45387  2283583    50.3 |  0.794 % |
c |    194551 |  479845  1317473 |  342862   47095  2351141    49.9 |  0.794 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x169_bit0 -x170_bit0 -x171_bit0 -x172_bit0 -x173_bit0 x174_bit0 -x175_bit0 -x176_bit0 -x177_bit0 -x178_bit0 -x179_bit0 -x180_bit0 x181_bit0 x182_bit0 x183_bit0 -x184_bit0 -x185_bit0 x186_bit0 -x187_bit0 -x188_bit0 x189_bit0 -x190_bit0 -x191_bit0 x192_bit0 -x193_bit0 -x194_bit0 -x195_bit0 x196_bit0 x197_bit0 -x198_bit0 -x199_bit0 x200_bit0 x201_bit0 -x202_bit0 -x203_bit0 -x204_bit0 -x205_bit0 -x206_bit0 x207_bit0 -x208_bit0 -x209_bit0 -x210_bit0 -x211_bit0 -x212_bit0 -x213_bit0 x214_bit0 -x215_bit0 -x216_bit0 -x217_bit0 -x218_bit0 -x219_bit0 x220_bit0 -x221_bit0 -x222_bit0 -x223_bit0 -x224_bit0 -x225_bit0 x226_bit0 x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 -x244_bit0 x245_bit0 x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 x252_bit0 -x253_bit0 -x254_bit0 -x255_bit0 -x256_bit0 x257_bit0 -x258_bit0 -x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 x268_bit0 -x269_bit0 x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 x280_bit0 x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 x287_bit0 -x288_bit0 x289_bit0 x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 -x294_bit0 x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 x314_bit0 x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x1_bit_7 -x1_bit_6 -x1_bit_5 -x1_bit_4 -x1_bit_3 -x1_bit_2 -x1_bit_1 -x1_bit0 -x2_bit_7 -x2_bit_6 -x2_bit_5 -x2_bit_4 -x2_bit_3 -x2_bit_2 -x2_bit_1 -x2_bit0 -x3_bit_7 -x3_bit_6 -x3_bit_5 -x3_bit_4 -x3_bit_3 -x3_bit_2 -x3_bit_1 -x3_bit0 -x4_bit_7 -x4_bit_6 -x4_bit_5 -x4_bit_4 -x4_bit_3 -x4_bit_2 -x4_bit_1 -x4_bit0 -x5_bit_7 -x5_bit_6 -x5_bit_5 -x5_bit_4 -x5_bit_3 -x5_bit_2 -x5_bit_1 -x5_bit0 x6_bit_7 -x6_bit_6 -x6_bit_5 x6_bit_4 -x6_bit_3 -x6_bit_2 -x6_bit_1 -x6_bit0 -x7_bit_7 -x7_bit_6 -x7_bit_5 -x7_bit_4 -x7_bit_3 -x7_bit_2 -x7_bit_1 -x7_bit0 -x8_bit_7 -x8_bit_6 -x8_bit_5 -x8_bit_4 -x8_bit_3 -x8_bit_2 -x8_bit_1 -x8_bit0 -x9_bit_7 -x9_bit_6 -x9_bit_5 -x9_bit_4 -x9_bit_3 -x9_bit_2 -x9_bit_1 -x9_bit0 -x10_bit_7 -x10_bit_6 -x10_bit_5 -x10_bit_4 -x10_bit_3 -x10_bit_2 -x10_bit_1 -x10_bit0 -x11_bit_7 -x11_bit_6 -x11_bit_5 -x11_bit_4 -x11_bit_3 -x11_bit_2 -x11_bit_1 -x11_bit0 -x12_bit_7 -x12_bit_6 -x12_bit_5 -x12_bit_4 -x12_bit_3 -x12_bit_2 -x12_bit_1 -x12_bit0 -x13_bit_7 x13_bit_6 -x13_bit_5 -x13_bit_4 x13_bit_3 x13_bit_2 x13_bit_1 -x13_bit0 -x14_bit_7 x14_bit_6 -x14_bit_5 -x14_bit_4 x14_bit_3 x14_bit_2 x14_bit_1 -x14_bit0 -x15_bit_7 x15_bit_6 x15_bit_5 -x15_bit_4 -x15_bit_3 x15_bit_2 -x15_bit_1 -x15_bit0 -x16_bit_7 -x16_bit_6 -x16_bit_5 -x16_bit_4 -x16_bit_3 -x16_bit_2 -x16_bit_1 -x16_bit0 -x17_bit_7 -x17_bit_6 -x17_bit_5 -x17_bit_4 -x17_bit_3 -x17_bit_2 -x17_bit_1 -x17_bit0 x18_bit_7 x18_bit_6 -x18_bit_5 -x18_bit_4 x18_bit_3 x18_bit_2 x18_bit_1 -x18_bit0 -x19_bit_7 -x19_bit_6 -x19_bit_5 -x19_bit_4 -x19_bit_3 -x19_bit_2 -x19_bit_1 -x19_bit0 -x20_bit_7 -x20_bit_6 -x20_bit_5 -x20_bit_4 -x20_bit_3 -x20_bit_2 -x20_bit_1 -x20_bit0 x21_bit_7 x21_bit_6 x21_bit_5 x21_bit_4 -x21_bit_3 x21_bit_2 x21_bit_1 -x21_bit0 -x22_bit_7 -x22_bit_6 -x22_bit_5 -x22_bit_4 -x22_bit_3 -x22_bit_2 -x22_bit_1 -x22_bit0 -x23_bit_7 -x23_bit_6 -x23_bit_5 -x23_bit_4 -x23_bit_3 -x23_bit_2 -x23_bit_1 -x23_bit0 x24_bit_7 x24_bit_6 x24_bit_5 x24_bit_4 -x24_bit_3 -x24_bit_2 -x24_bit_1 -x24_bit0 -x25_bit_7 -x25_bit_6 -x25_bit_5 -x25_bit_4 -x25_bit_3 -x25_bit_2 -x25_bit_1 -x25_bit0 -x26_bit_7 -x26_bit_6 -x26_bit_5 -x26_bit_4 -x26_bit_3 -x26_bit_2 -x26_bit_1 -x26_bit0 -x27_bit_7 -x27_bit_6 -x27_bit_5 -x27_bit_4 -x27_bit_3 -x27_bit_2 -x27_bit_1 -x27_bit0 x28_bit_7 x28_bit_6 x28_bit_5 x28_bit_4 -x28_bit_3 -x28_bit_2 -x28_bit_1 -x28_bit0 -x29_bit_7 -x29_bit_6 x29_bit_5 x29_bit_4 x29_bit_3 -x29_bit_2 x29_bit_1 -x29_bit0 -x30_bit_7 -x30_bit_6 -x30_bit_5 -x30_bit_4 -x30_bit_3 -x30_bit_2 -x30_bit_1 -x30_bit0 -x31_bit_7 -x31_bit_6 -x31_bit_5 -x31_bit_4 -x31_bit_3 -x31_bit_2 -x31_bit_1 -x31_bit0 -x32_bit_7 -x32_bit_6 x32_bit_5 -x32_bit_4 x32_bit_3 x32_bit_2 x32_bit_1 -x32_bit0 x33_bit_7 x33_bit_6 x33_bit_5 -x33_bit_4 x33_bit_3 x33_bit_2 x33_bit_1 -x33_bit0 -x34_bit_7 -x34_bit_6 -x34_bit_5 -x34_bit_4 -x34_bit_3 -x34_bit_2 -x34_bit_1 -x34_bit0 -x35_bit_7 -x35_bit_6 -x35_bit_5 -x35_bit_4 -x35_bit_3 -x35_bit_2 -x35_bit_1 -x35_bit0 -x36_bit_7 -x36_bit_6 -x36_bit_5 -x36_bit_4 -x36_bit_3 -x36_bit_2 -x36_bit_1 -x36_bit0 -x37_bit_7 -x37_bit_6 -x37_bit_5 -x37_bit_4 -x37_bit_3 -x37_bit_2 -x37_bit_1 -x37_bit0 -x38_bit_7 -x38_bit_6 -x38_bit_5 -x38_bit_4 -x38_bit_3 -x38_bit_2 -x38_bit_1 -x38_bit0 -x39_bit_7 -x39_bit_6 -x39_bit_5 -x39_bit_4 -x39_bit_3 -x39_bit_2 x39_bit_1 -x39_bit0 -x40_bit_7 -x40_bit_6 -x40_bit_5 -x40_bit_4 -x40_bit_3 -x40_bit_2 -x40_bit_1 -x40_bit0 -x41_bit_7 -x41_bit_6 -x41_bit_5 -x41_bit_4 -x41_bit_3 -x41_bit_2 -x41_bit_1 -x41_bit0 -x42_bit_7 -x42_bit_6 -x42_bit_5 -x42_bit_4 -x42_bit_3 -x42_bit_2 -x42_bit_1 -x42_bit0 -x43_bit_7 -x43_bit_6 -x43_bit_5 -x43_bit_4 -x43_bit_3 -x43_bit_2 -x43_bit_1 -x43_bit0 -x44_bit_7 -x44_bit_6 -x44_bit_5 -x44_bit_4 -x44_bit_3 -x44_bit_2 -x44_bit_1 -x44_bit0 -x45_bit_7 -x45_bit_6 -x45_bit_5 -x45_bit_4 -x45_bit_3 -x45_bit_2 -x45_bit_1 -x45_bit0 -x46_bit_7 -x46_bit_6 -x46_bit_5 -x46_bit_4 x46_bit_3 x46_bit_2 x46_bit_1 -x46_bit0 -x47_bit_7 -x47_bit_6 -x47_bit_5 -x47_bit_4 -x47_bit_3 -x47_bit_2 -x47_bit_1 -x47_bit0 -x48_bit_7 -x48_bit_6 -x48_bit_5 -x48_bit_4 -x48_bit_3 -x48_bit_2 -x48_bit_1 -x48_bit0 -x49_bit_7 -x49_bit_6 -x49_bit_5 -x49_bit_4 -x49_bit_3 -x49_bit_2 -x49_bit_1 -x49_bit0 -x50_bit_7 -x50_bit_6 -x50_bit_5 -x50_bit_4 -x50_bit_3 -x50_bit_2 -x50_bit_1 -x50_bit0 -x51_bit_7 -x51_bit_6 -x51_bit_5 -x51_bit_4 -x51_bit_3 -x51_bit_2 -x51_bit_1 -x51_bit0 x52_bit_7 -x52_bit_6 -x52_bit_5 -x52_bit_4 -x52_bit_3 -x52_bit_2 -x52_bit_1 -x52_bit0 -x53_bit_7 -x53_bit_6 -x53_bit_5 -x53_bit_4 -x53_bit_3 -x53_bit_2 -x53_bit_1 -x53_bit0 -x54_bit_7 -x54_bit_6 -x54_bit_5 -x54_bit_4 -x54_bit_3 -x54_bit_2 -x54_bit_1 -x54_bit0 -x55_bit_7 -x55_bit_6 -x55_bit_5 -x55_bit_4 -x55_bit_3 -x55_bit_2 -x55_bit_1 -x55_bit0 -x56_bit_7 -x56_bit_6 -x56_bit_5 -x56_bit_4 -x56_bit_3 -x56_bit_2 -x56_bit_1 -x56_bit0 -x57_bit_7 -x57_bit_6 -x57_bit_5 -x57_bit_4 -x57_bit_3 -x57_bit_2 -x57_bit_1 -x57_bit0 x58_bit_7 -x58_bit_6 -x58_bit_5 x58_bit_4 -x58_bit_3 -x58_bit_2 x58_bit_1 -x58_bit0 x59_bit_7 -x59_bit_6 -x59_bit_5 -x59_bit_4 -x59_bit_3 x59_bit_2 x59_bit_1 -x59_bit0 -x60_bit_7 -x60_bit_6 -x60_bit_5 -x60_bit_4 -x60_bit_3 -x60_bit_2 -x60_bit_1 -x60_bit0 -x61_bit_7 -x61_bit_6 -x61_bit_5 -x61_bit_4 -x61_bit_3 -x61_bit_2 -x61_bit_1 -x61_bit0 -x62_bit_7 -x62_bit_6 -x62_bit_5 -x62_bit_4 -x62_bit_3 -x62_bit_2 -x62_bit_1 -x62_bit0 -x63_bit_7 -x63_bit_6 -x63_bit_5 -x63_bit_4 -x63_bit_3 -x63_bit_2 -x63_bit_1 -x63_bit0 -x64_bit_7 -x64_bit_6 -x64_bit_5 -x64_bit_4 -x64_bit_3 -x64_bit_2 -x64_bit_1 -x64_bit0 -x65_bit_7 -x65_bit_6 -x65_bit_5 -x65_bit_4 -x65_bit_3 -x65_bit_2 -x65_bit_1 -x65_bit0 -x66_bit_7 -x66_bit_6 -x66_bit_5 -x66_bit_4 -x66_bit_3 -x66_bit_2 -x66_bit_1 -x66_bit0 -x67_bit_7 -x67_bit_6 -x67_bit_5 -x67_bit_4 -x67_bit_3 -x67_bit_2 -x67_bit_1 -x67_bit0 -x68_bit_7 -x68_bit_6 -x68_bit_5 -x68_bit_4 -x68_bit_3 -x68_bit_2 -x68_bit_1 -x68_bit0 -x69_bit_7 -x69_bit_6 -x69_bit_5 -x69_bit_4 -x69_bit_3 -x69_bit_2 -x69_bit_1 -x69_bit0 -x70_bit_7 -x70_bit_6 -x70_bit_5 -x70_bit_4 -x70_bit_3 -x70_bit_2 -x70_bit_1 -x70_bit0 x71_bit_7 -x71_bit_6 x71_bit_5 -x71_bit_4 x71_bit_3 -x71_bit_2 x71_bit_1 -x71_bit0 -x72_bit_7 -x72_bit_6 -x72_bit_5 -x72_bit_4 -x72_bit_3 -x72_bit_2 -x72_bit_1 -x72_bit0 -x73_bit_7 -x73_bit_6 -x73_bit_5 -x73_bit_4 -x73_bit_3 -x73_bit_2 -x73_bit_1 -x73_bit0 -x74_bit_7 -x74_bit_6 -x74_bit_5 -x74_bit_4 -x74_bit_3 -x74_bit_2 -x74_bit_1 -x74_bit0 -x75_bit_7 -x75_bit_6 -x75_bit_5 -x75_bit_4 -x75_bit_3 -x75_bit_2 -x75_bit_1 -x75_bit0 -x76_bit_7 -x76_bit_6 -x76_bit_5 -x76_bit_4 -x76_bit_3 -x76_bit_2 -x76_bit_1 -x76_bit0 -x77_bit_7 x77_bit_6 x77_bit_5 x77_bit_4 x77_bit_3 -x77_bit_2 -x77_bit_1 -x77_bit0 -x78_bit_7 x78_bit_6 x78_bit_5 x78_bit_4 -x78_bit_3 x78_bit_2 x78_bit_1 -x78_bit0 -x79_bit_7 -x79_bit_6 -x79_bit_5 -x79_bit_4 -x79_bit_3 -x79_bit_2 -x79_bit_1 -x79_bit0 -x80_bit_7 -x80_bit_6 -x80_bit_5 -x80_bit_4 -x80_bit_3 -x80_bit_2 -x80_bit_1 -x80_bit0 -x81_bit_7 -x81_bit_6 -x81_bit_5 -x81_bit_4 -x81_bit_3 -x81_bit_2 -x81_bit_1 -x81_bit0 -x82_bit_7 -x82_bit_6 -x82_bit_5 -x82_bit_4 -x82_bit_3 -x82_bit_2 -x82_bit_1 -x82_bit0 -x83_bit_7 -x83_bit_6 -x83_bit_5 -x83_bit_4 -x83_bit_3 -x83_bit_2 -x83_bit_1 -x83_bit0 x84_bit_7 x84_bit_6 x84_bit_5 x84_bit_4 -x84_bit_3 x84_bit_2 x84_bit_1 -x84_bit0 -x85_bit_7 -x85_bit_6 -x85_bit_5 -x85_bit_4 -x85_bit_3 -x85_bit_2 -x85_bit_1 -x85_bit0 -x86_bit_7 -x86_bit_6 -x86_bit_5 -x86_bit_4 -x86_bit_3 -x86_bit_2 -x86_bit_1 -x86_bit0 -x87_bit_7 -x87_bit_6 -x87_bit_5 -x87_bit_4 -x87_bit_3 -x87_bit_2 -x87_bit_1 -x87_bit0 -x88_bit_7 -x88_bit_6 -x88_bit_5 -x88_bit_4 -x88_bit_3 -x88_bit_2 -x88_bit_1 -x88_bit0 x89_bit_7 -x89_bit_6 x89_bit_5 x89_bit_4 x89_bit_3 -x89_bit_2 x89_bit_1 -x89_bit0 -x90_bit_7 -x90_bit_6 -x90_bit_5 -x90_bit_4 -x90_bit_3 -x90_bit_2 -x90_bit_1 -x90_bit0 -x91_bit_7 -x91_bit_6 -x91_bit_5 -x91_bit_4 -x91_bit_3 -x91_bit_2 -x91_bit_1 -x91_bit0 -x92_bit_7 -x92_bit_6 -x92_bit_5 -x92_bit_4 -x92_bit_3 -x92_bit_2 -x92_bit_1 -x92_bit0 -x93_bit_7 -x93_bit_6 -x93_bit_5 -x93_bit_4 -x93_bit_3 -x93_bit_2 -x93_bit_1 -x93_bit0 -x94_bit_7 -x94_bit_6 -x94_bit_5 -x94_bit_4 -x94_bit_3 -x94_bit_2 -x94_bit_1 -x94_bit0 -x95_bit_7 -x95_bit_6 -x95_bit_5 -x95_bit_4 -x95_bit_3 -x95_bit_2 -x95_bit_1 -x95_bit0 x96_bit_7 -x96_bit_6 x96_bit_5 x96_bit_4 -x96_bit_3 -x96_bit_2 x96_bit_1 -x96_bit0 -x97_bit_7 -x97_bit_6 -x97_bit_5 -x97_bit_4 -x97_bit_3 -x97_bit_2 -x97_bit_1 -x97_bit0 -x98_bit_7 -x98_bit_6 -x98_bit_5 -x98_bit_4 -x98_bit_3 -x98_bit_2 -x98_bit_1 -x98_bit0 -x99_bit_7 -x99_bit_6 -x99_bit_5 -x99_bit_4 -x99_bit_3 -x99_bit_2 -x99_bit_1 -x99_bit0 x100_bit_7 x100_bit_6 x100_bit_5 -x100_bit_4 -x100_bit_3 x100_bit_2 x100_bit_1 -x100_bit0 -x101_bit_7 -x101_bit_6 -x101_bit_5 -x101_bit_4 -x101_bit_3 -x101_bit_2 -x101_bit_1 -x101_bit0 -x102_bit_7 -x102_bit_6 -x102_bit_5 -x102_bit_4 -x102_bit_3 -x102_bit_2 -x102_bit_1 -x102_bit0 -x103_bit_7 -x103_bit_6 -x103_bit_5 -x103_bit_4 -x103_bit_3 -x103_bit_2 -x103_bit_1 -x103_bit0 -x104_bit_7 -x104_bit_6 -x104_bit_5 -x104_bit_4 -x104_bit_3 -x104_bit_2 -x104_bit_1 -x104_bit0 -x105_bit_7 -x105_bit_6 -x105_bit_5 -x105_bit_4 -x105_bit_3 -x105_bit_2 -x105_bit_1 -x105_bit0 -x106_bit_7 -x106_bit_6 -x106_bit_5 -x106_bit_4 -x106_bit_3 -x106_bit_2 -x106_bit_1 -x106_bit0 -x107_bit_7 x107_bit_6 -x107_bit_5 -x107_bit_4 x107_bit_3 -x107_bit_2 -x107_bit_1 -x107_bit0 -x108_bit_7 -x108_bit_6 -x108_bit_5 -x108_bit_4 -x108_bit_3 -x108_bit_2 -x108_bit_1 -x108_bit0 -x109_bit_7 -x109_bit_6 -x109_bit_5 -x109_bit_4 -x109_bit_3 -x109_bit_2 -x109_bit_1 -x109_bit0 -x110_bit_7 -x110_bit_6 -x110_bit_5 -x110_bit_4 -x110_bit_3 -x110_bit_2 -x110_bit_1 -x110_bit0 -x111_bit_7 -x111_bit_6 -x111_bit_5 -x111_bit_4 -x111_bit_3 -x111_bit_2 -x111_bit_1 -x111_bit0 x112_bit_7 x112_bit_6 x112_bit_5 x112_bit_4 -x112_bit_3 x112_bit_2 x112_bit_1 -x112_bit0 x113_bit_7 -x113_bit_6 -x113_bit_5 x113_bit_4 -x113_bit_3 -x113_bit_2 -x113_bit_1 -x113_bit0 -x114_bit_7 -x114_bit_6 -x114_bit_5 -x114_bit_4 -x114_bit_3 -x114_bit_2 -x114_bit_1 -x114_bit0 -x115_bit_7 -x115_bit_6 -x115_bit_5 -x115_bit_4 -x115_bit_3 -x115_bit_2 -x115_bit_1 -x115_bit0 -x116_bit_7 -x116_bit_6 -x116_bit_5 -x116_bit_4 -x116_bit_3 -x116_bit_2 -x116_bit_1 -x116_bit0 -x117_bit_7 -x117_bit_6 -x117_bit_5 -x117_bit_4 -x117_bit_3 -x117_bit_2 -x117_bit_1 -x117_bit0 -x118_bit_7 -x118_bit_6 -x118_bit_5 -x118_bit_4 -x118_bit_3 -x118_bit_2 -x118_bit_1 -x118_bit0 x119_bit_7 x119_bit_6 -x119_bit_5 x119_bit_4 -x119_bit_3 -x119_bit_2 -x119_bit_1 -x119_bit0 -x120_bit_7 -x120_bit_6 -x120_bit_5 -x120_bit_4 -x120_bit_3 -x120_bit_2 -x120_bit_1 -x120_bit0 x121_bit_7 -x121_bit_6 x121_bit_5 x121_bit_4 x121_bit_3 x121_bit_2 x121_bit_1 -x121_bit0 -x122_bit_7 -x122_bit_6 -x122_bit_5 -x122_bit_4 -x122_bit_3 -x122_bit_2 x122_bit_1 -x122_bit0 -x123_bit_7 -x123_bit_6 -x123_bit_5 -x123_bit_4 -x123_bit_3 -x123_bit_2 -x123_bit_1 -x123_bit0 -x124_bit_7 -x124_bit_6 -x124_bit_5 -x124_bit_4 -x124_bit_3 -x124_bit_2 -x124_bit_1 -x124_bit0 -x125_bit_7 -x125_bit_6 -x125_bit_5 -x125_bit_4 -x125_bit_3 -x125_bit_2 -x125_bit_1 -x125_bit0 -x126_bit_7 -x126_bit_6 -x126_bit_5 -x126_bit_4 -x126_bit_3 -x126_bit_2 -x126_bit_1 -x126_bit0 x127_bit_7 -x127_bit_6 x127_bit_5 -x127_bit_4 x127_bit_3 x127_bit_2 x127_bit_1 -x127_bit0 -x128_bit_7 -x128_bit_6 -x128_bit_5 -x128_bit_4 -x128_bit_3 -x128_bit_2 -x128_bit_1 -x128_bit0 -x129_bit_7 -x129_bit_6 -x129_bit_5 -x129_bit_4 -x129_bit_3 -x129_bit_2 -x129_bit_1 -x129_bit0 -x130_bit_7 -x130_bit_6 -x130_bit_5 -x130_bit_4 -x130_bit_3 -x130_bit_2 -x130_bit_1 -x130_bit0 -x131_bit_7 -x131_bit_6 -x131_bit_5 -x131_bit_4 -x131_bit_3 -x131_bit_2 -x131_bit_1 -x131_bit0 -x132_bit_7 -x132_bit_6 -x132_bit_5 -x132_bit_4 -x132_bit_3 -x132_bit_2 -x132_bit_1 -x132_bit0 -x133_bit_7 -x133_bit_6 -x133_bit_5 -x133_bit_4 -x133_bit_3 -x133_bit_2 -x133_bit_1 -x133_bit0 -x134_bit_7 -x134_bit_6 -x134_bit_5 -x134_bit_4 -x134_bit_3 -x134_bit_2 -x134_bit_1 -x134_bit0 -x135_bit_7 -x135_bit_6 -x135_bit_5 -x135_bit_4 -x135_bit_3 -x135_bit_2 -x135_bit_1 -x135_bit0 -x136_bit_7 -x136_bit_6 -x136_bit_5 -x136_bit_4 -x136_bit_3 -x136_bit_2 -x136_bit_1 -x136_bit0 -x137_bit_7 -x137_bit_6 -x137_bit_5 -x137_bit_4 -x137_bit_3 -x137_bit_2 -x137_bit_1 -x137_bit0 -x138_bit_7 -x138_bit_6 -x138_bit_5 -x138_bit_4 -x138_bit_3 -x138_bit_2 -x138_bit_1 -x138_bit0 -x139_bit_7 -x139_bit_6 -x139_bit_5 -x139_bit_4 -x139_bit_3 -x139_bit_2 -x139_bit_1 -x139_bit0 -x140_bit_7 -x140_bit_6 -x140_bit_5 -x140_bit_4 -x140_bit_3 -x140_bit_2 -x140_bit_1 -x140_bit0 -x141_bit_7 -x141_bit_6 -x141_bit_5 -x141_bit_4 -x141_bit_3 -x141_bit_2 -x141_bit_1 -x141_bit0 -x142_bit_7 -x142_bit_6 -x142_bit_5 -x142_bit_4 -x142_bit_3 -x142_bit_2 -x142_bit_1 -x142_bit0 -x143_bit_7 -x143_bit_6 -x143_bit_5 -x143_bit_4 -x143_bit_3 -x143_bit_2 -x143_bit_1 -x143_bit0 -x144_bit_7 -x144_bit_6 -x144_bit_5 -x144_bit_4 -x144_bit_3 -x144_bit_2 -x144_bit_1 -x144_bit0 -x145_bit_7 -x145_bit_6 -x145_bit_5 -x145_bit_4 -x145_bit_3 -x145_bit_2 -x145_bit_1 -x145_bit0 -x146_bit_7 -x146_bit_6 -x146_bit_5 x146_bit_4 x146_bit_3 x146_bit_2 -x146_bit_1 -x146_bit0 -x147_bit_7 -x147_bit_6 x147_bit_5 x147_bit_4 x147_bit_3 x147_bit_2 x147_bit_1 -x147_bit0 -x148_bit_7 -x148_bit_6 -x148_bit_5 -x148_bit_4 -x148_bit_3 -x148_bit_2 -x148_bit_1 -x148_bit0 -x149_bit_7 -x149_bit_6 -x149_bit_5 -x149_bit_4 -x149_bit_3 -x149_bit_2 -x149_bit_1 -x149_bit0 -x150_bit_7 -x150_bit_6 -x150_bit_5 -x150_bit_4 -x150_bit_3 -x150_bit_2 -x150_bit_1 -x150_bit0 -x151_bit_7 -x151_bit_6 -x151_bit_5 -x151_bit_4 -x151_bit_3 -x151_bit_2 -x151_bit_1 -x151_bit0 -x152_bit_7 -x152_bit_6 -x152_bit_5 -x152_bit_4 -x152_bit_3 -x152_bit_2 -x152_bit_1 -x152_bit0 -x153_bit_7 -x153_bit_6 -x153_bit_5 -x153_bit_4 -x153_bit_3 -x153_bit_2 -x153_bit_1 -x153_bit0 -x154_bit_7 -x154_bit_6 -x154_bit_5 -x154_bit_4 -x154_bit_3 -x154_bit_2 -x154_bit_1 -x154_bit0 -x155_bit_7 -x155_bit_6 -x155_bit_5 -x155_bit_4 -x155_bit_3 -x155_bit_2 -x155_bit_1 -x155_bit0 -x156_bit_7 -x156_bit_6 -x156_bit_5 -x156_bit_4 -x156_bit_3 -x156_bit_2 -x156_bit_1 -x156_bit0 -x157_bit_7 -x157_bit_6 -x157_bit_5 -x157_bit_4 -x157_bit_3 -x157_bit_2 -x157_bit_1 -x157_bit0 -x158_bit_7 -x158_bit_6 -x158_bit_5 -x158_bit_4 -x158_bit_3 -x158_bit_2 -x158_bit_1 -x158_bit0 -x159_bit_7 -x159_bit_6 -x159_bit_5 -x159_bit_4 -x159_bit_3 -x159_bit_2 -x159_bit_1 -x159_bit0 -x160_bit_7 -x160_bit_6 -x160_bit_5 -x160_bit_4 -x160_bit_3 -x160_bit_2 -x160_bit_1 -x160_bit0 -x161_bit_7 -x161_bit_6 -x161_bit_5 -x161_bit_4 -x161_bit_3 -x161_bit_2 -x161_bit_1 -x161_bit0 -x162_bit_7 -x162_bit_6 -x162_bit_5 -x162_bit_4 -x162_bit_3 -x162_bit_2 -x162_bit_1 -x162_bit0 -x163_bit_7 -x163_bit_6 -x163_bit_5 -x163_bit_4 -x163_bit_3 -x163_bit_2 -x163_bit_1 -x163_bit0 -x164_bit_7 -x164_bit_6 -x164_bit_5 -x164_bit_4 -x164_bit_3 -x164_bit_2 -x164_bit_1 -x164_bit0 -x165_bit_7 -x165_bit_6 -x165_bit_5 -x165_bit_4 -x165_bit_3 -x165_bit_2 -x165_bit_1 -x165_bit0 -x166_bit_7 -x166_bit_6 -x166_bit_5 -x166_bit_4 -x166_bit_3 -x166_bit_2 -x166_bit_1 -x166_bit0 -x167_bit_7 -x167_bit_6 -x167_bit_5 -x167_bit_4 -x167_bit_3 -x167_bit_2 -x167_bit_1 -x167_bit0 -x168_bit_7 -x168_bit_6 -x168_bit_5 -x168_bit_4 -x168_bit_3 -x168_bit_2 -x168_bit_1 -x168_bit0 -x337_bit_7 -x337_bit_6 -x337_bit_5 -x337_bit_4 -x337_bit_3 x337_bit_2 -x337_bit_1 -x337_bit0 -x337_bit1 -x337_bit2 x337_bit3 x337_bit4 x337_bit5 -x337_bit6 -x337_bit7 -x338_bit_7 -x338_bit_6 -x338_bit_5 -x338_bit_4 -x338_bit_3 -x338_bit_2 x338_bit_1 -x338_bit0 -x338_bit1 -x338_bit2 -x338_bit3 x338_bit4 x338_bit5 x338_bit6 -x338_bit7 -x339_bit_7 -x339_bit_6 x339_bit_5 -x339_bit_4 x339_bit_3 x339_bit_2 -x339_bit_1 x339_bit0 x339_bit1 x339_bit2 x339_bit3 x339_bit4 x339_bit5 -x339_bit6 x339_bit7 -x340_bit_7 -x340_bit_6 x340_bit_5 -x340_bit_4 x340_bit_3 x340_bit_2 -x340_bit_1 x340_bit0 x340_bit1 x340_bit2 x340_bit3 x340_bit4 x340_bit5 -x340_bit6 x340_bit7 -x341_bit_7 -x341_bit_6 x341_bit_5 -x341_bit_4 x341_bit_3 x341_bit_2 -x341_bit_1 x341_bit0 x341_bit1 x341_bit2 x341_bit3 x341_bit4 x341_bit5 -x341_bit6 x341_bit7 -x342_bit_7 -x342_bit_6 -x342_bit_5 -x342_bit_4 -x342_bit_3 -x342_bit_2 -x342_bit_1 -x342_bit0 -x342_bit1 -x342_bit2 -x342_bit3 -x342_bit4 -x342_bit5 -x342_bit6 -x342_bit7 -x343_bit_7 -x343_bit_6 -x343_bit_5 -x343_bit_4 -x343_bit_3 -x343_bit_2 -x343_bit_1 -x343_bit0 -x343_bit1 -x343_bit2 x343_bit3 -x343_bit4 -x343_bit5 x343_bit6 x343_bit7 -x344_bit_7 -x344_bit_6 -x344_bit_5 -x344_bit_4 -x344_bit_3 x344_bit_2 -x344_bit_1 x344_bit0 -x344_bit1 -x344_bit2 -x344_bit3 x344_bit4 -x344_bit5 x344_bit6 -x344_bit7 -x345_bit_7 -x345_bit_6 -x345_bit_5 x345_bit_4 x345_bit_3 -x345_bit_2 -x345_bit_1 x345_bit0 -x345_bit1 x345_bit2 -x345_bit3 x345_bit4 x345_bit5 x345_bit6 -x345_bit7 -x346_bit_7 -x346_bit_6 -x346_bit_5 x346_bit_4 -x346_bit_3 -x346_bit_2 -x346_bit_1 -x346_bit0 x346_bit1 -x346_bit2 -x346_bit3 x346_bit4 x346_bit5 x346_bit6 -x346_bit7 -x347_bit_7 -x347_bit_6 -x347_bit_5 x347_bit_4 -x347_bit_3 -x347_bit_2 x347_bit_1 x347_bit0 -x347_bit1 -x347_bit2 -x347_bit3 -x347_bit4 -x347_bit5 -x347_bit6 -x347_bit7 -x348_bit_7 -x348_bit_6 -x348_bit_5 x348_bit_4 -x348_bit_3 -x348_bit_2 x348_bit_1 x348_bit0 -x348_bit1 -x348_bit2 -x348_bit3 -x348_bit4 -x348_bit5 -x348_bit6 -x348_bit7 -x349_bit_7 -x349_bit_6 -x349_bit_5 -x349_bit_4 -x349_bit_3 -x349_bit_2 -x349_bit_1 -x349_bit0 -x349_bit1 x349_bit2 -x349_bit3 -x349_bit4 x349_bit5 x349_bit6 -x350_bit_7 -x350_bit_6 -x350_bit_5 -x350_bit_4 -x350_bit_3 -x350_bit_2 -x350_bit_1 -x350_bit0 -x350_bit1 x350_bit2 -x350_bit3 -x350_bit4 x350_bit5 x350_bit6 -x351_bit_7 -x351_bit_6 -x351_bit_5 -x351_bit_4 -x351_bit_3 -x351_bit_2 -x351_bit_1 -x351_bit0 -x351_bit1 x351_bit2 -x351_bit3 -x351_bit4 x351_bit5 x351_bit6 -x352_bit_7 -x352_bit_6 -x352_bit_5 -x352_bit_4 -x352_bit_3 x352_bit_2 -x352_bit_1 x352_bit0 x352_bit1 x352_bit2 x352_bit3 x352_bit4 -x352_bit5 -x352_bit6 -x353_bit_7 -x353_bit_6 -x353_bit_5 -x353_bit_4 -x353_bit_3 -x353_bit_2 -x353_bit_1 -x353_bit0 -x353_bit1 -x353_bit2 -x353_bit3 -x353_bit4 -x353_bit5 -x353_bit6 -x354_bit_7 -x354_bit_6 -x354_bit_5 -x354_bit_4 -x354_bit_3 -x354_bit_2 -x354_bit_1 -x354_bit0 -x354_bit1 -x354_bit2 -x354_bit3 -x354_bit4 -x354_bit5 -x354_bit6 -x355_bit_7 -x355_bit_6 -x355_bit_5 -x355_bit_4 -x355_bit_3 -x355_bit_2 -x355_bit_1 -x355_bit0 -x355_bit1 x355_bit2 -x355_bit3 -x355_bit4 x355_bit5 x355_bit6 -x356_bit_7 -x356_bit_6 -x356_bit_5 -x356_bit_4 -x356_bit_3 -x356_bit_2 -x356_bit_1 -x356_bit0 -x356_bit1 x356_bit2 -x356_bit3 -x356_bit4 x356_bit5 x356_bit6 -x357_bit_7 -x357_bit_6 -x357_bit_5 -x357_bit_4 -x357_bit_3 -x357_bit_2 -x357_bit_1 -x357_bit0 -x357_bit1 x357_bit2 -x357_bit3 -x357_bit4 x357_bit5 x357_bit6 -x358_bit_7 -x358_bit_6 -x358_bit_5 -x358_bit_4 -x358_bit_3 -x358_bit_2 -x358_bit_1 -x358_bit0 -x358_bit1 x358_bit2 -x358_bit3 -x358_bit4 x358_bit5 x358_bit6 -x359_bit_7 -x359_bit_6 -x359_bit_5 -x359_bit_4 x359_bit_3 -x359_bit#### 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.92 0.95 0.93 2/56 28625
Raw data (stat): 28625 (runsolver) R 28624 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 430793550 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9995 s]
Raw data (loadavg): 0.93 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 14975 0 0 0 964 34 0 0 25 0 1 0 430793550 67874816 14182 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16571 14182 603 41 0 16530 0
vsize: 66284
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 15179 0 0 0 1964 35 0 0 25 0 1 0 430793550 68685824 14386 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16769 14386 603 41 0 16728 0
vsize: 67076
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 15291 0 0 0 2963 35 0 0 25 0 1 0 430793550 69214208 14498 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16898 14498 603 41 0 16857 0
vsize: 67592
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 15493 0 0 0 3963 36 0 0 25 0 1 0 430793550 70074368 14700 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17108 14700 603 41 0 17067 0
vsize: 68432
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 15667 0 0 0 4963 37 0 0 25 0 1 0 430793550 70746112 14874 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14874 603 41 0 17231 0
vsize: 69088
[startup+60.003 s]
Raw data (loadavg): 0.97 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 15852 0 0 0 5962 37 0 0 25 0 1 0 430793550 71606272 15059 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 15059 603 41 0 17441 0
vsize: 69928
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 16023 0 0 0 6961 38 0 0 25 0 1 0 430793550 72269824 15230 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17644 15230 603 41 0 17603 0
vsize: 70576
[startup+80.004 s]
Raw data (loadavg): 0.98 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 16206 0 0 0 7961 38 0 0 25 0 1 0 430793550 72933376 15413 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17806 15413 603 41 0 17765 0
vsize: 71224
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 16511 0 0 0 8961 39 0 0 25 0 1 0 430793550 73879552 15718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18037 15718 603 41 0 17996 0
vsize: 72148
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 16880 0 0 0 9959 41 0 0 25 0 1 0 430793550 75354112 16087 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18397 16087 603 41 0 18356 0
vsize: 73588
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 17176 0 0 0 10958 42 0 0 25 0 1 0 430793550 76689408 16383 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18723 16383 603 41 0 18682 0
vsize: 74892
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 17299 0 0 0 11957 43 0 0 25 0 1 0 430793550 77238272 16506 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18857 16506 603 41 0 18816 0
vsize: 75428
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 17977 0 0 0 12956 45 0 0 25 0 1 0 430793550 79396864 17184 4294967295 134512640 134672761 3221224544 3221223712 134561136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19384 17184 603 41 0 19343 0
vsize: 77536
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 18089 0 0 0 13956 45 0 0 25 0 1 0 430793550 79929344 17296 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19514 17296 603 41 0 19473 0
vsize: 78056
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 18181 0 0 0 14955 46 0 0 25 0 1 0 430793550 80322560 17388 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19610 17388 603 41 0 19569 0
vsize: 78440
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 18295 0 0 0 15955 46 0 0 25 0 1 0 430793550 80732160 17502 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19710 17502 603 41 0 19669 0
vsize: 78840
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 18443 0 0 0 16954 47 0 0 25 0 1 0 430793550 81281024 17650 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19844 17650 603 41 0 19803 0
vsize: 79376
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 18532 0 0 0 17954 47 0 0 25 0 1 0 430793550 81678336 17739 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19941 17739 603 41 0 19900 0
vsize: 79764
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 18617 0 0 0 18954 47 0 0 25 0 1 0 430793550 82079744 17824 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20039 17824 603 41 0 19998 0
vsize: 80156
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 18718 0 0 0 19954 48 0 0 25 0 1 0 430793550 82477056 17925 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20136 17925 603 41 0 20095 0
vsize: 80544
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 18843 0 0 0 20954 48 0 0 25 0 1 0 430793550 82931712 18050 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20247 18050 603 41 0 20206 0
vsize: 80988
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 18988 0 0 0 21953 48 0 0 25 0 1 0 430793550 83599360 18195 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20410 18195 603 41 0 20369 0
vsize: 81640
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 19119 0 0 0 22953 49 0 0 25 0 1 0 430793550 84402176 18326 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20606 18326 603 41 0 20565 0
vsize: 82424
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 19201 0 0 0 23952 50 0 0 25 0 1 0 430793550 84668416 18408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20671 18408 603 41 0 20630 0
vsize: 82684
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 19296 0 0 0 24952 50 0 0 25 0 1 0 430793550 85069824 18503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20769 18503 603 41 0 20728 0
vsize: 83076
[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 19406 0 0 0 25953 50 0 0 25 0 1 0 430793550 85606400 18613 4294967295 134512640 134672761 3221224544 3221223680 134565119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20900 18613 603 41 0 20859 0
vsize: 83600
[startup+270.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 19536 0 0 0 26953 51 0 0 25 0 1 0 430793550 86142976 18743 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21031 18743 603 41 0 20990 0
vsize: 84124
[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 19641 0 0 0 27953 51 0 0 25 0 1 0 430793550 86548480 18848 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21130 18848 603 41 0 21089 0
vsize: 84520
[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 19754 0 0 0 28953 52 0 0 25 0 1 0 430793550 86949888 18961 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21228 18961 603 41 0 21187 0
vsize: 84912
[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28627
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 19868 0 0 0 29952 52 0 0 25 0 1 0 430793550 87478272 19075 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21357 19075 603 41 0 21316 0
vsize: 85428
[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 19962 0 0 0 30952 52 0 0 25 0 1 0 430793550 88420352 19169 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21587 19169 603 41 0 21546 0
vsize: 86348
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 20048 0 0 0 31952 52 0 0 25 0 1 0 430793550 88821760 19255 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21685 19255 603 41 0 21644 0
vsize: 86740
[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 20147 0 0 0 32952 53 0 0 25 0 1 0 430793550 89223168 19354 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21783 19354 603 41 0 21742 0
vsize: 87132
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 20197 0 0 0 33952 53 0 0 25 0 1 0 430793550 89358336 19404 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21816 19404 603 41 0 21775 0
vsize: 87264
[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 20284 0 0 0 34951 54 0 0 25 0 1 0 430793550 89759744 19491 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21914 19491 603 41 0 21873 0
vsize: 87656
[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 20418 0 0 0 35951 54 0 0 25 0 1 0 430793550 90292224 19625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22044 19625 603 41 0 22003 0
vsize: 88176
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 20621 0 0 0 36950 55 0 0 25 0 1 0 430793550 91090944 19828 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22239 19828 603 41 0 22198 0
vsize: 88956
[startup+380.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 20756 0 0 0 37950 56 0 0 25 0 1 0 430793550 91619328 19963 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22368 19963 603 41 0 22327 0
vsize: 89472
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 20867 0 0 0 38950 56 0 0 25 0 1 0 430793550 92160000 20074 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22500 20074 603 41 0 22459 0
vsize: 90000
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 20966 0 0 0 39950 56 0 0 25 0 1 0 430793550 92557312 20173 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22597 20173 603 41 0 22556 0
vsize: 90388
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 21056 0 0 0 40950 56 0 0 25 0 1 0 430793550 92823552 20263 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22662 20263 603 41 0 22621 0
vsize: 90648
[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 21130 0 0 0 41949 57 0 0 25 0 1 0 430793550 93093888 20337 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22728 20337 603 41 0 22687 0
vsize: 90912
[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 21199 0 0 0 42949 57 0 0 25 0 1 0 430793550 93491200 20406 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22825 20406 603 41 0 22784 0
vsize: 91300
[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 21285 0 0 0 43949 57 0 0 25 0 1 0 430793550 93761536 20492 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22891 20492 603 41 0 22850 0
vsize: 91564
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 21427 0 0 0 44949 58 0 0 25 0 1 0 430793550 94437376 20634 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23056 20634 603 41 0 23015 0
vsize: 92224
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 21769 0 0 0 45948 59 0 0 25 0 1 0 430793550 95379456 20976 4294967295 134512640 134672761 3221224544 3221223636 134555596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23286 20976 603 41 0 23245 0
vsize: 93144
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 21872 0 0 0 46948 59 0 0 25 0 1 0 430793550 95797248 21079 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23388 21079 603 41 0 23347 0
vsize: 93552
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 21981 0 0 0 47947 60 0 0 25 0 1 0 430793550 96210944 21188 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23489 21188 603 41 0 23448 0
vsize: 93956
[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 22143 0 0 0 48947 61 0 0 25 0 1 0 430793550 96882688 21350 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23653 21350 603 41 0 23612 0
vsize: 94612
[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 22257 0 0 0 49947 61 0 0 25 0 1 0 430793550 97275904 21464 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23749 21464 603 41 0 23708 0
vsize: 94996
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 22349 0 0 0 50946 61 0 0 25 0 1 0 430793550 97800192 21556 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23877 21556 603 41 0 23836 0
vsize: 95508
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 22448 0 0 0 51946 62 0 0 25 0 1 0 430793550 98070528 21655 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23943 21655 603 41 0 23902 0
vsize: 95772
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 22542 0 0 0 52946 62 0 0 25 0 1 0 430793550 98480128 21749 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24043 21749 603 41 0 24002 0
vsize: 96172
[startup+540.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 22685 0 0 0 53946 62 0 0 25 0 1 0 430793550 99024896 21892 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24176 21892 603 41 0 24135 0
vsize: 96704
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 22801 0 0 0 54945 63 0 0 25 0 1 0 430793550 99565568 22008 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24308 22008 603 41 0 24267 0
vsize: 97232
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 22930 0 0 0 55944 64 0 0 25 0 1 0 430793550 100093952 22137 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24437 22137 603 41 0 24396 0
vsize: 97748
[startup+570.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23016 0 0 0 56946 64 0 0 25 0 1 0 430793550 100499456 22223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24536 22223 603 41 0 24495 0
vsize: 98144
[startup+580.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23110 0 0 0 57946 64 0 0 25 0 1 0 430793550 100900864 22317 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24634 22317 603 41 0 24593 0
vsize: 98536
[startup+590.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23231 0 0 0 58946 64 0 0 25 0 1 0 430793550 101830656 22438 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24861 22438 603 41 0 24820 0
vsize: 99444
[startup+600.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28629
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23384 0 0 0 59946 65 0 0 25 0 1 0 430793550 102502400 22591 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25025 22591 603 41 0 24984 0
vsize: 100100
[startup+610.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23445 0 0 0 60946 65 0 0 25 0 1 0 430793550 102764544 22652 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25089 22652 603 41 0 25048 0
vsize: 100356
[startup+620.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23515 0 0 0 61945 66 0 0 25 0 1 0 430793550 103030784 22722 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25154 22722 603 41 0 25113 0
vsize: 100616
[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23602 0 0 0 62944 66 0 0 25 0 1 0 430793550 103432192 22809 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25252 22809 603 41 0 25211 0
vsize: 101008
[startup+640.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23659 0 0 0 63944 66 0 0 25 0 1 0 430793550 103702528 22866 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25318 22866 603 41 0 25277 0
vsize: 101272
[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23696 0 0 0 64944 66 0 0 25 0 1 0 430793550 103837696 22903 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25351 22903 603 41 0 25310 0
vsize: 101404
[startup+660.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23775 0 0 0 65944 67 0 0 25 0 1 0 430793550 104103936 22982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25416 22982 603 41 0 25375 0
vsize: 101664
[startup+670.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23857 0 0 0 66945 67 0 0 25 0 1 0 430793550 104509440 23064 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25515 23064 603 41 0 25474 0
vsize: 102060
[startup+680.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23928 0 0 0 67944 68 0 0 25 0 1 0 430793550 104775680 23135 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25580 23135 603 41 0 25539 0
vsize: 102320
[startup+690.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 23969 0 0 0 68944 68 0 0 25 0 1 0 430793550 104910848 23176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25613 23176 603 41 0 25572 0
vsize: 102452
[startup+700.069 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24028 0 0 0 69945 68 0 0 25 0 1 0 430793550 105177088 23235 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25678 23235 603 41 0 25637 0
vsize: 102712
[startup+710.068 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24091 0 0 0 70945 68 0 0 25 0 1 0 430793550 105439232 23298 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25742 23298 603 41 0 25701 0
vsize: 102968
[startup+720.069 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24123 0 0 0 71945 69 0 0 25 0 1 0 430793550 105570304 23330 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25774 23330 603 41 0 25733 0
vsize: 103096
[startup+730.069 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24149 0 0 0 72945 69 0 0 25 0 1 0 430793550 105701376 23356 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25806 23356 603 41 0 25765 0
vsize: 103224
[startup+740.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24189 0 0 0 73945 69 0 0 25 0 1 0 430793550 105832448 23396 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25838 23396 603 41 0 25797 0
vsize: 103352
[startup+750.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24242 0 0 0 74945 69 0 0 25 0 1 0 430793550 105971712 23449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25872 23449 603 41 0 25831 0
vsize: 103488
[startup+760.069 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24295 0 0 0 75945 69 0 0 25 0 1 0 430793550 106237952 23502 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25937 23502 603 41 0 25896 0
vsize: 103748
[startup+770.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24404 0 0 0 76945 69 0 0 25 0 1 0 430793550 106635264 23611 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26034 23611 603 41 0 25993 0
vsize: 104136
[startup+780.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24537 0 0 0 77946 70 0 0 25 0 1 0 430793550 107302912 23744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26197 23744 603 41 0 26156 0
vsize: 104788
[startup+790.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24622 0 0 0 78945 70 0 0 25 0 1 0 430793550 107565056 23829 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26261 23829 603 41 0 26220 0
vsize: 105044
[startup+800.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24725 0 0 0 79945 71 0 0 25 0 1 0 430793550 107966464 23932 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26359 23932 603 41 0 26318 0
vsize: 105436
[startup+810.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 24841 0 0 0 80945 71 0 0 25 0 1 0 430793550 108503040 24048 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26490 24048 603 41 0 26449 0
vsize: 105960
[startup+820.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25006 0 0 0 81944 72 0 0 25 0 1 0 430793550 109170688 24213 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26653 24213 603 41 0 26612 0
vsize: 106612
[startup+830.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25137 0 0 0 82944 72 0 0 25 0 1 0 430793550 109723648 24344 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26788 24344 603 41 0 26747 0
vsize: 107152
[startup+840.084 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25197 0 0 0 83944 73 0 0 25 0 1 0 430793550 109993984 24404 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26854 24404 603 41 0 26813 0
vsize: 107416
[startup+850.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25247 0 0 0 84944 73 0 0 25 0 1 0 430793550 110129152 24454 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26887 24454 603 41 0 26846 0
vsize: 107548
[startup+860.084 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25338 0 0 0 85944 73 0 0 25 0 1 0 430793550 110538752 24545 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26987 24545 603 41 0 26946 0
vsize: 107948
[startup+870.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25406 0 0 0 86944 73 0 0 25 0 1 0 430793550 110809088 24613 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27053 24613 603 41 0 27012 0
vsize: 108212
[startup+880.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25420 0 0 0 87944 73 0 0 25 0 1 0 430793550 110809088 24627 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27053 24627 603 41 0 27012 0
vsize: 108212
[startup+890.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25436 0 0 0 88944 74 0 0 25 0 1 0 430793550 110940160 24643 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27085 24643 603 41 0 27044 0
vsize: 108340
[startup+900.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28631
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25451 0 0 0 89944 74 0 0 25 0 1 0 430793550 110940160 24658 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27085 24658 603 41 0 27044 0
vsize: 108340
[startup+910.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25465 0 0 0 90944 74 0 0 25 0 1 0 430793550 111071232 24672 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27117 24672 603 41 0 27076 0
vsize: 108468
[startup+920.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25514 0 0 0 91944 74 0 0 25 0 1 0 430793550 111206400 24721 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27150 24721 603 41 0 27109 0
vsize: 108600
[startup+930.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25577 0 0 0 92944 74 0 0 25 0 1 0 430793550 111472640 24784 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27215 24784 603 41 0 27174 0
vsize: 108860
[startup+940.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25660 0 0 0 93944 75 0 0 25 0 1 0 430793550 111874048 24867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27313 24867 603 41 0 27272 0
vsize: 109252
[startup+950.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25730 0 0 0 94944 75 0 0 25 0 1 0 430793550 112136192 24937 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27377 24937 603 41 0 27336 0
vsize: 109508
[startup+960.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25814 0 0 0 95944 75 0 0 25 0 1 0 430793550 112402432 25021 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27442 25021 603 41 0 27401 0
vsize: 109768
[startup+970.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 96944 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134561639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+980.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 97944 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+990.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 98944 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 99945 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 100945 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 101945 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 102945 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 103945 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 104946 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 105946 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 106946 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 107946 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 108946 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 109946 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 110947 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 111947 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 112947 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 113947 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 114947 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 115947 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 116948 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 117948 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 118948 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 28633
Raw data (stat): 28625 (minisat+) R 28624 12452 12451 0 -1 0 25870 0 0 0 119948 76 0 0 25 0 1 0 430793550 112672768 25077 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27508 25077 603 41 0 27467 0
vsize: 110032
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.93 1/56 28633
Raw data (stat): 28625 (minisat+) Z 28624 12452 12451 0 -1 12 25873 0 0 0 119949 81 0 0 25 0 1 0 430793550 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.15
CPU time (s): 1200.3
CPU user time (s): 1199.49
CPU system time (s): 0.810876
CPU usage (%): 100.012
Max. virtual memory (Kb): 110032
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####