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/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a2.opb
MD5SUM	6005a01d3f2ae55b0ca9c19f876c5827
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	139
Optimality of the best value was proved	NO
Number of terms in the objective function	360
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	360
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	360
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	360
Total number of constraints	980
Number of constraints which are clauses	980
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 6255

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 04:00:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4676 boxname=wulflinc32 idbench=164 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6005a01d3f2ae55b0ca9c19f876c5827  /oldhome/oroussel/tmp/wulflinc32/normalized-ii8a2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc32/normalized-ii8a2.opb /oldhome/oroussel/tmp/wulflinc32/normalized-ii8a2.opb
IDLAUNCH: 4676
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        701628 kB
Buffers:         35356 kB
Cached:         186200 kB
SwapCached:       1212 kB
Active:         147472 kB
Inactive:       154392 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        701372 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25432 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:20:28 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4676 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 980 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     980     2412 |     326       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 150[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13276     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |   32604    76428 |   10868       3       20     6.7 |  0.000 % |
c |       104 |   32406    75983 |   11954      96      468     4.9 |  0.740 % |
c |       254 |   29960    70368 |   13150     173     1330     7.7 |  7.530 % |
c |       479 |   27314    64330 |   14465     351     2994     8.5 | 14.783 % |
c |       816 |   19537    46439 |   15911     459     3504     7.6 | 37.382 % |
c |      1323 |   17615    42007 |   17503     910    27349    30.1 | 42.701 % |
c |      2084 |   16909    40368 |   19253    1659    72886    43.9 | 44.875 % |
c |      3226 |   14474    34721 |   21178    2712    93483    34.5 | 52.266 % |
c |      4935 |   13262    31907 |   23296    3594   107287    29.9 | 56.022 % |
c ==============================================================================
c [1mFound solution: 149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5140 |   13148    31648 |    4382    3656   110475    30.2 | 56.022 % |
c |      5240 |   12533    30216 |    4820    3736   112116    30.0 | 58.364 % |
c |      5390 |   12533    30216 |    5302    3886   113117    29.1 | 58.364 % |
c |      5615 |   12533    30216 |    5832    4111   121329    29.5 | 58.364 % |
c |      5952 |   12210    29470 |    6415    4436   128777    29.0 | 59.306 % |
c |      6459 |   12052    29103 |    7057    4910   142504    29.0 | 59.795 % |
c ==============================================================================
c [1mFound solution: 148[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7086 |   11930    28812 |    3976    5513   158913    28.8 | 59.795 % |
c ==============================================================================
c [1mFound solution: 147[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7092 |   11974    28923 |    3991    5519   158972    28.8 | 59.795 % |
c ==============================================================================
c [1mFound solution: 146[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7103 |   11945    28846 |    3981    5497   157412    28.6 | 59.795 % |
c |      7203 |   11830    28581 |    4379    5592   158303    28.3 | 60.505 % |
c |      7354 |   11830    28581 |    4817    5743   161665    28.1 | 60.505 % |
c |      7579 |   11830    28581 |    5298    5968   171463    28.7 | 60.505 % |
c |      7917 |   11830    28581 |    5828    6306   185820    29.5 | 60.505 % |
c ==============================================================================
c [1mFound solution: 145[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8311 |   11800    28519 |    3933    6687   202725    30.3 | 60.505 % |
c |      8411 |   11800    28519 |    4326    6787   204324    30.1 | 60.712 % |
c |      8561 |   11683    28250 |    4758    6931   205825    29.7 | 61.043 % |
c |      8786 |   11683    28250 |    5234    7156   213786    29.9 | 61.043 % |
c |      9123 |   11587    28025 |    5758    7490   227687    30.4 | 61.337 % |
c |      9629 |   11587    28025 |    6334    7996   246414    30.8 | 61.337 % |
c |     10388 |   11587    28025 |    6967    8755   278203    31.8 | 61.337 % |
c |     11529 |   11587    28025 |    7664    9896   325023    32.8 | 61.337 % |
c |     13239 |   11476    27769 |    8430   11598   392462    33.8 | 61.650 % |
c |     15801 |   11476    27769 |    9273   14160   490355    34.6 | 61.650 % |
c |     19646 |   11476    27769 |   10201    9156   320683    35.0 | 61.650 % |
c |     25413 |   11476    27769 |   11221   14923   590524    39.6 | 61.650 % |
c |     34062 |   11476    27769 |   12343   14037   569995    40.6 | 61.650 % |
c |     47036 |   11476    27769 |   13577   16809   585254    34.8 | 61.650 % |
c |     66497 |   11415    27625 |   14935   14402   517399    35.9 | 61.861 % |
c |     95689 |   11411    27616 |   16429   20224   871653    43.1 | 61.870 % |
c |    139479 |   11411    27616 |   18072   15071   582857    38.7 | 61.870 % |
c |    205163 |   11411    27616 |   19879   14992   621756    41.5 | 61.870 % |
c |    303689 |   11411    27616 |   21867   14825   512868    34.6 | 61.870 % |
c ==============================================================================
c [1mFound solution: 144[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    345495 |   11382    27541 |    3794   25475  1349393    53.0 | 61.870 % |
c |    345595 |   11382    27541 |    4173    6469   235841    36.5 | 61.951 % |
c |    345745 |   11382    27541 |    4590    6619   240732    36.4 | 61.951 % |
c |    345970 |   11382    27541 |    5049    6844   247798    36.2 | 61.951 % |
c |    346307 |   11382    27541 |    5554    7181   261832    36.5 | 61.951 % |
c |    346814 |   11382    27541 |    6110    7688   277016    36.0 | 61.951 % |
c |    347576 |   11382    27541 |    6721    8450   296157    35.0 | 61.951 % |
c |    348716 |   11382    27541 |    7393    9590   340495    35.5 | 61.951 % |
c ==============================================================================
c [1mFound solution: 143[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    348987 |   11426    27652 |    3808    9861   348511    35.3 | 61.951 % |
c |    349088 |   11426    27652 |    4188    9962   349169    35.1 | 61.887 % |
c |    349240 |   11426    27652 |    4607   10114   351615    34.8 | 61.887 % |
c |    349465 |   11426    27652 |    5068   10339   356046    34.4 | 61.887 % |
c |    349802 |   11426    27652 |    5575   10676   361882    33.9 | 61.887 % |
c |    350308 |   11426    27652 |    6132   11182   372977    33.4 | 61.887 % |
c |    351068 |   11426    27652 |    6746   11942   394960    33.1 | 61.887 % |
c |    352207 |   11426    27652 |    7420   13081   474005    36.2 | 61.887 % |
c |    353915 |   11426    27652 |    8162   14789   542568    36.7 | 61.887 % |
c |    356479 |   11426    27652 |    8979    9477   345030    36.4 | 61.887 % |
c |    360325 |   11426    27652 |    9876   13323   557675    41.9 | 61.887 % |
c |    366091 |   11426    27652 |   10864    9969   405072    40.6 | 61.887 % |
c |    374740 |   11422    27643 |   11951    9467   409062    43.2 | 61.896 % |
c ==============================================================================
c [1mFound solution: 142[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    377442 |   11390    27557 |    3796   12169   557688    45.8 | 61.896 % |
c |    377546 |   11390    27557 |    4175    6189   229497    37.1 | 61.986 % |
c |    377697 |   11390    27557 |    4593    6340   231547    36.5 | 61.986 % |
c |    377922 |   11390    27557 |    5052    6565   238680    36.4 | 61.986 % |
c |    378259 |   11390    27557 |    5557    6902   248402    36.0 | 61.986 % |
c |    378768 |   11390    27557 |    6113    7411   271567    36.6 | 61.986 % |
c |    379532 |   11390    27557 |    6724    8175   303188    37.1 | 61.986 % |
c |    380672 |   11390    27557 |    7397    9315   358323    38.5 | 61.986 % |
c |    382381 |   11390    27557 |    8137   11024   484158    43.9 | 61.986 % |
c |    384944 |   11390    27557 |    8950   13587   635326    46.8 | 61.986 % |
c |    388789 |   11390    27557 |    9845    9049   392125    43.3 | 61.986 % |
c |    394555 |   11390    27557 |   10830   14815   620935    41.9 | 61.986 % |
c |    403204 |   11390    27557 |   11913   13870   599212    43.2 | 61.986 % |
c |    416179 |   11390    27557 |   13104   16718   780912    46.7 | 61.986 % |
c |    435640 |   11390    27557 |   14415   14609   661156    45.3 | 61.986 % |
c |    464832 |   11390    27557 |   15856   20986   911321    43.4 | 61.986 % |
c |    508621 |   11390    27557 |   17442   16392   653931    39.9 | 61.986 % |
c |    574306 |   11390    27557 |   19186   17400   738755    42.5 | 61.986 % |
#### 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.88 0.94 0.90 2/53 15285
Raw data (stat): 15285 (runsolver) R 15284 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481539771 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.90 0.94 0.90 2/53 15285
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 1451 0 0 0 996 3 0 0 25 0 1 0 481539771 7770112 1423 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1897 1423 603 41 0 1856 0
vsize: 7588
[startup+20.0018 s]
Raw data (loadavg): 0.91 0.94 0.91 2/53 15285
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 1818 0 0 0 1995 4 0 0 25 0 1 0 481539771 9220096 1790 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2251 1790 603 41 0 2210 0
vsize: 9004
[startup+30.0036 s]
Raw data (loadavg): 0.93 0.94 0.91 2/53 15285
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2004 0 0 0 2994 5 0 0 25 0 1 0 481539771 10006528 1976 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2443 1976 603 41 0 2402 0
vsize: 9772
[startup+40.0043 s]
Raw data (loadavg): 0.94 0.95 0.91 2/53 15285
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2153 0 0 0 3994 6 0 0 25 0 1 0 481539771 10678272 2125 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2607 2125 603 41 0 2566 0
vsize: 10428
[startup+50.0048 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 15285
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2268 0 0 0 4993 6 0 0 25 0 1 0 481539771 11206656 2240 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2736 2240 603 41 0 2695 0
vsize: 10944
[startup+60.0056 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2288 0 0 0 5992 7 0 0 25 0 1 0 481539771 11341824 2260 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2769 2260 603 41 0 2728 0
vsize: 11076
[startup+70.0063 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2376 0 0 0 6992 7 0 0 25 0 1 0 481539771 11603968 2348 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2833 2348 603 41 0 2792 0
vsize: 11332
[startup+80.0082 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2392 0 0 0 7993 7 0 0 25 0 1 0 481539771 11763712 2364 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2872 2364 603 41 0 2831 0
vsize: 11488
[startup+90.0089 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2399 0 0 0 8993 7 0 0 25 0 1 0 481539771 11763712 2371 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2872 2371 603 41 0 2831 0
vsize: 11488
[startup+100.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2413 0 0 0 9993 7 0 0 25 0 1 0 481539771 11763712 2385 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2872 2385 603 41 0 2831 0
vsize: 11488
[startup+110.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2428 0 0 0 10993 7 0 0 25 0 1 0 481539771 11911168 2400 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2908 2400 603 41 0 2867 0
vsize: 11632
[startup+120.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2431 0 0 0 11993 7 0 0 25 0 1 0 481539771 11911168 2403 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2908 2403 603 41 0 2867 0
vsize: 11632
[startup+130.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2519 0 0 0 12992 7 0 0 25 0 1 0 481539771 12304384 2491 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3004 2491 603 41 0 2963 0
vsize: 12016
[startup+140.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2597 0 0 0 13992 8 0 0 25 0 1 0 481539771 12582912 2569 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3072 2569 603 41 0 3031 0
vsize: 12288
[startup+150.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2620 0 0 0 14993 8 0 0 25 0 1 0 481539771 12730368 2592 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3108 2592 603 41 0 3067 0
vsize: 12432
[startup+160.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2692 0 0 0 15992 8 0 0 25 0 1 0 481539771 12992512 2664 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3172 2664 603 41 0 3131 0
vsize: 12688
[startup+170.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2697 0 0 0 16993 8 0 0 25 0 1 0 481539771 12992512 2669 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3172 2669 603 41 0 3131 0
vsize: 12688
[startup+180.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2724 0 0 0 17992 9 0 0 25 0 1 0 481539771 13127680 2696 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3205 2696 603 41 0 3164 0
vsize: 12820
[startup+190.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2814 0 0 0 18992 9 0 0 25 0 1 0 481539771 13533184 2786 4294967295 134512640 134672761 3221224576 3221223752 134559668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3304 2786 603 41 0 3263 0
vsize: 13216
[startup+200.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2817 0 0 0 19992 9 0 0 25 0 1 0 481539771 13533184 2789 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3304 2789 603 41 0 3263 0
vsize: 13216
[startup+210.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2827 0 0 0 20992 9 0 0 25 0 1 0 481539771 13533184 2799 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3304 2799 603 41 0 3263 0
vsize: 13216
[startup+220.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2827 0 0 0 21993 9 0 0 25 0 1 0 481539771 13533184 2799 4294967295 134512640 134672761 3221224576 3221223760 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3304 2799 603 41 0 3263 0
vsize: 13216
[startup+230.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2839 0 0 0 22993 9 0 0 25 0 1 0 481539771 13533184 2811 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3304 2811 603 41 0 3263 0
vsize: 13216
[startup+240.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2850 0 0 0 23993 9 0 0 25 0 1 0 481539771 13688832 2822 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3342 2822 603 41 0 3301 0
vsize: 13368
[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2854 0 0 0 24993 9 0 0 25 0 1 0 481539771 13688832 2826 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3342 2826 603 41 0 3301 0
vsize: 13368
[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2857 0 0 0 25993 9 0 0 25 0 1 0 481539771 13688832 2829 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3342 2829 603 41 0 3301 0
vsize: 13368
[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2857 0 0 0 26993 9 0 0 25 0 1 0 481539771 13688832 2829 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3342 2829 603 41 0 3301 0
vsize: 13368
[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2857 0 0 0 27992 10 0 0 25 0 1 0 481539771 13688832 2829 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3342 2829 603 41 0 3301 0
vsize: 13368
[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2932 0 0 0 28992 10 0 0 25 0 1 0 481539771 13950976 2904 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3406 2904 603 41 0 3365 0
vsize: 13624
[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2976 0 0 0 29992 10 0 0 25 0 1 0 481539771 14225408 2948 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3473 2948 603 41 0 3432 0
vsize: 13892
[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2977 0 0 0 30993 10 0 0 25 0 1 0 481539771 14225408 2949 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3473 2949 603 41 0 3432 0
vsize: 13892
[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2991 0 0 0 31993 10 0 0 25 0 1 0 481539771 14225408 2963 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3473 2963 603 41 0 3432 0
vsize: 13892
[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 2991 0 0 0 32993 10 0 0 25 0 1 0 481539771 14225408 2963 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3473 2963 603 41 0 3432 0
vsize: 13892
[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15287
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3002 0 0 0 33994 10 0 0 25 0 1 0 481539771 14389248 2974 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3513 2974 603 41 0 3472 0
vsize: 14052
[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3002 0 0 0 34994 10 0 0 25 0 1 0 481539771 14389248 2974 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3513 2974 603 41 0 3472 0
vsize: 14052
[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3002 0 0 0 35994 10 0 0 25 0 1 0 481539771 14389248 2974 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3513 2974 603 41 0 3472 0
vsize: 14052
[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3002 0 0 0 36994 10 0 0 25 0 1 0 481539771 14389248 2974 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3513 2974 603 41 0 3472 0
vsize: 14052
[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3002 0 0 0 37994 10 0 0 25 0 1 0 481539771 14389248 2974 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3513 2974 603 41 0 3472 0
vsize: 14052
[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3002 0 0 0 38995 10 0 0 25 0 1 0 481539771 14389248 2974 4294967295 134512640 134672761 3221224576 3221223744 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3513 2974 603 41 0 3472 0
vsize: 14052
[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3002 0 0 0 39995 10 0 0 25 0 1 0 481539771 14389248 2974 4294967295 134512640 134672761 3221224576 3221223680 134559814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3513 2974 603 41 0 3472 0
vsize: 14052
[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3016 0 0 0 40995 10 0 0 25 0 1 0 481539771 14389248 2988 4294967295 134512640 134672761 3221224576 3221223728 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3513 2988 603 41 0 3472 0
vsize: 14052
[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3016 0 0 0 41994 11 0 0 25 0 1 0 481539771 14389248 2988 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3513 2988 603 41 0 3472 0
vsize: 14052
[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3169 0 0 0 42992 12 0 0 25 0 1 0 481539771 15048704 3141 4294967295 134512640 134672761 3221224576 3221223760 134559489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3674 3141 603 41 0 3633 0
vsize: 14696
[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3339 0 0 0 43992 13 0 0 25 0 1 0 481539771 15716352 3311 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3837 3311 603 41 0 3796 0
vsize: 15348
[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3344 0 0 0 44992 13 0 0 25 0 1 0 481539771 15716352 3316 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3837 3316 603 41 0 3796 0
vsize: 15348
[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3350 0 0 0 45992 13 0 0 25 0 1 0 481539771 15716352 3322 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3837 3322 603 41 0 3796 0
vsize: 15348
[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3360 0 0 0 46992 13 0 0 25 0 1 0 481539771 15847424 3332 4294967295 134512640 134672761 3221224576 3221223576 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3332 603 41 0 3828 0
vsize: 15476
[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3360 0 0 0 47993 13 0 0 25 0 1 0 481539771 15847424 3332 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3332 603 41 0 3828 0
vsize: 15476
[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3367 0 0 0 48993 13 0 0 25 0 1 0 481539771 15847424 3339 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3339 603 41 0 3828 0
vsize: 15476
[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3380 0 0 0 49993 13 0 0 25 0 1 0 481539771 15847424 3352 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3352 603 41 0 3828 0
vsize: 15476
[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3380 0 0 0 50993 13 0 0 25 0 1 0 481539771 15847424 3352 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3352 603 41 0 3828 0
vsize: 15476
[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3380 0 0 0 51994 13 0 0 25 0 1 0 481539771 15847424 3352 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3352 603 41 0 3828 0
vsize: 15476
[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3382 0 0 0 52994 13 0 0 25 0 1 0 481539771 15847424 3354 4294967295 134512640 134672761 3221224576 3221223744 134561701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3354 603 41 0 3828 0
vsize: 15476
[startup+540.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3388 0 0 0 53994 13 0 0 25 0 1 0 481539771 16007168 3360 4294967295 134512640 134672761 3221224576 3221223760 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3360 603 41 0 3867 0
vsize: 15632
[startup+550.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3388 0 0 0 54994 13 0 0 25 0 1 0 481539771 16007168 3360 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3360 603 41 0 3867 0
vsize: 15632
[startup+560.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3393 0 0 0 55995 13 0 0 25 0 1 0 481539771 16007168 3365 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3365 603 41 0 3867 0
vsize: 15632
[startup+570.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3393 0 0 0 56995 13 0 0 25 0 1 0 481539771 16007168 3365 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3365 603 41 0 3867 0
vsize: 15632
[startup+580.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3407 0 0 0 57995 13 0 0 25 0 1 0 481539771 16007168 3379 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3379 603 41 0 3867 0
vsize: 15632
[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3410 0 0 0 58995 13 0 0 25 0 1 0 481539771 16007168 3382 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3382 603 41 0 3867 0
vsize: 15632
[startup+600.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3410 0 0 0 59996 13 0 0 25 0 1 0 481539771 16007168 3382 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3382 603 41 0 3867 0
vsize: 15632
[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3410 0 0 0 60996 13 0 0 25 0 1 0 481539771 16007168 3382 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3382 603 41 0 3867 0
vsize: 15632
[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3410 0 0 0 61996 13 0 0 25 0 1 0 481539771 16007168 3382 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3908 3382 603 41 0 3867 0
vsize: 15632
[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3410 0 0 0 62996 13 0 0 25 0 1 0 481539771 16007168 3382 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3382 603 41 0 3867 0
vsize: 15632
[startup+640.058 s]
Raw data (loadavg): 1.07 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3410 0 0 0 63996 13 0 0 25 0 1 0 481539771 16007168 3382 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3908 3382 603 41 0 3867 0
vsize: 15632
[startup+650.059 s]
Raw data (loadavg): 1.06 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3446 0 0 0 64996 13 0 0 25 0 1 0 481539771 16285696 3418 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3976 3418 603 41 0 3935 0
vsize: 15904
[startup+660.059 s]
Raw data (loadavg): 1.05 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3449 0 0 0 65996 13 0 0 25 0 1 0 481539771 16285696 3421 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3976 3421 603 41 0 3935 0
vsize: 15904
[startup+670.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3449 0 0 0 66997 13 0 0 25 0 1 0 481539771 16285696 3421 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3976 3421 603 41 0 3935 0
vsize: 15904
[startup+680.061 s]
Raw data (loadavg): 1.04 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3731 0 0 0 67996 14 0 0 25 0 1 0 481539771 17354752 3703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4237 3703 603 41 0 4196 0
vsize: 16948
[startup+690.062 s]
Raw data (loadavg): 1.03 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3939 0 0 0 68995 15 0 0 25 0 1 0 481539771 18292736 3911 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3911 603 41 0 4425 0
vsize: 17864
[startup+700.063 s]
Raw data (loadavg): 1.03 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3942 0 0 0 69995 15 0 0 25 0 1 0 481539771 18292736 3914 4294967295 134512640 134672761 3221224576 3221223680 134560322 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3914 603 41 0 4425 0
vsize: 17864
[startup+710.063 s]
Raw data (loadavg): 1.02 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3943 0 0 0 70996 15 0 0 25 0 1 0 481539771 18292736 3915 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3915 603 41 0 4425 0
vsize: 17864
[startup+720.064 s]
Raw data (loadavg): 1.02 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 71995 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+730.08 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 72996 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+740.081 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 73997 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+750.081 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 74997 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+760.082 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 75998 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+770.083 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 76998 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223680 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+780.084 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 77998 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+790.085 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 78997 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+800.086 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 79998 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+810.087 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 80998 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+820.088 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 81998 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+830.088 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 82998 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+840.089 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 83999 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+850.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 84999 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+860.091 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 85999 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+870.091 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 86999 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+880.092 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 87999 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+890.093 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 88999 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+900.094 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 89999 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+910.094 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 91000 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+920.095 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3950 0 0 0 92000 16 0 0 25 0 1 0 481539771 18292736 3922 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3922 603 41 0 4425 0
vsize: 17864
[startup+930.096 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3952 0 0 0 93000 16 0 0 25 0 1 0 481539771 18292736 3924 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3924 603 41 0 4425 0
vsize: 17864
[startup+940.097 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3952 0 0 0 94000 16 0 0 25 0 1 0 481539771 18292736 3924 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3924 603 41 0 4425 0
vsize: 17864
[startup+950.097 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3952 0 0 0 95001 16 0 0 25 0 1 0 481539771 18292736 3924 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3924 603 41 0 4425 0
vsize: 17864
[startup+960.098 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3952 0 0 0 96001 16 0 0 25 0 1 0 481539771 18292736 3924 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3924 603 41 0 4425 0
vsize: 17864
[startup+970.099 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 97001 16 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+980.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 98001 16 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+990.101 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 99002 16 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1000.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 100002 16 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223632 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1010.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 101002 16 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1020.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 102001 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1030.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 103002 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1040.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 104002 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1050.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 105002 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1060.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 106002 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1070.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 107003 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223712 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1080.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 108003 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134564451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1090.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 109003 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1100.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 110003 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1110.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 111004 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1120.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 112004 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1130.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 113004 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1140.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 114004 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223680 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1150.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 115004 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223712 134560632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1160.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 116004 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1170.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 117004 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1180.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 118005 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1190.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3953 0 0 0 119005 17 0 0 25 0 1 0 481539771 18292736 3925 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4466 3925 603 41 0 4425 0
vsize: 17864
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15289
Raw data (stat): 15285 (minisat+) R 15284 7987 7986 0 -1 0 3987 0 0 0 120005 17 0 0 25 0 1 0 481539771 18427904 3959 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4499 3959 603 41 0 4458 0
vsize: 17996
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 15289
Raw data (stat): 15285 (minisat+) Z 15284 7987 7986 0 -1 12 3990 0 0 0 120005 18 0 0 25 0 1 0 481539771 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.13
CPU time (s): 1200.24
CPU user time (s): 1200.06
CPU system time (s): 0.184971
CPU usage (%): 100.009
Max. virtual memory (Kb): 17996
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####