PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod008.opb
MD5SUM	fbdb3cf321a85412feefcaac30780520
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	307
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	22000
Number of bits of the biggest number in a constraint	15
Biggest sum of numbers in a constraint	1027256
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01584
Number of variables	319
Total number of constraints	325
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	319
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	231
Trace number 31896

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-05-27 06:42:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23282 boxname=wulflinc17 idbench=926 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fbdb3cf321a85412feefcaac30780520  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-mod008.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-mod008.opb
IDLAUNCH: 23282
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        810660 kB
Buffers:         33292 kB
Cached:         169576 kB
SwapCached:        520 kB
Active:          44744 kB
Inactive:       160316 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        810408 kB
SwapTotal:     2097892 kB
SwapFree:      2096560 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            13132 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 07:02:37 (client local time) WITH STATUS 152 IN 1229.98 SECONDS
stats: 23282 7 1229.98 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss
c ---[   8]---> BDD-cost:777098
c ---[   5]---> BDD-cost: 5719
c ---[   4]---> BDD-cost:24274
c ---[   2]---> BDD-cost:  478
c ---[   1]---> BDD-cost: 2553
c ---[   0]---> BDD-cost: 7307
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2386590  7171332 |  795530       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 2736[0m
c ---[   0]---> Sorter-cost:61665     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2537120  7522847 |  845706       0        0     nan |  0.000 % |
c |       103 | 2537120  7522847 |  930276     103     2421    23.5 |  0.001 % |
c |       254 | 2537120  7522847 | 1023304     254    12318    48.5 |  0.001 % |
c |       479 | 2537120  7522847 | 1125634     479    14776    30.8 |  0.001 % |
c |       816 | 2537120  7522847 | 1238198     816    25056    30.7 |  0.001 % |
c |      1323 | 2537120  7522847 | 1362017    1323    33177    25.1 |  0.001 % |
c |      2082 | 2537120  7522847 | 1498219    2082    68922    33.1 |  0.001 % |
c |      3221 | 2536930  7522420 | 1648041    3118    83012    26.6 |  0.007 % |
c |      4930 | 2536930  7522420 | 1812845    4827   117257    24.3 |  0.007 % |
c |      7492 | 2536930  7522420 | 1994130    7389   151151    20.5 |  0.007 % |
c |     11337 | 2536930  7522420 | 2193543   11234   199352    17.7 |  0.007 % |
c |     17103 | 2536930  7522420 | 2412897   17000   291674    17.2 |  0.007 % |
c ==============================================================================
c [1mFound solution: 2359[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19729 | 2537972  7525048 |  845990   19626   321546    16.4 |  0.007 % |
c |     19829 | 2537972  7525048 |  930589   19726   322143    16.3 |  0.007 % |
c |     19979 | 2537972  7525048 | 1023647   19876   323106    16.3 |  0.007 % |
c |     20207 | 2537972  7525048 | 1126012   20104   327986    16.3 |  0.007 % |
c |     20544 | 2537972  7525048 | 1238613   20441   336109    16.4 |  0.007 % |
c |     21050 | 2537972  7525048 | 1362475   20947   347397    16.6 |  0.007 % |
c |     21812 | 2537972  7525048 | 1498722   21709   369904    17.0 |  0.007 % |
c |     22952 | 2537972  7525048 | 1648595   22849   409663    17.9 |  0.007 % |
c |     24661 | 2537972  7525048 | 1813454   24558   456229    18.6 |  0.007 % |
c |     27223 | 2537972  7525048 | 1994800   27120   543521    20.0 |  0.007 % |
c ==============================================================================
c [1mFound solution: 2330[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28130 | 2537982  7525075 |  845994   28027   571748    20.4 |  0.007 % |
c ==============================================================================
c [1mFound solution: 2268[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28200 | 2538600  7526620 |  846200   28097   576554    20.5 |  0.007 % |
c |     28300 | 2538600  7526620 |  930820   28197   577583    20.5 |  0.007 % |
c |     28452 | 2538600  7526620 | 1023902   28349   580020    20.5 |  0.007 % |
c |     28678 | 2538600  7526620 | 1126292   28575   583723    20.4 |  0.007 % |
c |     29015 | 2538600  7526620 | 1238921   28912   589799    20.4 |  0.007 % |
c ==============================================================================
c [1mFound solution: 1774[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29389 | 2538666  7526861 |  846222   29286   596861    20.4 |  0.007 % |
c |     29490 | 2538666  7526861 |  930844   29387   597305    20.3 |  0.008 % |
c |     29640 | 2538666  7526861 | 1023928   29537   601370    20.4 |  0.008 % |
c |     29866 | 2538666  7526861 | 1126321   29763   605027    20.3 |  0.008 % |
c |     30203 | 2538666  7526861 | 1238953   30100   609517    20.2 |  0.008 % |
c |     30710 | 2538666  7526861 | 1362848   30607   620907    20.3 |  0.008 % |
c |     31470 | 2538646  7526816 | 1499133   31360   634128    20.2 |  0.008 % |
c ==============================================================================
c [1mFound solution: 1760[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31804 | 2538658  7526847 |  846219   31694   644703    20.3 |  0.008 % |
c |     31904 | 2538658  7526847 |  930840   31794   653680    20.6 |  0.008 % |
c |     32054 | 2538658  7526847 | 1023924   31944   655505    20.5 |  0.008 % |
c |     32279 | 2538658  7526847 | 1126317   32169   657038    20.4 |  0.008 % |
c |     32616 | 2538658  7526847 | 1238949   32506   660050    20.3 |  0.008 % |
c |     33124 | 2538658  7526847 | 1362844   33014   665670    20.2 |  0.008 % |
c |     33883 | 2538658  7526847 | 1499128   33773   682971    20.2 |  0.008 % |
c |     35022 | 2538658  7526847 | 1649041   34912   697748    20.0 |  0.008 % |
c |     36730 | 2538658  7526847 | 1813945   36620   727400    19.9 |  0.008 % |
c |     39292 | 2538658  7526847 | 1995340   39182   812482    20.7 |  0.008 % |
c |     43136 | 2538658  7526847 | 2194874   43026   977964    22.7 |  0.008 % |
c ==============================================================================
c [1mFound solution: 1519[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43236 | 2538693  7526935 |  846231   43126   979511    22.7 |  0.008 % |
c |     43336 | 2538693  7526935 |  930854   43226   986637    22.8 |  0.008 % |
c ==============================================================================
c [1mFound solution: 936[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43345 | 2538740  7527044 |  846246   43235   987190    22.8 |  0.008 % |
c |     43445 | 2538740  7527044 |  930870   43335   994189    22.9 |  0.008 % |
c |     43595 | 2538740  7527044 | 1023957   43485   998827    23.0 |  0.008 % |
c ==============================================================================
c [1mFound solution: 814[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43628 | 2538769  7527114 |  846256   43518   999616    23.0 |  0.008 % |
c ==============================================================================
c [1mFound solution: 804[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43685 | 2538780  7527143 |  846260   43575  1001178    23.0 |  0.008 % |
c |     43785 | 2538780  7527143 |  930886   43675  1028207    23.5 |  0.009 % |
c |     43935 | 2538780  7527143 | 1023974   43825  1030963    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 739[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43968 | 2538786  7527159 |  846262   43858  1031377    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 674[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43980 | 2538805  7527207 |  846268   43870  1031641    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 654[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43987 | 2538810  7527222 |  846270   43877  1031873    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 649[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44003 | 2538817  7527238 |  846272   43893  1032613    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 496[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44021 | 2538840  7527293 |  846280   43911  1033912    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 489[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44023 | 2538846  7527307 |  846282   43913  1034858    23.6 |  0.009 % |
c |     44124 | 2538846  7527307 |  930910   44014  1046891    23.8 |  0.009 % |
c |     44274 | 2538846  7527307 | 1024001   44164  1052996    23.8 |  0.009 % |
c |     44503 | 2538846  7527307 | 1126401   44393  1105198    24.9 |  0.009 % |
c |     44841 | 2538846  7527307 | 1239041   44731  1207157    27.0 |  0.009 % |
c |     45349 | 2538846  7527307 | 1362945   45239  1241301    27.4 |  0.009 % |
c |     46108 | 2538846  7527307 | 1499240   45998  1292536    28.1 |  0.009 % |
c |     47248 | 2538846  7527307 | 1649164   47138  1354106    28.7 |  0.009 % |
c |     48956 | 2538846  7527307 | 1814080   48846  1777892    36.4 |  0.009 % |
c |     51519 | 2538846  7527307 | 1995488   51409  1945080    37.8 |  0.009 % |
c |     55363 | 2538693  7526960 | 2195037   55100  2139380    38.8 |  0.014 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  4552 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.91 0.95 0.90 2/54 4548
Raw data (stat): 4548 (runsolver) R 4547 7475 7474 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854096928 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0011 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4552
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 4587
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 4605
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 4605
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 4605
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 4605
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 4605
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 4605
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 4605
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 4607
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 4607
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 4607
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 4607
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 4607
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 4607
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 4607
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.86 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 4607
Raw data (stat): 4548 (minisat+_script) S 4547 7475 7474 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854096928 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.86
CPU time (s): 1229.98
CPU user time (s): 1227.6
CPU system time (s): 2.38264
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####