PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare1_1.opb
MD5SUM	f88781e3d6e9a5487d13eaa213c27b55
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4272
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	6291450
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	6291450
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	205
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	105
Trace number 14699

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 00:51:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19484 boxname=wulflinc3 idbench=1499 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f88781e3d6e9a5487d13eaa213c27b55  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-markshare1_1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-markshare1_1.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-markshare1_1.opb
IDLAUNCH: 19484
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 2
cpu MHz		: 451.190
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:        304360 kB
Buffers:         34356 kB
Cached:         672572 kB
SwapCached:          0 kB
Active:         200028 kB
Inactive:       509640 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        304108 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6840 kB
Slab:            15004 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:11:17 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 19484 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  15]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  14]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  13]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  12]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  10]---> Adder-cost: 554   maxlim: 438520   bits: 20/19
c ---[   8]---> Adder-cost: 562   maxlim: 469716   bits: 20/19
c ---[   6]---> Adder-cost: 644   maxlim: 485238   bits: 20/19
c ---[   4]---> Adder-cost: 446   maxlim: 425237   bits: 20/19
c ---[   2]---> Adder-cost: 494   maxlim: 433357   bits: 20/19
c ---[   0]---> Adder-cost: 474   maxlim: 432725   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21925    78014 |    7308       0        0     nan |  0.000 % |
c |       103 |   21925    78014 |    8038     103      334     3.2 |  7.810 % |
c |       254 |   21909    77962 |    8842     252     1483     5.9 |  7.866 % |
c ==============================================================================
c [1mFound solution: 832295[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 180   maxlim: 740563   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       285 |   23111    82302 |    7703     283     1798     6.4 |  7.866 % |
c ==============================================================================
c [1mFound solution: 446279[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1126579   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       329 |   23110    82301 |    7703     327     2131     6.5 |  7.866 % |
c |       431 |   23110    82301 |    8473     429     2803     6.5 |  8.011 % |
c ==============================================================================
c [1mFound solution: 440296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1132562   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       520 |   23127    82413 |    7709     518     3811     7.4 |  8.011 % |
c |       621 |   23119    82387 |    8479     618     6563    10.6 |  8.149 % |
c |       771 |   23111    82361 |    9327     767     7633    10.0 |  8.176 % |
c |       996 |   23095    82309 |   10260     990    10706    10.8 |  8.228 % |
c |      1334 |   23087    82283 |   11286    1327    22488    16.9 |  8.254 % |
c |      1840 |   23087    82283 |   12415    1833    66611    36.3 |  8.254 % |
c ==============================================================================
c [1mFound solution: 392218[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1180640   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2108 |   23102    82403 |    7700    2101    80122    38.1 |  8.254 % |
c ==============================================================================
c [1mFound solution: 374514[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1198344   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2159 |   23113    82487 |    7704    2152    81699    38.0 |  8.254 % |
c |      2260 |   23113    82487 |    8474    2253    86283    38.3 |  8.539 % |
c |      2410 |   23113    82487 |    9321    2403    90943    37.8 |  8.539 % |
c |      2635 |   23113    82487 |   10254    2628    93899    35.7 |  8.539 % |
c |      2973 |   23113    82487 |   11279    2966   116813    39.4 |  8.539 % |
c |      3479 |   23113    82487 |   12407    3472   185837    53.5 |  8.539 % |
c ==============================================================================
c [1mFound solution: 248774[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1324084   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3609 |   23102    82288 |    7700    3601   189514    52.6 |  8.539 % |
c |      3709 |   23085    82229 |    8470    3699   195078    52.7 |  8.825 % |
c ==============================================================================
c [1mFound solution: 245760[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1327098   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3806 |   23100    82382 |    7700    3796   201185    53.0 |  8.825 % |
c |      3906 |   23093    82359 |    8470    3893   205140    52.7 |  9.103 % |
c |      4057 |   23093    82359 |    9317    4044   208409    51.5 |  9.103 % |
c |      4282 |   23084    82330 |   10248    4266   216255    50.7 |  9.155 % |
c |      4620 |   23076    82304 |   11273    4603   223168    48.5 |  9.181 % |
c |      5127 |   23076    82304 |   12400    5110   240199    47.0 |  9.181 % |
c |      5887 |   23068    82278 |   13641    5869   283020    48.2 |  9.207 % |
c ==============================================================================
c [1mFound solution: 125384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4   maxlim: 661042   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6115 |   23009    82133 |    7669    6075   285962    47.1 |  9.207 % |
c |      6217 |   23009    82133 |    8435    6177   291616    47.2 |  9.710 % |
c |      6368 |   23009    82133 |    9279    6328   292938    46.3 |  9.710 % |
c |      6593 |   22991    82069 |   10207    6518   286650    44.0 |  9.762 % |
c |      6931 |   22982    82040 |   11228    6855   294294    42.9 |  9.814 % |
c |      7437 |   22940    81733 |   12351    7357   303463    41.2 |  9.943 % |
c |      8196 |   22940    81733 |   13586    8116   352971    43.5 |  9.943 % |
c |      9335 |   22940    81733 |   14944    9255   423628    45.8 |  9.943 % |
c |     11044 |   22932    81707 |   16439   10963   510044    46.5 |  9.969 % |
c |     13606 |   22932    81707 |   18083   13525   628448    46.5 |  9.969 % |
c |     17452 |   22932    81707 |   19891   17371   797096    45.9 |  9.969 % |
c |     23219 |   22932    81707 |   21880   12238   737148    60.2 |  9.969 % |
c |     31868 |   22932    81707 |   24068   20887  1355438    64.9 |  9.969 % |
c |     44842 |   22932    81707 |   26475   21131  1061404    50.2 |  9.969 % |
c ==============================================================================
c [1mFound solution: 109668[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 676758   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62575 |   22939    81796 |    7646   24799  1149196    46.3 |  9.969 % |
c |     62675 |   22939    81796 |    8410    6300   263206    41.8 | 10.188 % |
c |     62826 |   22939    81796 |    9251    6451   267181    41.4 | 10.188 % |
c |     63053 |   22939    81796 |   10176    6678   272405    40.8 | 10.188 % |
c |     63391 |   22939    81796 |   11194    7016   277320    39.5 | 10.188 % |
c |     63898 |   22939    81796 |   12313    7523   291371    38.7 | 10.188 % |
c |     64658 |   22939    81796 |   13545    8283   325699    39.3 | 10.188 % |
c |     65797 |   22939    81796 |   14899    9422   356224    37.8 | 10.188 % |
c ==============================================================================
c [1mFound solution: 89258[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 697168   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67010 |   22954    81887 |    7651   10635   405305    38.1 | 10.188 % |
c |     67113 |   22954    81887 |    8416    5421   141392    26.1 | 10.340 % |
c |     67266 |   22954    81887 |    9257    5574   144938    26.0 | 10.340 % |
c |     67492 |   22954    81887 |   10183    5800   151207    26.1 | 10.340 % |
c |     67829 |   22954    81887 |   11201    6137   155962    25.4 | 10.340 % |
c |     68335 |   22954    81887 |   12322    6643   165870    25.0 | 10.340 % |
c |     69094 |   22954    81887 |   13554    7402   185894    25.1 | 10.340 % |
c |     70233 |   22954    81887 |   14909    8541   228447    26.7 | 10.340 % |
c |     71941 |   22954    81887 |   16400   10249   291543    28.4 | 10.340 % |
c |     74503 |   22954    81887 |   18040   12811   384438    30.0 | 10.340 % |
c |     78348 |   22954    81887 |   19844   16656   831726    49.9 | 10.340 % |
c |     84114 |   22954    81887 |   21829   12030   752105    62.5 | 10.340 % |
c |     92763 |   22954    81887 |   24012   20679  1198160    57.9 | 10.340 % |
c |    105737 |   22954    81887 |   26413   21131   942456    44.6 | 10.340 % |
c |    125200 |   22954    81887 |   29054   25743  1811506    70.4 | 10.340 % |
c ==============================================================================
c [1mFound solution: 82436[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 703990   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    148131 |   22974    82036 |    7658   15604   872396    55.9 | 10.340 % |
c |    148231 |   22974    82036 |    8423    7902   356220    45.1 | 10.568 % |
c |    148382 |   22974    82036 |    9266    8053   361725    44.9 | 10.568 % |
c |    148608 |   22974    82036 |   10192    8279   367170    44.3 | 10.568 % |
c |    148946 |   22974    82036 |   11212    8617   378275    43.9 | 10.568 % |
c |    149453 |   22974    82036 |   12333    9124   395162    43.3 | 10.568 % |
c |    150212 |   22974    82036 |   13566    9883   420572    42.6 | 10.568 % |
c |    151351 |   22974    82036 |   14923   11022   445058    40.4 | 10.568 % |
c |    153059 |   22974    82036 |   16415   12730   506906    39.8 | 10.568 % |
c |    155624 |   22974    82036 |   18057   15295   602253    39.4 | 10.568 % |
c |    159469 |   22974    82036 |   19862    9694   334701    34.5 | 10.568 % |
c |    165235 |   22974    82036 |   21849   15460   954337    61.7 | 10.568 % |
c |    173886 |   22974    82036 |   24034   12136   947473    78.1 | 10.568 % |
c |    186862 |   22974    82036 |   26437   25112  1736947    69.2 | 10.568 % |
c |    206323 |   22974    82036 |   29081   15927   696259    43.7 | 10.568 % |
c |    235516 |   22974    82036 |   31989   26722  1778021    66.5 | 10.568 % |
c |    279305 |   22974    82036 |   35188   32131  1746496    54.4 | 10.568 % |
c |    344989 |   22974    82036 |   38707   30633  3372784   110.1 | 10.568 % |
c |    443517 |   22974    82036 |   42577   27965  1908736    68.3 | 10.568 % |
c |    591306 |   22974    82036 |   46835   36313  1912728    52.7 | 10.568 % |
#### 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.97 1.01 0.95 2/54 2765
Raw data (stat): 2765 (runsolver) R 2764 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482671571 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0009 s]
Raw data (loadavg): 0.97 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 1491 0 0 0 995 3 0 0 25 0 1 0 482671571 7737344 1469 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1889 1469 603 41 0 1848 0
vsize: 7556
[startup+20.0017 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2073 0 0 0 1993 5 0 0 25 0 1 0 482671571 10162176 2051 4294967295 134512640 134672761 3221224528 3221223712 134558916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2481 2051 603 41 0 2440 0
vsize: 9924
[startup+30.002 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2173 0 0 0 2992 6 0 0 25 0 1 0 482671571 10559488 2151 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2578 2151 603 41 0 2537 0
vsize: 10312
[startup+40.0024 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2597 0 0 0 3989 9 0 0 25 0 1 0 482671571 12292096 2575 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3001 2575 603 41 0 2960 0
vsize: 12004
[startup+50.0022 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2599 0 0 0 4989 9 0 0 25 0 1 0 482671571 12292096 2577 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3001 2577 603 41 0 2960 0
vsize: 12004
[startup+60.0035 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2599 0 0 0 5989 9 0 0 25 0 1 0 482671571 12292096 2577 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3001 2577 603 41 0 2960 0
vsize: 12004
[startup+70.0039 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2600 0 0 0 6988 10 0 0 25 0 1 0 482671571 12292096 2578 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3001 2578 603 41 0 2960 0
vsize: 12004
[startup+80.0037 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2600 0 0 0 7988 10 0 0 25 0 1 0 482671571 12292096 2578 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3001 2578 603 41 0 2960 0
vsize: 12004
[startup+90.004 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2600 0 0 0 8988 10 0 0 25 0 1 0 482671571 12292096 2578 4294967295 134512640 134672761 3221224528 3221223632 134555093 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3001 2578 603 41 0 2960 0
vsize: 12004
[startup+100.003 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2600 0 0 0 9987 11 0 0 25 0 1 0 482671571 12292096 2578 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3001 2578 603 41 0 2960 0
vsize: 12004
[startup+110.011 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 2611 0 0 0 10987 12 0 0 25 0 1 0 482671571 12292096 2589 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3001 2589 603 41 0 2960 0
vsize: 12004
[startup+120.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3240 0 0 0 11985 14 0 0 25 0 1 0 482671571 14831616 3218 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3621 3218 603 41 0 3580 0
vsize: 14484
[startup+130.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3410 0 0 0 12984 15 0 0 25 0 1 0 482671571 15634432 3388 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3817 3388 603 41 0 3776 0
vsize: 15268
[startup+140.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3410 0 0 0 13983 15 0 0 25 0 1 0 482671571 15634432 3388 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3817 3388 603 41 0 3776 0
vsize: 15268
[startup+150.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3416 0 0 0 14983 15 0 0 25 0 1 0 482671571 15634432 3394 4294967295 134512640 134672761 3221224528 3221223596 1075346560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3817 3394 603 41 0 3776 0
vsize: 15268
[startup+160.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3416 0 0 0 15983 16 0 0 25 0 1 0 482671571 15634432 3394 4294967295 134512640 134672761 3221224528 3221223544 1075352732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3817 3394 603 41 0 3776 0
vsize: 15268
[startup+170.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3416 0 0 0 16982 16 0 0 25 0 1 0 482671571 15634432 3394 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3817 3394 603 41 0 3776 0
vsize: 15268
[startup+180.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3416 0 0 0 17982 16 0 0 25 0 1 0 482671571 15634432 3394 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3817 3394 603 41 0 3776 0
vsize: 15268
[startup+190.013 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3416 0 0 0 18983 16 0 0 25 0 1 0 482671571 15634432 3394 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3817 3394 603 41 0 3776 0
vsize: 15268
[startup+200.013 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3416 0 0 0 19983 16 0 0 25 0 1 0 482671571 15634432 3394 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3817 3394 603 41 0 3776 0
vsize: 15268
[startup+210.027 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3416 0 0 0 20984 16 0 0 25 0 1 0 482671571 15634432 3394 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3817 3394 603 41 0 3776 0
vsize: 15268
[startup+220.034 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3416 0 0 0 21985 16 0 0 25 0 1 0 482671571 15634432 3394 4294967295 134512640 134672761 3221224528 3221223652 134566136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3817 3394 603 41 0 3776 0
vsize: 15268
[startup+230.034 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3417 0 0 0 22985 16 0 0 25 0 1 0 482671571 15634432 3395 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3817 3395 603 41 0 3776 0
vsize: 15268
[startup+240.034 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3417 0 0 0 23986 16 0 0 25 0 1 0 482671571 15634432 3395 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3817 3395 603 41 0 3776 0
vsize: 15268
[startup+250.034 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3576 0 0 0 24986 16 0 0 25 0 1 0 482671571 16302080 3554 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3980 3554 603 41 0 3939 0
vsize: 15920
[startup+260.035 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3763 0 0 0 25985 17 0 0 25 0 1 0 482671571 17104896 3741 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4176 3741 603 41 0 4135 0
vsize: 16704
[startup+270.035 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3798 0 0 0 26985 17 0 0 25 0 1 0 482671571 17252352 3776 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4212 3776 603 41 0 4171 0
vsize: 16848
[startup+280.034 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3822 0 0 0 27985 17 0 0 25 0 1 0 482671571 17416192 3800 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4252 3800 603 41 0 4211 0
vsize: 17008
[startup+290.035 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3822 0 0 0 28985 17 0 0 25 0 1 0 482671571 17416192 3800 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4252 3800 603 41 0 4211 0
vsize: 17008
[startup+300.035 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3822 0 0 0 29986 17 0 0 25 0 1 0 482671571 17416192 3800 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4252 3800 603 41 0 4211 0
vsize: 17008
[startup+310.036 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3822 0 0 0 30986 17 0 0 25 0 1 0 482671571 17416192 3800 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4252 3800 603 41 0 4211 0
vsize: 17008
[startup+320.036 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3832 0 0 0 31986 17 0 0 25 0 1 0 482671571 17416192 3810 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4252 3810 603 41 0 4211 0
vsize: 17008
[startup+330.036 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3845 0 0 0 32986 17 0 0 25 0 1 0 482671571 17555456 3823 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4286 3823 603 41 0 4245 0
vsize: 17144
[startup+340.036 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 3990 0 0 0 33985 18 0 0 25 0 1 0 482671571 18096128 3968 4294967295 134512640 134672761 3221224528 3221223632 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4418 3968 603 41 0 4377 0
vsize: 17672
[startup+350.036 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 4446 0 0 0 34985 19 0 0 25 0 1 0 482671571 19984384 4424 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4879 4424 603 41 0 4838 0
vsize: 19516
[startup+360.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 4580 0 0 0 35985 20 0 0 25 0 1 0 482671571 20525056 4558 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4558 603 41 0 4970 0
vsize: 20044
[startup+370.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 4580 0 0 0 36985 20 0 0 25 0 1 0 482671571 20525056 4558 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4558 603 41 0 4970 0
vsize: 20044
[startup+380.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 4580 0 0 0 37985 20 0 0 25 0 1 0 482671571 20525056 4558 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4558 603 41 0 4970 0
vsize: 20044
[startup+390.044 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 4804 0 0 0 38984 20 0 0 25 0 1 0 482671571 21467136 4782 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5241 4782 603 41 0 5200 0
vsize: 20964
[startup+400.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5240 0 0 0 39983 22 0 0 25 0 1 0 482671571 23195648 5218 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5663 5218 603 41 0 5622 0
vsize: 22652
[startup+410.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5645 0 0 0 40982 24 0 0 25 0 1 0 482671571 24936448 5623 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6088 5623 603 41 0 6047 0
vsize: 24352
[startup+420.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5911 0 0 0 41981 24 0 0 25 0 1 0 482671571 26001408 5889 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6348 5889 603 41 0 6307 0
vsize: 25392
[startup+430.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5911 0 0 0 42982 24 0 0 25 0 1 0 482671571 26001408 5889 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6348 5889 603 41 0 6307 0
vsize: 25392
[startup+440.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5911 0 0 0 43982 24 0 0 25 0 1 0 482671571 26001408 5889 4294967295 134512640 134672761 3221224528 3221223768 134557469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6348 5889 603 41 0 6307 0
vsize: 25392
[startup+450.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5911 0 0 0 44982 24 0 0 25 0 1 0 482671571 26001408 5889 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6348 5889 603 41 0 6307 0
vsize: 25392
[startup+460.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5913 0 0 0 45982 24 0 0 25 0 1 0 482671571 26001408 5891 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6348 5891 603 41 0 6307 0
vsize: 25392
[startup+470.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5915 0 0 0 46981 24 0 0 25 0 1 0 482671571 26001408 5893 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6348 5893 603 41 0 6307 0
vsize: 25392
[startup+480.043 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5970 0 0 0 47980 25 0 0 25 0 1 0 482671571 26271744 5948 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5948 603 41 0 6373 0
vsize: 25656
[startup+490.044 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5970 0 0 0 48981 25 0 0 25 0 1 0 482671571 26271744 5948 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5948 603 41 0 6373 0
vsize: 25656
[startup+500.044 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 49981 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+510.044 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 50981 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+520.044 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 2765
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 51981 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+530.044 s]
Raw data (loadavg): 0.99 1.00 0.95 3/58 2794
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 52981 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+540.044 s]
Raw data (loadavg): 1.07 1.02 0.96 2/54 2818
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 53981 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+550.044 s]
Raw data (loadavg): 1.06 1.02 0.96 2/54 2818
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 54981 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+560.045 s]
Raw data (loadavg): 1.05 1.01 0.96 2/54 2818
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 55982 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+570.045 s]
Raw data (loadavg): 1.04 1.01 0.96 2/54 2818
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 56982 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+580.045 s]
Raw data (loadavg): 1.03 1.01 0.96 2/54 2818
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 57982 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+590.045 s]
Raw data (loadavg): 1.03 1.01 0.96 2/54 2818
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 58982 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+600.045 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 2818
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 59982 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+610.046 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 60983 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223664 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+620.046 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 61983 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+630.046 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5971 0 0 0 62982 25 0 0 25 0 1 0 482671571 26271744 5949 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5949 603 41 0 6373 0
vsize: 25656
[startup+640.047 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 63983 25 0 0 25 0 1 0 482671571 26271744 5952 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5952 603 41 0 6373 0
vsize: 25656
[startup+650.047 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 64983 25 0 0 25 0 1 0 482671571 26271744 5952 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5952 603 41 0 6373 0
vsize: 25656
[startup+660.047 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 65983 25 0 0 25 0 1 0 482671571 26271744 5952 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5952 603 41 0 6373 0
vsize: 25656
[startup+670.047 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 66983 25 0 0 25 0 1 0 482671571 26271744 5952 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6414 5952 603 41 0 6373 0
vsize: 25656
[startup+680.047 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 67983 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+690.048 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 68984 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+700.048 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 69984 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+710.049 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 70984 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+720.049 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 71984 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+730.049 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 72984 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+740.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 73985 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+750.051 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 74985 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+760.052 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 75985 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+770.052 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 76985 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+780.052 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 77985 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223664 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+790.052 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5974 0 0 0 78986 25 0 0 25 0 1 0 482671571 26251264 5952 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5952 603 41 0 6368 0
vsize: 25636
[startup+800.052 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5975 0 0 0 79986 25 0 0 25 0 1 0 482671571 26251264 5953 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5953 603 41 0 6368 0
vsize: 25636
[startup+810.067 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5975 0 0 0 80988 25 0 0 25 0 1 0 482671571 26251264 5953 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5953 603 41 0 6368 0
vsize: 25636
[startup+820.076 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5975 0 0 0 81989 25 0 0 25 0 1 0 482671571 26251264 5953 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5953 603 41 0 6368 0
vsize: 25636
[startup+830.075 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5975 0 0 0 82989 25 0 0 25 0 1 0 482671571 26251264 5953 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5953 603 41 0 6368 0
vsize: 25636
[startup+840.076 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2820
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5975 0 0 0 83989 25 0 0 25 0 1 0 482671571 26251264 5953 4294967295 134512640 134672761 3221224528 3221223712 134558853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5953 603 41 0 6368 0
vsize: 25636
[startup+850.076 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5975 0 0 0 84989 25 0 0 25 0 1 0 482671571 26251264 5953 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5953 603 41 0 6368 0
vsize: 25636
[startup+860.077 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5975 0 0 0 85989 25 0 0 25 0 1 0 482671571 26251264 5953 4294967295 134512640 134672761 3221224528 3221223712 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6409 5953 603 41 0 6368 0
vsize: 25636
[startup+870.078 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 86988 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+880.078 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 87989 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+890.079 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 88989 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+900.078 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 89989 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+910.079 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 90989 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+920.08 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 91989 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+930.08 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 92990 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+940.081 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 93990 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+950.083 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 94990 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+960.084 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 95990 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+970.083 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 96990 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+980.083 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5978 0 0 0 97991 25 0 0 25 0 1 0 482671571 26251264 5956 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5956 603 41 0 6368 0
vsize: 25636
[startup+990.095 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5979 0 0 0 98992 25 0 0 25 0 1 0 482671571 26251264 5957 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5957 603 41 0 6368 0
vsize: 25636
[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5979 0 0 0 99992 25 0 0 25 0 1 0 482671571 26251264 5957 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5957 603 41 0 6368 0
vsize: 25636
[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5979 0 0 0 100992 25 0 0 25 0 1 0 482671571 26251264 5957 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5957 603 41 0 6368 0
vsize: 25636
[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5979 0 0 0 101993 25 0 0 25 0 1 0 482671571 26251264 5957 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5957 603 41 0 6368 0
vsize: 25636
[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 5979 0 0 0 102993 25 0 0 25 0 1 0 482671571 26251264 5957 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6409 5957 603 41 0 6368 0
vsize: 25636
[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 6259 0 0 0 103992 27 0 0 25 0 1 0 482671571 27316224 6237 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6669 6237 603 41 0 6628 0
vsize: 26676
[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 6664 0 0 0 104991 28 0 0 25 0 1 0 482671571 29052928 6642 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7093 6642 603 41 0 7052 0
vsize: 28372
[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 7098 0 0 0 105989 30 0 0 25 0 1 0 482671571 30781440 7076 4294967295 134512640 134672761 3221224528 3221223632 134560065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7515 7076 603 41 0 7474 0
vsize: 30060
[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 7525 0 0 0 106988 31 0 0 25 0 1 0 482671571 32526336 7503 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7941 7503 603 41 0 7900 0
vsize: 31764
[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 7889 0 0 0 107987 32 0 0 25 0 1 0 482671571 34127872 7867 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8332 7867 603 41 0 8291 0
vsize: 33328
[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8140 0 0 0 108987 33 0 0 25 0 1 0 482671571 35061760 8118 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 8118 603 41 0 8519 0
vsize: 34240
[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8140 0 0 0 109987 33 0 0 25 0 1 0 482671571 35061760 8118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 8118 603 41 0 8519 0
vsize: 34240
[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8140 0 0 0 110987 33 0 0 25 0 1 0 482671571 35061760 8118 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 8118 603 41 0 8519 0
vsize: 34240
[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8140 0 0 0 111987 33 0 0 25 0 1 0 482671571 35061760 8118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 8118 603 41 0 8519 0
vsize: 34240
[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8140 0 0 0 112988 33 0 0 25 0 1 0 482671571 35061760 8118 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 8118 603 41 0 8519 0
vsize: 34240
[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8140 0 0 0 113988 33 0 0 25 0 1 0 482671571 35061760 8118 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 8118 603 41 0 8519 0
vsize: 34240
[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8140 0 0 0 114988 33 0 0 25 0 1 0 482671571 35061760 8118 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 8118 603 41 0 8519 0
vsize: 34240
[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8140 0 0 0 115988 33 0 0 25 0 1 0 482671571 35061760 8118 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 8118 603 41 0 8519 0
vsize: 34240
[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8140 0 0 0 116988 33 0 0 25 0 1 0 482671571 35061760 8118 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8560 8118 603 41 0 8519 0
vsize: 34240
[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8455 0 0 0 117987 35 0 0 25 0 1 0 482671571 36392960 8433 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8885 8433 603 41 0 8844 0
vsize: 35540
[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 8802 0 0 0 118986 35 0 0 25 0 1 0 482671571 37867520 8780 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9245 8780 603 41 0 9204 0
vsize: 36980
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 2822
Raw data (stat): 2765 (minisat+) R 2764 10720 10719 0 -1 0 9150 0 0 0 119985 36 0 0 25 0 1 0 482671571 39374848 9128 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9613 9128 603 41 0 9572 0
vsize: 38452
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 2822
Raw data (stat): 2765 (minisat+) Z 2764 10720 10719 0 -1 12 9153 0 0 0 119986 38 0 0 25 0 1 0 482671571 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.13
CPU time (s): 1200.25
CPU user time (s): 1199.86
CPU system time (s): 0.386941
CPU usage (%): 100.01
Max. virtual memory (Kb): 38452
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####