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/miplib3/normalized-mps-v2-13-7-rout.opb
MD5SUM	43b060c182b659f22c02b8a980d1ee8f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1221280
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	33812000
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	166074535
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1569.48
Number of variables	5151
Total number of constraints	606
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	314
Number of constraints which are nor clauses,nor cardinality constraints	292
Minimum length of a constraint	1
Maximum length of a constraint	617
Trace number 31235

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-05-25 23:18:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22635 boxname=wulflinc9 idbench=1451 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  43b060c182b659f22c02b8a980d1ee8f  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-rout.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-rout.opb
IDLAUNCH: 22635
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        517188 kB
Buffers:         38156 kB
Cached:         458068 kB
SwapCached:        584 kB
Active:          17696 kB
Inactive:       480564 kB
HighTotal:      131008 kB
HighFree:        31416 kB
LowTotal:       903652 kB
LowFree:        485772 kB
SwapTotal:     2097136 kB
SwapFree:      2095648 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            13568 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 23:39:14 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22635 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 337 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################
c   -- Clauses(.)/Splits(s): ...............
c ---[ 320]---> Adder-cost: 3854   maxlim: 97129415   bits: 27/27
c ---[ 319]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 318]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 317]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 316]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 315]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 314]---> BDD-cost:   37
c ---[ 313]---> BDD-cost:   37
c ---[ 312]---> BDD-cost:   84
c ---[ 311]---> BDD-cost:   37
c ---[ 310]---> BDD-cost:   37
c ---[ 309]---> BDD-cost:   37
c ---[ 308]---> BDD-cost:   37
c ---[ 307]---> BDD-cost:   37
c ---[ 306]---> BDD-cost:   37
c ---[ 305]---> BDD-cost:   37
c ---[ 304]---> BDD-cost:   37
c ---[ 303]---> BDD-cost:   37
c ---[ 302]---> BDD-cost:   37
c ---[ 301]---> BDD-cost:   37
c ---[ 300]---> BDD-cost:   37
c ---[ 298]---> Sorter-cost:  441     Base: 2
c ---[ 296]---> Sorter-cost:  441     Base: 2
c ---[ 294]---> Sorter-cost:  441     Base: 2
c ---[ 292]---> Sorter-cost:  441     Base: 2
c ---[ 290]---> Sorter-cost:  441     Base: 2
c ---[ 288]---> Sorter-cost:  347     Base: 2
c ---[ 286]---> Sorter-cost:  347     Base: 2
c ---[ 284]---> Sorter-cost:  347     Base: 2
c ---[ 282]---> Sorter-cost:  347     Base: 2
c ---[ 280]---> Sorter-cost:  347     Base: 2
c ---[ 278]---> Sorter-cost:  515     Base: 2
c ---[ 276]---> Sorter-cost:  515     Base: 2
c ---[ 274]---> Sorter-cost:  515     Base: 2
c ---[ 272]---> Sorter-cost:  515     Base: 2
c ---[ 270]---> Sorter-cost:  515     Base: 2
c ---[ 268]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[ 266]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[ 264]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[ 262]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[ 260]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[ 258]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[ 256]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[ 254]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[ 252]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[ 250]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[ 248]---> Adder-cost: 608   maxlim: 21483   bits: 16/15
c ---[ 246]---> Adder-cost: 608   maxlim: 21483   bits: 16/15
c ---[ 244]---> Adder-cost: 608   maxlim: 21483   bits: 16/15
c ---[ 242]---> Adder-cost: 608   maxlim: 21483   bits: 16/15
c ---[ 240]---> Adder-cost: 608   maxlim: 21483   bits: 16/15
c ---[ 239]---> BDD-cost:   13
c ---[ 238]---> BDD-cost:   13
c ---[ 237]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   13
c ---[ 235]---> BDD-cost:   13
c ---[ 234]---> BDD-cost:   13
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   13
c ---[ 231]---> BDD-cost:   13
c ---[ 230]---> BDD-cost:   13
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   13
c ---[ 226]---> BDD-cost:   13
c ---[ 225]---> BDD-cost:   13
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   13
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   13
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   13
c ---[ 218]---> BDD-cost:   13
c ---[ 217]---> BDD-cost:   13
c ---[ 216]---> BDD-cost:   13
c ---[ 215]---> BDD-cost:   13
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   13
c ---[ 211]---> BDD-cost:   13
c ---[ 210]---> BDD-cost:   13
c ---[ 209]---> BDD-cost:   13
c ---[ 208]---> BDD-cost:   13
c ---[ 207]---> BDD-cost:   13
c ---[ 206]---> BDD-cost:   13
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   13
c ---[ 202]---> BDD-cost:   13
c ---[ 201]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   13
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   13
c ---[ 197]---> BDD-cost:   13
c ---[ 196]---> BDD-cost:   13
c ---[ 195]---> BDD-cost:   13
c ---[ 194]---> BDD-cost:   13
c ---[ 193]---> BDD-cost:   13
c ---[ 192]---> BDD-cost:   13
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:   13
c ---[ 189]---> BDD-cost:   25
c ---[ 188]---> BDD-cost:   25
c ---[ 187]---> BDD-cost:   25
c ---[ 186]---> BDD-cost:   25
c ---[ 185]---> BDD-cost:   25
c ---[ 184]---> BDD-cost:   25
c ---[ 183]---> BDD-cost:   25
c ---[ 182]---> BDD-cost:   25
c ---[ 181]---> BDD-cost:   25
c ---[ 180]---> BDD-cost:   25
c ---[ 179]---> BDD-cost:   13
c ---[ 178]---> BDD-cost:   13
c ---[ 177]---> BDD-cost:   13
c ---[ 176]---> BDD-cost:   13
c ---[ 175]---> BDD-cost:   13
c ---[ 174]---> BDD-cost:   13
c ---[ 173]---> BDD-cost:   13
c ---[ 172]---> BDD-cost:   13
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   13
c ---[ 167]---> BDD-cost:   13
c ---[ 166]---> BDD-cost:   13
c ---[ 165]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   13
c ---[ 160]---> BDD-cost:   13
c ---[ 159]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   13
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   13
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   13
c ---[ 151]---> BDD-cost:   13
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   13
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   13
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   13
c ---[ 143]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:   13
c ---[ 139]---> BDD-cost:   13
c ---[ 138]---> BDD-cost:   13
c ---[ 137]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   13
c ---[ 135]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   13
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   13
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   13
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   13
c ---[ 125]---> BDD-cost:   13
c ---[ 124]---> BDD-cost:   13
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   13
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   13
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   13
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   13
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   13
c ---[ 103]---> BDD-cost:   13
c ---[ 102]---> BDD-cost:   13
c ---[ 101]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   13
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   13
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   13
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   13
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   13
c ---[  74]---> BDD-cost:   13
c ---[  73]---> BDD-cost:   13
c ---[  72]---> BDD-cost:   13
c ---[  71]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   13
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   13
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   13
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   13
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   13
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   13
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  124244   417096 |   41414       0        0     nan |  0.000 % |
c |       101 |  124217   417035 |   45555     100      698     7.0 | 12.443 % |
c |       251 |  124062   416689 |   50110     246     6914    28.1 | 12.591 % |
c |       476 |  123805   416084 |   55122     454    13340    29.4 | 12.865 % |
c |       816 |  123756   415925 |   60634     787    18326    23.3 | 12.898 % |
c |      1324 |  123756   415925 |   66697    1295    35601    27.5 | 12.898 % |
c |      2084 |  123085   414363 |   73367    1962    62841    32.0 | 13.602 % |
c |      3224 |  122985   414092 |   80704    3096   118065    38.1 | 13.696 % |
c |      4934 |  122862   413789 |   88774    4790   197053    41.1 | 13.819 % |
c |      7497 |  122620   413234 |   97652    7339   309485    42.2 | 14.072 % |
c |     11341 |  122262   412313 |  107417   11128   514303    46.2 | 14.407 % |
c |     17107 |  121189   409690 |  118158   16758   762422    45.5 | 15.448 % |
c |     25756 |  120340   407507 |  129974   25263  1148488    45.5 | 16.250 % |
c ==============================================================================
c [1mFound solution: 1285216[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30291 |  119977   406542 |   39992   29735  1411880    47.5 | 16.250 % |
c |     30391 |  119977   406542 |   43991   29835  1412942    47.4 | 16.578 % |
c |     30543 |  119977   406542 |   48390   29987  1416578    47.2 | 16.578 % |
c |     30770 |  119977   406542 |   53229   30214  1435944    47.5 | 16.578 % |
c |     31108 |  119716   405913 |   58552   30528  1448420    47.4 | 16.838 % |
c |     31614 |  119684   405809 |   64407   31029  1466017    47.2 | 16.859 % |
c |     32374 |  119680   405800 |   70848   31788  1499929    47.2 | 16.863 % |
c |     33513 |  119617   405636 |   77933   32925  1610828    48.9 | 16.924 % |
c |     35222 |  119600   405579 |   85726   34629  1714499    49.5 | 16.931 % |
c |     37785 |  119575   405496 |   94299   37179  1839171    49.5 | 16.942 % |
c |     41629 |  119438   405146 |  103728   41015  2130976    52.0 | 17.065 % |
c |     47396 |  119223   404565 |  114101   46770  2351738    50.3 | 17.264 % |
c |     56047 |  119086   404232 |  125512   55411  2812411    50.8 | 17.408 % |
c ==============================================================================
c [1mFound solution: 1251200[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64248 |  119011   403982 |   39670   63593  3313693    52.1 | 17.408 % |
c |     64348 |  119003   403956 |   43637   17993   679000    37.7 | 17.458 % |
c |     64499 |  119003   403956 |   48000   18144   680284    37.5 | 17.458 % |
c |     64725 |  119003   403956 |   52800   18370   686673    37.4 | 17.458 % |
c |     65062 |  118823   403544 |   58080   18694   696874    37.3 | 17.667 % |
c |     65569 |  118740   403355 |   63888   19196   729606    38.0 | 17.761 % |
c |     66328 |  118714   403265 |   70277   19948   757553    38.0 | 17.776 % |
c |     67468 |  118678   403184 |   77305   21085   895546    42.5 | 17.815 % |
c |     69176 |  118623   403060 |   85036   22778  1086526    47.7 | 17.877 % |
c |     71738 |  118578   402925 |   93539   25334  1193623    47.1 | 17.905 % |
c |     75582 |  118405   402338 |  102893   29145  1553328    53.3 | 17.970 % |
c |     81349 |  118010   401262 |  113183   34854  2113396    60.6 | 18.292 % |
c |     89998 |  117841   400764 |  124501   43484  2710361    62.3 | 18.407 % |
c ==============================================================================
c [1mFound solution: 1248960[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97930 |  117543   399817 |   39181   51376  3282887    63.9 | 18.407 % |
c |     98031 |  117543   399817 |   43099   17682   835672    47.3 | 18.565 % |
c |     98182 |  117543   399817 |   47409   17833   840056    47.1 | 18.565 % |
c |     98407 |  117528   399784 |   52149   18054   853589    47.3 | 18.583 % |
c |     98745 |  117528   399784 |   57364   18392   860176    46.8 | 18.583 % |
c |     99253 |  117356   399392 |   63101   18891   876968    46.4 | 18.778 % |
c |    100017 |  117356   399392 |   69411   19655   904697    46.0 | 18.778 % |
c |    101156 |  117270   399167 |   76352   20788  1011115    48.6 | 18.857 % |
c |    102865 |  117062   398567 |   83987   22178  1100209    49.6 | 19.045 % |
c |    105428 |  117062   398567 |   92386   24741  1202538    48.6 | 19.045 % |
c |    109274 |  117026   398443 |  101625   28582  1650684    57.8 | 19.059 % |
c ==============================================================================
c [1mFound solution: 1246144[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    112627 |  117039   398474 |   39013   31935  1952177    61.1 | 19.059 % |
c |    112729 |  117039   398474 |   42914   32037  1958040    61.1 | 19.060 % |
c |    112879 |  117039   398474 |   47205   32187  1971623    61.3 | 19.060 % |
c |    113104 |  117039   398474 |   51926   32412  1978748    61.0 | 19.060 % |
c |    113442 |  117039   398474 |   57118   32750  1992939    60.9 | 19.060 % |
c |    113948 |  117039   398474 |   62830   33256  2016699    60.6 | 19.060 % |
c |    114712 |  117029   398451 |   69113   34019  2041172    60.0 | 19.070 % |
c |    115853 |  117029   398451 |   76025   35160  2268157    64.5 | 19.070 % |
c |    117563 |  116823   397964 |   83627   36858  2393497    64.9 | 19.341 % |
c |    120125 |  116823   397964 |   91990   39420  2606433    66.1 | 19.341 % |
c ==============================================================================
c [1mFound solution: 1234880[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122895 |  116807   397899 |   38935   42182  2736619    64.9 | 19.341 % |
c |    122996 |  116807   397899 |   42828   42283  2738718    64.8 | 19.356 % |
c |    123146 |  116807   397899 |   47111   42433  2746931    64.7 | 19.356 % |
c |    123373 |  116807   397899 |   51822   42660  2755996    64.6 | 19.356 % |
c |    123711 |  116792   397846 |   57004   42994  2794961    65.0 | 19.360 % |
c |    124217 |  116580   397224 |   62705   43481  2821750    64.9 | 19.512 % |
c |    124976 |  116491   396913 |   68975   44228  2858088    64.6 | 19.544 % |
c |    126116 |  116480   396889 |   75873   45365  2909809    64.1 | 19.558 % |
c |    127830 |  116480   396889 |   83460   47079  3109096    66.0 | 19.558 % |
c |    130392 |  116390   396661 |   91806   49631  3488547    70.3 | 19.659 % |
c |    134238 |  116390   396661 |  100987   53477  3848404    72.0 | 19.659 % |
c |    140004 |  115826   394740 |  111086   59149  4268263    72.2 | 19.883 % |
c |    148653 |  115653   394198 |  122194   67774  4735565    69.9 | 19.991 % |
c |    161629 |  114458   390240 |  134414   80215  5727660    71.4 | 20.619 % |
c |    181093 |  114381   390000 |  147855   99662  8618461    86.5 | 20.670 % |
c |    210287 |  113873   388445 |  162641  128776 12743443    99.0 | 21.023 % |
c |    254076 |  113316   386586 |  178905   30880  3080645    99.8 | 21.319 % |
c ==============================================================================
c [1mFound solution: 1233728[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    297161 |  113199   386212 |   37733   73937  8061862   109.0 | 21.319 % |
c |    297262 |  113199   386212 |   41506   23322  1900788    81.5 | 21.405 % |
c |    297414 |  113199   386212 |   45656   23474  1906738    81.2 | 21.405 % |
c |    297641 |  113199   386212 |   50222   23701  1927801    81.3 | 21.405 % |
c |    297978 |  113199   386212 |   55244   24038  1947263    81.0 | 21.405 % |
c |    298484 |  113199   386212 |   60769   24544  2029571    82.7 | 21.405 % |
c |    299243 |  113199   386212 |   66846   25303  2077259    82.1 | 21.405 % |
c |    300383 |  113199   386212 |   73530   26443  2106865    79.7 | 21.405 % |
c ==============================================================================
c [1mFound solution: 1219168[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    300741 |  113217   386254 |   37739   26801  2188556    81.7 | 21.405 % |
c |    300843 |  113217   386254 |   41512   26903  2189597    81.4 | 21.401 % |
c |    300994 |  113217   386254 |   45664   27054  2195142    81.1 | 21.401 % |
c |    301221 |  113217   386254 |   50230   27281  2221836    81.4 | 21.401 % |
c |    301558 |  113217   386254 |   55253   27618  2239887    81.1 | 21.401 % |
c |    302064 |  113217   386254 |   60779   28124  2270146    80.7 | 21.401 % |
c |    302824 |  113217   386254 |   66856   28884  2340382    81.0 | 21.401 % |
c |    303963 |  113156   386104 |   73542   30013  2392486    79.7 | 21.476 % |
c |    305671 |  113156   386104 |   80896   31721  2698061    85.1 | 21.476 % |
c |    308235 |  113137   386035 |   88986   34282  3088884    90.1 | 21.487 % |
c |    312080 |  113137   386035 |   97885   38127  3656945    95.9 | 21.487 % |
c |    317846 |  113137   386035 |  107673   43893  4218970    96.1 | 21.487 % |
c |    326495 |  113128   386004 |  118441   52538  5743778   109.3 | 21.491 % |
c |    339470 |  113073   385819 |  130285   65501  8650761   132.1 | 21.520 % |
c |    358931 |  113069   385810 |  143313   84958 12148453   143.0 | 21.523 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 25355 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.92 2/54 25351
Raw data (stat): 25351 (runsolver) R 25350 3944 3943 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784560298 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.0006 s]
Raw data (loadavg): 0.94 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0003 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0014 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0009 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0006 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0007 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0012 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0024 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.75 s]
Raw data (loadavg): 0.99 0.98 0.92 1/53 25355
Raw data (stat): 25351 (minisat+_script) S 25350 3944 3943 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784560298 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.75
CPU time (s): 1229.88
CPU user time (s): 1229.13
CPU system time (s): 0.751885
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####