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 32369

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        881636 kB
Buffers:         14832 kB
Cached:         117592 kB
SwapCached:        788 kB
Active:          17812 kB
Inactive:       116876 kB
HighTotal:      131008 kB
HighFree:        10584 kB
LowTotal:       903652 kB
LowFree:        871052 kB
SwapTotal:     2097640 kB
SwapFree:      2096168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5448 kB
Slab:            12740 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 09:49:03 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 23751 7 1229.88 152
#### 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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 ---[   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 |    197113 |  479845  1317473 |  377149   49657  2541259    51.2 |  0.794 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 19110 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.93 0.98 0.91 2/54 19106
Raw data (stat): 19106 (runsolver) R 19105 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855089805 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0007 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.002 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0027 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.002 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0023 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.111 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.111 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.11 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.111 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.111 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.111 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.112 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.112 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.112 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.113 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.114 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.114 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.114 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.115 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.114 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.115 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.115 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.118 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.118 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.118 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.119 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.12 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.119 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.119 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.12 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.119 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.12 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.121 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.12 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.121 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.122 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.123 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.123 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.123 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.124 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.123 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.124 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.125 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.125 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.125 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.126 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.126 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.126 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.126 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.127 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.127 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.128 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.129 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.128 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.129 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.13 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.13 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.13 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.13 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.13 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.13 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.139 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.139 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.139 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.139 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.139 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.14 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.15 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.15 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.15 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.71 s]
Raw data (loadavg): 0.99 0.98 0.91 1/53 19110
Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.71
CPU time (s): 1229.88
CPU user time (s): 1229.1
CPU system time (s): 0.777881
CPU usage (%): 100.014
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####