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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-4.opb
MD5SUM	e3892e1941a878802a8ccbbd36201a02
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-27
Optimality of the best value was proved	NO
Number of terms in the objective function	595
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	595
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	595
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	27842
Number of constraints which are clauses	27842
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	2
Trace number 30500

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-05-25 17:14:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21904 boxname=wulflinc19 idbench=322 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  e3892e1941a878802a8ccbbd36201a02  /oldhome/oroussel/tmp/wulflinc19/normalized-frb35-17-4.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-frb35-17-4.opb
IDLAUNCH: 21904
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        423576 kB
Buffers:         35660 kB
Cached:         548520 kB
SwapCached:        416 kB
Active:          60712 kB
Inactive:       525732 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        423324 kB
SwapTotal:     2097892 kB
SwapFree:      2096804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            18940 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 17:34:51 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 21904 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27842 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 |   27842    55684 |    9280       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -26[0m
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56133   122130 |   18711       0        0     nan |  0.000 % |
c |       100 |   55674   121173 |   20582      85      517     6.1 |  1.318 % |
c |       250 |   55337   120462 |   22640     201     1671     8.3 |  2.285 % |
c |       475 |   53886   117283 |   24904     355     3653    10.3 |  6.749 % |
c |       813 |   52308   113815 |   27394     620     7389    11.9 | 11.632 % |
c |      1319 |   49554   107621 |   30134     953    11439    12.0 | 20.509 % |
c |      2078 |   46551   100685 |   33147    1523    18456    12.1 | 30.615 % |
c |      3217 |   42835    92193 |   36462    2389    34261    14.3 | 42.639 % |
c ==============================================================================
c [1mFound solution: -28[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3273 |   42557    91588 |   14185    2416    34615    14.3 | 42.639 % |
c |      3373 |   42214    90786 |   15603    2489    35595    14.3 | 45.030 % |
c |      3523 |   41934    90117 |   17163    2594    37012    14.3 | 45.977 % |
c |      3748 |   41522    89143 |   18880    2783    39915    14.3 | 47.372 % |
c |      4086 |   40623    87001 |   20768    2975    42882    14.4 | 50.494 % |
c |      4593 |   39615    84625 |   22845    3304    51715    15.7 | 53.972 % |
c |      5353 |   38103    81054 |   25129    3854    65467    17.0 | 59.168 % |
c |      6492 |   37040    78558 |   27642    4854    94566    19.5 | 62.852 % |
c ==============================================================================
c [1mFound solution: -29[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7236 |   36536    77417 |   12178    5459   115634    21.2 | 62.852 % |
c |      7336 |   36373    77022 |   13395    5525   117833    21.3 | 65.194 % |
c |      7486 |   36245    76711 |   14735    5659   121848    21.5 | 65.636 % |
c |      7712 |   35618    75194 |   16208    5758   121613    21.1 | 67.804 % |
c |      8049 |   35083    73909 |   17829    5937   129670    21.8 | 69.674 % |
c |      8555 |   35082    73906 |   19612    6440   149607    23.2 | 69.679 % |
c |      9314 |   34665    72910 |   21574    7108   172599    24.3 | 71.138 % |
c |     10454 |   34563    72672 |   23731    8226   223484    27.2 | 71.487 % |
c |     12162 |   34403    72291 |   26104    9826   305581    31.1 | 72.052 % |
c |     14725 |   33512    70136 |   28715   11797   413482    35.0 | 75.269 % |
c |     18569 |   32730    68273 |   31586   14907   673193    45.2 | 78.002 % |
c |     24336 |   32584    67918 |   34745   20503  1088479    53.1 | 78.521 % |
c ==============================================================================
c [1mFound solution: -30[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25008 |   32376    67375 |   10792   20807  1127008    54.2 | 78.521 % |
c |     25109 |   32333    67266 |   11871   20854  1131597    54.3 | 79.396 % |
c |     25259 |   32266    67098 |   13058   20933  1134331    54.2 | 79.653 % |
c |     25484 |   32266    67098 |   14364   21158  1153914    54.5 | 79.653 % |
c |     25824 |   32266    67098 |   15800   21498  1181497    55.0 | 79.653 % |
c ==============================================================================
c [1mFound solution: -32[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26069 |   32269    67111 |   10756   20959  1109301    52.9 | 79.653 % |
c |     26169 |   32220    66999 |   11831   21035  1113907    53.0 | 79.898 % |
c |     26319 |   32220    66999 |   13014   21185  1119388    52.8 | 79.898 % |
c |     26544 |   32174    66891 |   14316   21380  1132489    53.0 | 80.051 % |
c |     26881 |   32174    66891 |   15747   21717  1150097    53.0 | 80.051 % |
c |     27388 |   32126    66770 |   17322   22203  1170894    52.7 | 80.215 % |
c |     28148 |   32036    66557 |   19054   22829  1208152    52.9 | 80.527 % |
c |     29287 |   32036    66557 |   20960   23968  1254726    52.4 | 80.527 % |
c |     30995 |   32008    66487 |   23056   25554  1358136    53.1 | 80.634 % |
c |     33557 |   32008    66487 |   25362   28116  1511958    53.8 | 80.634 % |
c |     37401 |   32008    66487 |   27898   31960  1790963    56.0 | 80.634 % |
c |     43167 |   31963    66380 |   30688   37641  2179278    57.9 | 80.788 % |
c |     51816 |   31942    66327 |   33756   46095  2740539    59.5 | 80.865 % |
c |     64790 |   31936    66313 |   37132   23972  1287927    53.7 | 80.885 % |
c ==============================================================================
c [1mFound solution: -33[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83994 |   31772    65908 |   10590   43119  2704132    62.7 | 80.885 % |
c |     84094 |   31769    65901 |   11649   16788   764343    45.5 | 81.544 % |
c |     84245 |   31761    65883 |   12813   16934   773077    45.7 | 81.569 % |
c |     84470 |   31761    65883 |   14095   17159   787038    45.9 | 81.569 % |
c |     84807 |   31629    65553 |   15504   17469   799984    45.8 | 82.070 % |
c |     85314 |   31616    65520 |   17055   17970   827588    46.1 | 82.121 % |
c |     86073 |   31535    65323 |   18760   18695   873445    46.7 | 82.407 % |
c |     87212 |   31529    65309 |   20636   19831   940958    47.4 | 82.428 % |
c |     88920 |   31523    65295 |   22700   21535  1039370    48.3 | 82.448 % |
c |     91482 |   31523    65295 |   24970   24097  1198465    49.7 | 82.448 % |
c |     95326 |   31486    65206 |   27467   27922  1432420    51.3 | 82.581 % |
c |    101092 |   31447    65117 |   30214   33656  1817647    54.0 | 82.708 % |
c |    109742 |   31438    65094 |   33235   42294  2206478    52.2 | 82.744 % |
c |    122717 |   31429    65073 |   36559   23198   776943    33.5 | 82.775 % |
c |    142179 |   31427    65069 |   40215   42658  1545047    36.2 | 82.780 % |
c |    171371 |   31424    65062 |   44237   32274  1209176    37.5 | 82.790 % |
c |    215161 |   31396    64996 |   48660   32992  1383853    41.9 | 82.887 % |
c |    280846 |   31348    64880 |   53526   51753  1853976    35.8 | 83.061 % |
c |    379372 |   31268    64690 |   58879   48632  1483738    30.5 | 83.337 % |
c ==============================================================================
c [1mFound solution: -34[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    387520 |   31254    64622 |   10418   56778  1800142    31.7 | 83.337 % |
c |    387621 |   31254    64622 |   11459   21874   574796    26.3 | 83.395 % |
c |    387771 |   31254    64622 |   12605   22024   579120    26.3 | 83.395 % |
c |    387996 |   31254    64622 |   13866   22249   585284    26.3 | 83.395 % |
c |    388334 |   31254    64622 |   15252   22587   595104    26.3 | 83.395 % |
c |    388840 |   31254    64622 |   16778   23093   611433    26.5 | 83.395 % |
c |    389599 |   31254    64622 |   18456   23852   651357    27.3 | 83.395 % |
c |    390738 |   31254    64622 |   20301   24991   708484    28.3 | 83.395 % |
c |    392446 |   31254    64622 |   22331   26699   784774    29.4 | 83.395 % |
c |    395008 |   31254    64622 |   24565   29261   882101    30.1 | 83.395 % |
c |    398852 |   31254    64622 |   27021   33105  1025751    31.0 | 83.395 % |
c |    404619 |   31237    64583 |   29723   38861  1224818    31.5 | 83.451 % |
c |    413269 |   31193    64477 |   32696   19145   554379    29.0 | 83.609 % |
c |    426243 |   31188    64466 |   35965   32115  1008537    31.4 | 83.625 % |
c |    445704 |   31188    64466 |   39562   51576  1732486    33.6 | 83.624 % |
c |    474896 |   31175    64437 |   43518   43794  1320198    30.1 | 83.665 % |
c |    518685 |   31066    64153 |   47870   45690  1182298    25.9 | 84.089 % |
c ==============================================================================
c [1mFound solution: -35[0m
c ---[   0]---> Sorter-cost:23198     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    565168 |   49180   106489 |   16393   38187  1077494    28.2 | 84.089 % |
c |    565268 |   49180   106489 |   18032   15309   289280    18.9 | 55.800 % |
c |    565418 |   49180   106489 |   19835   15459   294371    19.0 | 55.800 % |
c |    565643 |   49180   106489 |   21819   15684   302669    19.3 | 55.800 % |
c |    565980 |   49180   106489 |   24000   16021   312388    19.5 | 55.800 % |
c |    566490 |   49180   106489 |   26401   16531   329375    19.9 | 55.800 % |
c |    567250 |   49180   106489 |   29041   17291   353999    20.5 | 55.800 % |
c |    568389 |   49180   106489 |   31945   18430   386682    21.0 | 55.800 % |
c |    570097 |   49180   106489 |   35139   20138   435618    21.6 | 55.800 % |
c |    572659 |   49180   106489 |   38653   22700   507140    22.3 | 55.800 % |
c |    576504 |   49139   106407 |   42519   26544   621579    23.4 | 55.877 % |
c |    582270 |   49139   106407 |   46771   32310   777211    24.1 | 55.877 % |
c |    590919 |   49102   106333 |   51448   40958  1110939    27.1 | 55.940 % |
c |    603893 |   49102   106333 |   56593   53932  1518995    28.2 | 55.940 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 25483 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.98 2/54 25479
Raw data (stat): 25479 (runsolver) R 25478 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 840588845 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.94 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0019 s]
Raw data (loadavg): 0.95 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0024 s]
Raw data (loadavg): 0.97 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0036 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.005 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.007 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.007 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.008 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.009 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.009 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.009 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.01 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.01 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.011 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.011 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.012 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.013 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.013 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.013 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.014 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.014 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.015 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.015 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.017 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.017 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.017 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.018 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.018 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.019 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.02 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.02 s]
Raw data (loadavg): 0.99 0.98 0.98 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.02 s]
Raw data (loadavg): 1.07 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.021 s]
Raw data (loadavg): 1.06 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.021 s]
Raw data (loadavg): 1.05 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.021 s]
Raw data (loadavg): 1.04 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.021 s]
Raw data (loadavg): 1.04 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.022 s]
Raw data (loadavg): 1.03 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.022 s]
Raw data (loadavg): 1.03 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.022 s]
Raw data (loadavg): 1.02 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.023 s]
Raw data (loadavg): 1.02 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.023 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.024 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.024 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.025 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.025 s]
Raw data (loadavg): 1.01 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.025 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.025 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.025 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.025 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.027 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.027 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.027 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.027 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.027 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.026 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.027 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.027 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.029 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.029 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.029 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.029 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.029 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 1.00 1.00 0.99 1/53 25483
Raw data (stat): 25479 (minisat+_script) S 25478 10795 10794 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840588845 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.7
CPU time (s): 1229.85
CPU user time (s): 1229.44
CPU system time (s): 0.405938
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####