PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-sao2.b.opb
MD5SUM	3e273bcee52631aeea0b7b1138e7d68d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	25
Optimality of the best value was proved	NO
Number of terms in the objective function	373
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	373
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	373
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03784
Number of variables	372
Total number of constraints	779
Number of constraints which are clauses	772
Number of constraints which are cardinality constraints (but not clauses)	7
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 4668

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-13 19:44:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3457 boxname=wulflinc5 idbench=73 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3e273bcee52631aeea0b7b1138e7d68d  /oldhome/oroussel/tmp/wulflinc5/normalized-sao2.b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc5/normalized-sao2.b.opb /oldhome/oroussel/tmp/wulflinc5/normalized-sao2.b.opb
IDLAUNCH: 3457
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        925776 kB
Buffers:         32768 kB
Cached:          54924 kB
SwapCached:       2272 kB
Active:          47436 kB
Inactive:        45344 kB
HighTotal:      131008 kB
HighFree:        72268 kB
LowTotal:       903652 kB
LowFree:        853508 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10560 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:04:57 (client local time) WITH STATUS 10 IN 1200.12 SECONDS
stats: 3457 7 1200.12 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 644 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     644    12554 |     214       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 728   maxlim: 336   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |    5678    30522 |    1892       1       29    29.0 |  0.000 % |
c |       101 |    5670    30492 |    2081     100      418     4.2 |  1.268 % |
c |       252 |    5670    30492 |    2289     251      996     4.0 |  1.268 % |
c |       477 |    5661    30463 |    2518     475     2091     4.4 |  1.449 % |
c |       814 |    5661    30463 |    2770     812     4650     5.7 |  1.449 % |
c |      1324 |    5645    30411 |    3047    1318    28097    21.3 |  1.721 % |
c |      2085 |    5645    30411 |    3351    2079    66538    32.0 |  1.721 % |
c ==============================================================================
c [1mFound solution: 36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 337   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2371 |    5646    30417 |    1882    2365    76938    32.5 |  1.721 % |
c |      2471 |    5646    30417 |    2070    1283    31660    24.7 |  1.810 % |
c |      2625 |    5646    30417 |    2277    1437    38609    26.9 |  1.811 % |
c |      2851 |    5646    30417 |    2504    1663    47046    28.3 |  1.810 % |
c |      3189 |    5646    30417 |    2755    2001    65986    33.0 |  1.810 % |
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 340   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3316 |    5650    30435 |    1883    2128    74867    35.2 |  1.810 % |
c |      3416 |    5650    30435 |    2071    1164    19795    17.0 |  1.987 % |
c |      3566 |    5650    30435 |    2278    1314    27451    20.9 |  1.989 % |
c |      3793 |    5650    30435 |    2506    1541    35603    23.1 |  1.987 % |
c |      4130 |    5650    30435 |    2756    1878    53493    28.5 |  1.987 % |
c |      4636 |    5650    30435 |    3032    2384    76130    31.9 |  1.987 % |
c |      5395 |    5650    30435 |    3335    3143   140572    44.7 |  1.987 % |
c |      6536 |    5650    30435 |    3669    2424   161109    66.5 |  1.987 % |
c |      8246 |    5650    30435 |    4036    2179    97619    44.8 |  1.987 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 342   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9230 |    5654    30454 |    1884    3163   157276    49.7 |  1.987 % |
c |      9331 |    5654    30454 |    2072    1683    33271    19.8 |  2.164 % |
c |      9482 |    5654    30454 |    2279    1834    39060    21.3 |  2.164 % |
c |      9709 |    5654    30454 |    2507    2061    48614    23.6 |  2.164 % |
c |     10046 |    5654    30454 |    2758    2398    56722    23.7 |  2.164 % |
c |     10553 |    5654    30454 |    3034    2905    93290    32.1 |  2.164 % |
c |     11312 |    5654    30454 |    3337    1980    74507    37.6 |  2.164 % |
c |     12451 |    5654    30454 |    3671    3119   164429    52.7 |  2.164 % |
c |     14161 |    5654    30454 |    4038    2873   163741    57.0 |  2.164 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 343   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15782 |    5655    30458 |    1885    4494   281727    62.7 |  2.164 % |
c |     15882 |    5655    30458 |    2073    1224    20537    16.8 |  2.252 % |
c |     16034 |    5655    30458 |    2280    1376    27535    20.0 |  2.252 % |
c |     16261 |    5655    30458 |    2508    1603    43650    27.2 |  2.252 % |
c |     16598 |    5655    30458 |    2759    1940    71877    37.0 |  2.252 % |
c |     17105 |    5655    30458 |    3035    2447   116460    47.6 |  2.252 % |
c |     17865 |    5655    30458 |    3339    3207   183898    57.3 |  2.252 % |
c |     19007 |    5655    30458 |    3673    2496   134471    53.9 |  2.252 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 344   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20566 |    5659    30473 |    1886    4055   264393    65.2 |  2.252 % |
c |     20667 |    5659    30473 |    2074    1115    14826    13.3 |  2.338 % |
c |     20820 |    5659    30473 |    2282    1268    22596    17.8 |  2.338 % |
c |     21045 |    5659    30473 |    2510    1493    35844    24.0 |  2.338 % |
c |     21382 |    5659    30473 |    2761    1830    49129    26.8 |  2.338 % |
c |     21890 |    5659    30473 |    3037    2338    79987    34.2 |  2.338 % |
c |     22650 |    5626    30360 |    3341    3082   120505    39.1 |  2.788 % |
c |     23790 |    5626    30360 |    3675    2379   105455    44.3 |  2.788 % |
c |     25500 |    5600    30270 |    4042    2128    97603    45.9 |  3.148 % |
c |     28063 |    5600    30270 |    4447    2445   119459    48.9 |  3.148 % |
c |     31908 |    5600    30270 |    4891    3889   205114    52.7 |  3.148 % |
c |     37679 |    5600    30270 |    5380    4448   325346    73.1 |  3.148 % |
c |     46329 |    5600    30270 |    5919    4574   374079    81.8 |  3.148 % |
c ==============================================================================
c [1mFound solution: 28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 345   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54157 |    5601    30276 |    1867    6101   464812    76.2 |  3.148 % |
c |     54257 |    5601    30276 |    2053    1626    58356    35.9 |  3.235 % |
c |     54407 |    5601    30276 |    2259    1776    61591    34.7 |  3.235 % |
c |     54632 |    5601    30276 |    2484    2001    68692    34.3 |  3.235 % |
c |     54970 |    5601    30276 |    2733    2339    92287    39.5 |  3.235 % |
c |     55476 |    5601    30276 |    3006    2845   133236    46.8 |  3.235 % |
c |     56235 |    5601    30276 |    3307    1918    89927    46.9 |  3.235 % |
c |     57378 |    5601    30276 |    3638    3061   177349    57.9 |  3.235 % |
c |     59095 |    5601    30276 |    4002    2904   135915    46.8 |  3.235 % |
c |     61657 |    5601    30276 |    4402    3332   199636    59.9 |  3.235 % |
c |     65501 |    5601    30276 |    4842    2545   120911    47.5 |  3.235 % |
c |     71267 |    5601    30276 |    5326    3146   183751    58.4 |  3.235 % |
c |     79918 |    5589    30236 |    5859    3398   216247    63.6 |  3.414 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 346   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89992 |    5590    30243 |    1863    4289   291892    68.1 |  3.414 % |
c |     90092 |    5590    30243 |    2049    1173    19362    16.5 |  3.501 % |
c |     90243 |    5590    30243 |    2254    1324    27147    20.5 |  3.501 % |
c |     90469 |    5590    30243 |    2479    1550    36836    23.8 |  3.501 % |
c |     90806 |    5590    30243 |    2727    1887    49641    26.3 |  3.501 % |
c |     91314 |    5590    30243 |    3000    2395    76358    31.9 |  3.501 % |
c |     92073 |    5590    30243 |    3300    3154    96944    30.7 |  3.501 % |
c |     93212 |    5590    30243 |    3630    2476    98978    40.0 |  3.501 % |
c |     94922 |    5590    30243 |    3993    2234    99370    44.5 |  3.501 % |
c |     97488 |    5590    30243 |    4392    2697   147341    54.6 |  3.501 % |
c |    101333 |    5590    30243 |    4832    4227   267475    63.3 |  3.501 % |
c |    107099 |    5590    30243 |    5315    4857   344867    71.0 |  3.501 % |
c |    115749 |    5590    30243 |    5846    4980   405556    81.4 |  3.501 % |
c |    128724 |    5590    30243 |    6431    5731   345091    60.2 |  3.501 % |
c |    148185 |    5590    30243 |    7074    4942   436329    88.3 |  3.501 % |
c |    177378 |    5590    30243 |    7782    4965   351620    70.8 |  3.501 % |
c |    221170 |    5590    30243 |    8560    4448   301627    67.8 |  3.501 % |
c |    286854 |    5590    30243 |    9416    8592   703913    81.9 |  3.501 % |
c |    385381 |    5590    30243 |   10358    5815   486238    83.6 |  3.501 % |
c |    533172 |    5590    30243 |   11393    9414   916228    97.3 |  3.501 % |
c |    754855 |    5590    30243 |   12533    9728   718210    73.8 |  3.501 % |
c |   1087381 |    5590    30243 |   13786   10680   879568    82.4 |  3.501 % |
#### 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.85 0.94 0.68 2/54 25750
Raw data (stat): 25750 (runsolver) R 25749 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420349851 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99991 s]
Raw data (loadavg): 0.87 0.94 0.69 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 817 0 0 0 996 2 0 0 25 0 1 0 420349851 4878336 795 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1191 795 603 41 0 1150 0
vsize: 4764
[startup+19.9994 s]
Raw data (loadavg): 0.89 0.94 0.69 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1188 0 0 0 1993 4 0 0 25 0 1 0 420349851 6361088 1166 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1553 1166 603 41 0 1512 0
vsize: 6212
[startup+30.0008 s]
Raw data (loadavg): 0.91 0.94 0.69 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1189 0 0 0 2992 4 0 0 25 0 1 0 420349851 6361088 1167 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1553 1167 603 41 0 1512 0
vsize: 6212
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.94 0.70 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1189 0 0 0 3991 5 0 0 25 0 1 0 420349851 6361088 1167 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1553 1167 603 41 0 1512 0
vsize: 6212
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.94 0.70 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1212 0 0 0 4991 5 0 0 25 0 1 0 420349851 6496256 1190 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1586 1190 603 41 0 1545 0
vsize: 6344
[startup+60.002 s]
Raw data (loadavg): 0.94 0.95 0.70 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1245 0 0 0 5991 5 0 0 25 0 1 0 420349851 6631424 1223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1619 1223 603 41 0 1578 0
vsize: 6476
[startup+70.0023 s]
Raw data (loadavg): 0.95 0.95 0.70 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1314 0 0 0 6990 6 0 0 25 0 1 0 420349851 6901760 1292 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1685 1292 603 41 0 1644 0
vsize: 6740
[startup+80.003 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1543 0 0 0 7989 7 0 0 25 0 1 0 420349851 7847936 1521 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1916 1521 603 41 0 1875 0
vsize: 7664
[startup+90.0032 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1639 0 0 0 8988 8 0 0 25 0 1 0 420349851 8245248 1617 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2013 1617 603 41 0 1972 0
vsize: 8052
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.71 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1639 0 0 0 9987 9 0 0 25 0 1 0 420349851 8245248 1617 4294967295 134512640 134672761 3221224576 3221223680 134560269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2013 1617 603 41 0 1972 0
vsize: 8052
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1720 0 0 0 10987 9 0 0 25 0 1 0 420349851 8511488 1698 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2078 1698 603 41 0 2037 0
vsize: 8312
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1739 0 0 0 11986 10 0 0 25 0 1 0 420349851 8646656 1717 4294967295 134512640 134672761 3221224576 3221223760 134558690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2111 1717 603 41 0 2070 0
vsize: 8444
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1739 0 0 0 12986 10 0 0 25 0 1 0 420349851 8646656 1717 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2111 1717 603 41 0 2070 0
vsize: 8444
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1739 0 0 0 13985 10 0 0 25 0 1 0 420349851 8646656 1717 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2111 1717 603 41 0 2070 0
vsize: 8444
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1739 0 0 0 14985 10 0 0 25 0 1 0 420349851 8646656 1717 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2111 1717 603 41 0 2070 0
vsize: 8444
[startup+160.008 s]
Raw data (loadavg): 0.99 0.95 0.73 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1739 0 0 0 15984 11 0 0 25 0 1 0 420349851 8646656 1717 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2111 1717 603 41 0 2070 0
vsize: 8444
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1917 0 0 0 16984 11 0 0 25 0 1 0 420349851 9318400 1895 4294967295 134512640 134672761 3221224576 3221223760 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2275 1895 603 41 0 2234 0
vsize: 9100
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1924 0 0 0 17984 12 0 0 25 0 1 0 420349851 9465856 1902 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2311 1902 603 41 0 2270 0
vsize: 9244
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1932 0 0 0 18983 12 0 0 25 0 1 0 420349851 9465856 1910 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2311 1910 603 41 0 2270 0
vsize: 9244
[startup+200.01 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1956 0 0 0 19983 12 0 0 25 0 1 0 420349851 9601024 1934 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2344 1934 603 41 0 2303 0
vsize: 9376
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1957 0 0 0 20982 13 0 0 25 0 1 0 420349851 9601024 1935 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2344 1935 603 41 0 2303 0
vsize: 9376
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 1957 0 0 0 21982 13 0 0 25 0 1 0 420349851 9601024 1935 4294967295 134512640 134672761 3221224576 3221223760 134559272 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2344 1935 603 41 0 2303 0
vsize: 9376
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2110 0 0 0 22982 14 0 0 25 0 1 0 420349851 10141696 2088 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2476 2088 603 41 0 2435 0
vsize: 9904
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2146 0 0 0 23981 14 0 0 25 0 1 0 420349851 10276864 2124 4294967295 134512640 134672761 3221224576 3221223776 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2509 2124 603 41 0 2468 0
vsize: 10036
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2198 0 0 0 24981 14 0 0 25 0 1 0 420349851 10543104 2176 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2574 2176 603 41 0 2533 0
vsize: 10296
[startup+260.012 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2209 0 0 0 25980 15 0 0 25 0 1 0 420349851 10543104 2187 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2574 2187 603 41 0 2533 0
vsize: 10296
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2213 0 0 0 26980 15 0 0 25 0 1 0 420349851 10543104 2191 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2574 2191 603 41 0 2533 0
vsize: 10296
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2224 0 0 0 27980 15 0 0 25 0 1 0 420349851 10690560 2202 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2610 2202 603 41 0 2569 0
vsize: 10440
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2224 0 0 0 28981 15 0 0 25 0 1 0 420349851 10690560 2202 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2610 2202 603 41 0 2569 0
vsize: 10440
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2224 0 0 0 29981 15 0 0 25 0 1 0 420349851 10690560 2202 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2610 2202 603 41 0 2569 0
vsize: 10440
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2244 0 0 0 30981 15 0 0 25 0 1 0 420349851 10690560 2222 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2610 2222 603 41 0 2569 0
vsize: 10440
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2304 0 0 0 31981 15 0 0 25 0 1 0 420349851 10960896 2282 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2676 2282 603 41 0 2635 0
vsize: 10704
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2418 0 0 0 32981 16 0 0 25 0 1 0 420349851 11493376 2396 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2806 2396 603 41 0 2765 0
vsize: 11224
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2540 0 0 0 33980 16 0 0 25 0 1 0 420349851 12029952 2518 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2937 2518 603 41 0 2896 0
vsize: 11748
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2618 0 0 0 34981 16 0 0 25 0 1 0 420349851 12300288 2596 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3003 2596 603 41 0 2962 0
vsize: 12012
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2634 0 0 0 35981 16 0 0 25 0 1 0 420349851 12300288 2612 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3003 2612 603 41 0 2962 0
vsize: 12012
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2683 0 0 0 36981 16 0 0 25 0 1 0 420349851 12574720 2661 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2661 603 41 0 3029 0
vsize: 12280
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2683 0 0 0 37981 16 0 0 25 0 1 0 420349851 12574720 2661 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2661 603 41 0 3029 0
vsize: 12280
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2683 0 0 0 38981 16 0 0 25 0 1 0 420349851 12574720 2661 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2661 603 41 0 3029 0
vsize: 12280
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2683 0 0 0 39981 16 0 0 25 0 1 0 420349851 12574720 2661 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2661 603 41 0 3029 0
vsize: 12280
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2684 0 0 0 40981 17 0 0 25 0 1 0 420349851 12574720 2662 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3070 2662 603 41 0 3029 0
vsize: 12280
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2684 0 0 0 41981 17 0 0 25 0 1 0 420349851 12574720 2662 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2662 603 41 0 3029 0
vsize: 12280
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2684 0 0 0 42981 17 0 0 25 0 1 0 420349851 12574720 2662 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2662 603 41 0 3029 0
vsize: 12280
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2684 0 0 0 43981 17 0 0 25 0 1 0 420349851 12509184 2662 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2662 603 41 0 3013 0
vsize: 12216
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2684 0 0 0 44981 17 0 0 25 0 1 0 420349851 12509184 2662 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2662 603 41 0 3013 0
vsize: 12216
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2684 0 0 0 45982 17 0 0 25 0 1 0 420349851 12509184 2662 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2662 603 41 0 3013 0
vsize: 12216
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2684 0 0 0 46982 17 0 0 25 0 1 0 420349851 12509184 2662 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2662 603 41 0 3013 0
vsize: 12216
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2685 0 0 0 47982 17 0 0 25 0 1 0 420349851 12509184 2663 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2663 603 41 0 3013 0
vsize: 12216
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2685 0 0 0 48981 17 0 0 25 0 1 0 420349851 12509184 2663 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2663 603 41 0 3013 0
vsize: 12216
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2685 0 0 0 49981 17 0 0 25 0 1 0 420349851 12509184 2663 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2663 603 41 0 3013 0
vsize: 12216
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2685 0 0 0 50981 17 0 0 25 0 1 0 420349851 12509184 2663 4294967295 134512640 134672761 3221224576 3221223760 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2663 603 41 0 3013 0
vsize: 12216
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2685 0 0 0 51982 17 0 0 25 0 1 0 420349851 12509184 2663 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2663 603 41 0 3013 0
vsize: 12216
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2685 0 0 0 52982 17 0 0 25 0 1 0 420349851 12509184 2663 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2663 603 41 0 3013 0
vsize: 12216
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2685 0 0 0 53982 17 0 0 25 0 1 0 420349851 12509184 2663 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2663 603 41 0 3013 0
vsize: 12216
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2685 0 0 0 54982 17 0 0 25 0 1 0 420349851 12509184 2663 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2663 603 41 0 3013 0
vsize: 12216
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2702 0 0 0 55982 17 0 0 25 0 1 0 420349851 12656640 2680 4294967295 134512640 134672761 3221224576 3221223760 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3090 2680 603 41 0 3049 0
vsize: 12360
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2707 0 0 0 56983 17 0 0 25 0 1 0 420349851 12656640 2685 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3090 2685 603 41 0 3049 0
vsize: 12360
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2707 0 0 0 57983 17 0 0 25 0 1 0 420349851 12656640 2685 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3090 2685 603 41 0 3049 0
vsize: 12360
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2754 0 0 0 58983 17 0 0 25 0 1 0 420349851 12922880 2732 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2732 603 41 0 3114 0
vsize: 12620
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2764 0 0 0 59983 17 0 0 25 0 1 0 420349851 12922880 2742 4294967295 134512640 134672761 3221224576 3221223760 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2742 603 41 0 3114 0
vsize: 12620
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2764 0 0 0 60983 17 0 0 25 0 1 0 420349851 12922880 2742 4294967295 134512640 134672761 3221224576 3221223680 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2742 603 41 0 3114 0
vsize: 12620
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2765 0 0 0 61983 17 0 0 25 0 1 0 420349851 12922880 2743 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2743 603 41 0 3114 0
vsize: 12620
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2819 0 0 0 62983 17 0 0 25 0 1 0 420349851 13193216 2797 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3221 2797 603 41 0 3180 0
vsize: 12884
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2835 0 0 0 63983 17 0 0 25 0 1 0 420349851 13193216 2813 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3221 2813 603 41 0 3180 0
vsize: 12884
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2835 0 0 0 64983 17 0 0 25 0 1 0 420349851 13193216 2813 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3221 2813 603 41 0 3180 0
vsize: 12884
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2870 0 0 0 65983 18 0 0 25 0 1 0 420349851 13328384 2848 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3254 2848 603 41 0 3213 0
vsize: 13016
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2915 0 0 0 66983 18 0 0 25 0 1 0 420349851 13611008 2893 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2893 603 41 0 3282 0
vsize: 13292
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2932 0 0 0 67983 18 0 0 25 0 1 0 420349851 13611008 2910 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2910 603 41 0 3282 0
vsize: 13292
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2932 0 0 0 68983 18 0 0 25 0 1 0 420349851 13611008 2910 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2910 603 41 0 3282 0
vsize: 13292
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2932 0 0 0 69984 18 0 0 25 0 1 0 420349851 13611008 2910 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2910 603 41 0 3282 0
vsize: 13292
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2932 0 0 0 70984 18 0 0 25 0 1 0 420349851 13611008 2910 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2910 603 41 0 3282 0
vsize: 13292
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2932 0 0 0 71984 18 0 0 25 0 1 0 420349851 13611008 2910 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2910 603 41 0 3282 0
vsize: 13292
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2932 0 0 0 72984 18 0 0 25 0 1 0 420349851 13611008 2910 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2910 603 41 0 3282 0
vsize: 13292
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2932 0 0 0 73984 18 0 0 25 0 1 0 420349851 13611008 2910 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2910 603 41 0 3282 0
vsize: 13292
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2938 0 0 0 74985 18 0 0 25 0 1 0 420349851 13611008 2916 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2916 603 41 0 3282 0
vsize: 13292
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2938 0 0 0 75985 18 0 0 25 0 1 0 420349851 13611008 2916 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3323 2916 603 41 0 3282 0
vsize: 13292
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2944 0 0 0 76985 18 0 0 25 0 1 0 420349851 13774848 2922 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2922 603 41 0 3322 0
vsize: 13452
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2950 0 0 0 77985 18 0 0 25 0 1 0 420349851 13774848 2928 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2928 603 41 0 3322 0
vsize: 13452
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2950 0 0 0 78985 18 0 0 25 0 1 0 420349851 13774848 2928 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2928 603 41 0 3322 0
vsize: 13452
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2950 0 0 0 79985 18 0 0 25 0 1 0 420349851 13774848 2928 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2928 603 41 0 3322 0
vsize: 13452
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2950 0 0 0 80986 18 0 0 25 0 1 0 420349851 13774848 2928 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2928 603 41 0 3322 0
vsize: 13452
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2950 0 0 0 81986 18 0 0 25 0 1 0 420349851 13774848 2928 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2928 603 41 0 3322 0
vsize: 13452
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2956 0 0 0 82986 18 0 0 25 0 1 0 420349851 13774848 2934 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2934 603 41 0 3322 0
vsize: 13452
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2962 0 0 0 83986 18 0 0 25 0 1 0 420349851 13774848 2940 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2940 603 41 0 3322 0
vsize: 13452
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2962 0 0 0 84986 18 0 0 25 0 1 0 420349851 13774848 2940 4294967295 134512640 134672761 3221224576 3221223680 134555084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2940 603 41 0 3322 0
vsize: 13452
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2962 0 0 0 85987 18 0 0 25 0 1 0 420349851 13774848 2940 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2940 603 41 0 3322 0
vsize: 13452
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2962 0 0 0 86987 18 0 0 25 0 1 0 420349851 13774848 2940 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3363 2940 603 41 0 3322 0
vsize: 13452
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2970 0 0 0 87987 18 0 0 25 0 1 0 420349851 13922304 2948 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3399 2948 603 41 0 3358 0
vsize: 13596
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2970 0 0 0 88987 18 0 0 25 0 1 0 420349851 13922304 2948 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3399 2948 603 41 0 3358 0
vsize: 13596
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 25750
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2970 0 0 0 89987 18 0 0 25 0 1 0 420349851 13922304 2948 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3399 2948 603 41 0 3358 0
vsize: 13596
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.85 4/58 25779
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2976 0 0 0 90987 18 0 0 25 0 1 0 420349851 13922304 2954 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3399 2954 603 41 0 3358 0
vsize: 13596
[startup+920.027 s]
Raw data (loadavg): 1.07 0.99 0.85 2/54 25803
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 2976 0 0 0 91987 18 0 0 25 0 1 0 420349851 13922304 2954 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3399 2954 603 41 0 3358 0
vsize: 13596
[startup+930.027 s]
Raw data (loadavg): 1.06 0.99 0.85 2/54 25803
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3102 0 0 0 92986 19 0 0 25 0 1 0 420349851 14458880 3080 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3530 3080 603 41 0 3489 0
vsize: 14120
[startup+940.027 s]
Raw data (loadavg): 1.05 0.99 0.86 2/54 25803
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3111 0 0 0 93986 19 0 0 25 0 1 0 420349851 14458880 3089 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3530 3089 603 41 0 3489 0
vsize: 14120
[startup+950.026 s]
Raw data (loadavg): 1.04 0.99 0.86 2/54 25803
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3234 0 0 0 94986 19 0 0 25 0 1 0 420349851 14999552 3212 4294967295 134512640 134672761 3221224576 3221223680 134554919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3662 3212 603 41 0 3621 0
vsize: 14648
[startup+960.026 s]
Raw data (loadavg): 1.03 0.99 0.86 2/54 25803
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3330 0 0 0 95986 19 0 0 25 0 1 0 420349851 15405056 3308 4294967295 134512640 134672761 3221224576 3221223712 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3308 603 41 0 3720 0
vsize: 15044
[startup+970.027 s]
Raw data (loadavg): 1.03 0.99 0.86 2/54 25803
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3333 0 0 0 96986 19 0 0 25 0 1 0 420349851 15405056 3311 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3311 603 41 0 3720 0
vsize: 15044
[startup+980.028 s]
Raw data (loadavg): 1.02 0.99 0.86 2/54 25803
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3333 0 0 0 97987 19 0 0 25 0 1 0 420349851 15405056 3311 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3311 603 41 0 3720 0
vsize: 15044
[startup+990.028 s]
Raw data (loadavg): 1.02 0.99 0.86 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3334 0 0 0 98987 19 0 0 25 0 1 0 420349851 15405056 3312 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3312 603 41 0 3720 0
vsize: 15044
[startup+1000.03 s]
Raw data (loadavg): 1.02 0.99 0.86 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3334 0 0 0 99987 19 0 0 25 0 1 0 420349851 15405056 3312 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3312 603 41 0 3720 0
vsize: 15044
[startup+1010.03 s]
Raw data (loadavg): 1.01 0.99 0.86 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3334 0 0 0 100987 19 0 0 25 0 1 0 420349851 15405056 3312 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3312 603 41 0 3720 0
vsize: 15044
[startup+1020.03 s]
Raw data (loadavg): 1.01 0.99 0.86 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3334 0 0 0 101987 19 0 0 25 0 1 0 420349851 15405056 3312 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3312 603 41 0 3720 0
vsize: 15044
[startup+1030.03 s]
Raw data (loadavg): 1.01 0.99 0.86 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3334 0 0 0 102987 19 0 0 25 0 1 0 420349851 15405056 3312 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3312 603 41 0 3720 0
vsize: 15044
[startup+1040.03 s]
Raw data (loadavg): 1.01 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3334 0 0 0 103988 19 0 0 25 0 1 0 420349851 15405056 3312 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3312 603 41 0 3720 0
vsize: 15044
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3334 0 0 0 104988 19 0 0 25 0 1 0 420349851 15405056 3312 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3312 603 41 0 3720 0
vsize: 15044
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3334 0 0 0 105988 19 0 0 25 0 1 0 420349851 15405056 3312 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3312 603 41 0 3720 0
vsize: 15044
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3334 0 0 0 106988 19 0 0 25 0 1 0 420349851 15405056 3312 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3761 3312 603 41 0 3720 0
vsize: 15044
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3414 0 0 0 107988 19 0 0 25 0 1 0 420349851 15675392 3392 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3827 3392 603 41 0 3786 0
vsize: 15308
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3642 0 0 0 108988 20 0 0 25 0 1 0 420349851 16605184 3620 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4054 3620 603 41 0 4013 0
vsize: 16216
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3801 0 0 0 109987 20 0 0 25 0 1 0 420349851 17268736 3779 4294967295 134512640 134672761 3221224576 3221223680 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3779 603 41 0 4175 0
vsize: 16864
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3801 0 0 0 110988 20 0 0 25 0 1 0 420349851 17268736 3779 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3779 603 41 0 4175 0
vsize: 16864
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3801 0 0 0 111988 20 0 0 25 0 1 0 420349851 17268736 3779 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3779 603 41 0 4175 0
vsize: 16864
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3801 0 0 0 112988 20 0 0 25 0 1 0 420349851 17268736 3779 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3779 603 41 0 4175 0
vsize: 16864
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3801 0 0 0 113988 20 0 0 25 0 1 0 420349851 17268736 3779 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3779 603 41 0 4175 0
vsize: 16864
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3801 0 0 0 114988 20 0 0 25 0 1 0 420349851 17268736 3779 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3779 603 41 0 4175 0
vsize: 16864
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3801 0 0 0 115989 20 0 0 25 0 1 0 420349851 17268736 3779 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3779 603 41 0 4175 0
vsize: 16864
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3802 0 0 0 116989 20 0 0 25 0 1 0 420349851 17268736 3780 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3780 603 41 0 4175 0
vsize: 16864
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3802 0 0 0 117989 20 0 0 25 0 1 0 420349851 17268736 3780 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3780 603 41 0 4175 0
vsize: 16864
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3802 0 0 0 118989 20 0 0 25 0 1 0 420349851 17268736 3780 4294967295 134512640 134672761 3221224576 3221223760 134559665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4216 3780 603 41 0 4175 0
vsize: 16864
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 25805
Raw data (stat): 25750 (minisat+) R 25749 24215 24214 0 -1 0 3802 0 0 0 119989 20 0 0 25 0 1 0 420349851 17248256 3780 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4211 3780 603 41 0 4170 0
vsize: 16844
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.88 1/54 25805
Raw data (stat): 25750 (minisat+) Z 25749 24215 24214 0 -1 12 3805 0 0 0 119989 21 0 0 25 0 1 0 420349851 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.12
CPU user time (s): 1199.9
CPU system time (s): 0.218966
CPU usage (%): 100.006
Max. virtual memory (Kb): 16864
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####