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/een/normalized-mod008.opb
MD5SUM	18b325bb9311c83b0604c703bacc9a29
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	87
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	7499
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	758444
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.283956
Number of variables	319
Total number of constraints	6
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	186
Maximum length of a constraint	231
Trace number 7101

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        855584 kB
Buffers:         36412 kB
Cached:         105568 kB
SwapCached:          4 kB
Active:          66736 kB
Inactive:        79020 kB
HighTotal:      131008 kB
HighFree:        20944 kB
LowTotal:       903652 kB
LowFree:        834640 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27764 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:34:17 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 5145 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss.ss
c ---[   4]---> Adder-cost: 111   maxlim: 11   bits: 5/4
c ---[   3]---> Adder-cost: 124   maxlim: 20   bits: 6/5
c ---[   2]---> Adder-cost: 113   maxlim: 4   bits: 4/3
c ---[   1]---> Adder-cost: 66   maxlim: 5   bits: 4/3
c ---[   0]---> Adder-cost: 53   maxlim: 10   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2757    10913 |     919       0        0     nan |  0.000 % |
c |       100 |    2757    10913 |    1010     100      346     3.5 |  1.571 % |
c ==============================================================================
c [1mFound solution: 1914[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1828   maxlim: 21640   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       124 |   15448    56220 |    5149     124      424     3.4 |  1.571 % |
c |       225 |   15448    56220 |    5663     225      776     3.4 |  0.847 % |
c |       375 |   15448    56220 |    6230     375     1486     4.0 |  0.847 % |
c |       600 |   15415    56109 |    6853     595     2560     4.3 |  1.078 % |
c |       938 |   15398    56048 |    7538     929     4563     4.9 |  1.155 % |
c |      1444 |   15398    56048 |    8292    1435     7577     5.3 |  1.155 % |
c |      2203 |   15389    56019 |    9121    2193    14801     6.7 |  1.232 % |
c |      3343 |   15389    56019 |   10033    3333    23339     7.0 |  1.232 % |
c |      5051 |   15389    56019 |   11037    5041    58041    11.5 |  1.232 % |
c |      7614 |   15389    56019 |   12141    7604   112790    14.8 |  1.232 % |
c |     11458 |   15389    56019 |   13355   11448   231915    20.3 |  1.232 % |
c |     17225 |   15389    56019 |   14690   10133   377570    37.3 |  1.232 % |
c |     25874 |   15389    56019 |   16159   11254   784649    69.7 |  1.232 % |
c |     38848 |   15389    56019 |   17775   15894   666424    41.9 |  1.232 % |
c |     58309 |   15389    56019 |   19553   17067  1799760   105.5 |  1.232 % |
c |     87501 |   15389    56019 |   21508   16718   685612    41.0 |  1.232 % |
c |    131291 |   15389    56019 |   23659   16887  1720675   101.9 |  1.232 % |
c |    196976 |   15389    56019 |   26025   22042  1978672    89.8 |  1.232 % |
c ==============================================================================
c [1mFound solution: 1850[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21704   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    259858 |   15396    56059 |    5132   18673  1813136    97.1 |  1.232 % |
c |    259959 |   15396    56059 |    5645    4770   342468    71.8 |  1.345 % |
c |    260109 |   15396    56059 |    6209    4920   343541    69.8 |  1.345 % |
c |    260335 |   15396    56059 |    6830    5146   348913    67.8 |  1.345 % |
c |    260675 |   15396    56059 |    7513    5486   350820    63.9 |  1.345 % |
c |    261182 |   15396    56059 |    8265    5993   354693    59.2 |  1.345 % |
c |    261942 |   15396    56059 |    9091    6753   378847    56.1 |  1.345 % |
c |    263081 |   15396    56059 |   10000    7892   412458    52.3 |  1.345 % |
c |    264789 |   15396    56059 |   11000    9600   463372    48.3 |  1.345 % |
c |    267351 |   15396    56059 |   12100    6465   140775    21.8 |  1.345 % |
c |    271197 |   15396    56059 |   13311   10311   284942    27.6 |  1.345 % |
c |    276963 |   15396    56059 |   14642    9170   460269    50.2 |  1.345 % |
c |    285612 |   15396    56059 |   16106   10219   602203    58.9 |  1.345 % |
c |    298586 |   15396    56059 |   17717   14857  1073820    72.3 |  1.345 % |
c |    318047 |   15396    56059 |   19488   16108  1518898    94.3 |  1.345 % |
c ==============================================================================
c [1mFound solution: 1779[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21775   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    343961 |   15400    56079 |    5133   11881  1001040    84.3 |  1.345 % |
c |    344061 |   15400    56079 |    5646    3071   119306    38.8 |  1.421 % |
c |    344211 |   15391    56048 |    6210    3207   119918    37.4 |  1.459 % |
c |    344436 |   15391    56048 |    6832    3432   121344    35.4 |  1.459 % |
c |    344774 |   15391    56048 |    7515    3770   123801    32.8 |  1.459 % |
c |    345280 |   15391    56048 |    8266    4276   128375    30.0 |  1.459 % |
c |    346039 |   15391    56048 |    9093    5035   136856    27.2 |  1.459 % |
c |    347180 |   15391    56048 |   10002    6176   157196    25.5 |  1.459 % |
c |    348888 |   15391    56048 |   11003    7884   197398    25.0 |  1.459 % |
c |    351451 |   15391    56048 |   12103   10447   285101    27.3 |  1.459 % |
c |    355295 |   15391    56048 |   13313    7845   322469    41.1 |  1.459 % |
c |    361061 |   15391    56048 |   14645   13611   792496    58.2 |  1.459 % |
c |    369711 |   15391    56048 |   16109   14304  1132750    79.2 |  1.459 % |
c |    382685 |   15391    56048 |   17720   10536   748317    71.0 |  1.459 % |
c |    402148 |   15391    56048 |   19492   11469   699838    61.0 |  1.459 % |
c |    431341 |   15382    56017 |   21441   10417   870250    83.5 |  1.498 % |
c |    475130 |   15382    56017 |   23585   21090  2193454   104.0 |  1.498 % |
c ==============================================================================
c [1mFound solution: 1719[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21835   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    514393 |   15386    56046 |    5128   23760  2196756    92.5 |  1.498 % |
c |    514493 |   15386    56046 |    5640    3070    83111    27.1 |  1.610 % |
c |    514643 |   15386    56046 |    6204    3220    83881    26.1 |  1.610 % |
c |    514868 |   15386    56046 |    6825    3445    85560    24.8 |  1.610 % |
c |    515205 |   15386    56046 |    7507    3782    89250    23.6 |  1.610 % |
c |    515711 |   15386    56046 |    8258    4288    93612    21.8 |  1.610 % |
c |    516471 |   15386    56046 |    9084    5048   116120    23.0 |  1.610 % |
c |    517610 |   15386    56046 |    9993    6187   149681    24.2 |  1.610 % |
c |    519319 |   15386    56046 |   10992    7896   260183    33.0 |  1.610 % |
c |    521883 |   15386    56046 |   12091   10460   419191    40.1 |  1.610 % |
c |    525727 |   15386    56046 |   13300    7867   367801    46.8 |  1.610 % |
c |    531493 |   15386    56046 |   14630   13633   793887    58.2 |  1.610 % |
c |    540144 |   15386    56046 |   16093   14722   927563    63.0 |  1.610 % |
c |    553118 |   15386    56046 |   17703   11024  1155745   104.8 |  1.610 % |
c |    572579 |   15386    56046 |   19473   12278   803632    65.5 |  1.610 % |
c |    601771 |   15386    56046 |   21420   11586   838484    72.4 |  1.610 % |
c |    645563 |   15386    56046 |   23563   12101   957012    79.1 |  1.610 % |
c |    711247 |   15386    56046 |   25919   17852  1995275   111.8 |  1.610 % |
c |    809775 |   15386    56046 |   28511   24142  2008365    83.2 |  1.610 % |
c |    957565 |   15386    56046 |   31362   27254  2283978    83.8 |  1.610 % |
c ==============================================================================
c [1mFound solution: 1716[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21838   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1012276 |   15394    56093 |    5131   31947  3406414   106.6 |  1.610 % |
c |   1012378 |   15394    56093 |    5644    4096   166035    40.5 |  1.686 % |
c |   1012528 |   15394    56093 |    6208    4246   166803    39.3 |  1.686 % |
c |   1012755 |   15394    56093 |    6829    4473   167915    37.5 |  1.686 % |
c |   1013093 |   15394    56093 |    7512    4811   170394    35.4 |  1.686 % |
c |   1013601 |   15394    56093 |    8263    5319   177213    33.3 |  1.686 % |
c |   1014360 |   15394    56093 |    9089    6078   205923    33.9 |  1.686 % |
c |   1015499 |   15394    56093 |    9998    7217   255285    35.4 |  1.686 % |
c |   1017210 |   15394    56093 |   10998    8928   294096    32.9 |  1.686 % |
c |   1019772 |   15394    56093 |   12098   11490   403612    35.1 |  1.686 % |
c |   1023616 |   15394    56093 |   13308    8736   371954    42.6 |  1.686 % |
c |   1029386 |   15394    56093 |   14639    7575   236383    31.2 |  1.686 % |
c |   1038039 |   15394    56093 |   16103    8483   594922    70.1 |  1.686 % |
c |   1051013 |   15394    56093 |   17713   13136   717056    54.6 |  1.686 % |
c |   1070474 |   15394    56093 |   19484   14480  1028390    71.0 |  1.686 % |
c |   1099668 |   15394    56093 |   21433   13854   854302    61.7 |  1.686 % |
#### 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.69 0.88 0.87 2/54 27062
Raw data (stat): 27062 (runsolver) R 27061 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487752624 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+10.001 s]
Raw data (loadavg): 0.74 0.89 0.87 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 1610 0 0 0 994 4 0 0 25 0 1 0 487752624 8130560 1588 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1985 1588 603 41 0 1944 0
vsize: 7940
[startup+20.0017 s]
Raw data (loadavg): 0.78 0.89 0.87 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 1901 0 0 0 1993 5 0 0 25 0 1 0 487752624 9453568 1879 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2308 1879 603 41 0 2267 0
vsize: 9232
[startup+30.002 s]
Raw data (loadavg): 0.81 0.89 0.87 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 2040 0 0 0 2993 6 0 0 25 0 1 0 487752624 9986048 2018 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2438 2018 603 41 0 2397 0
vsize: 9752
[startup+40.002 s]
Raw data (loadavg): 0.84 0.90 0.87 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 2889 0 0 0 3990 8 0 0 25 0 1 0 487752624 13479936 2867 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2867 603 41 0 3250 0
vsize: 13164
[startup+50.0017 s]
Raw data (loadavg): 0.86 0.90 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 2898 0 0 0 4990 8 0 0 25 0 1 0 487752624 13479936 2876 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2876 603 41 0 3250 0
vsize: 13164
[startup+60.0021 s]
Raw data (loadavg): 0.88 0.90 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 2898 0 0 0 5990 9 0 0 25 0 1 0 487752624 13479936 2876 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2876 603 41 0 3250 0
vsize: 13164
[startup+70.002 s]
Raw data (loadavg): 0.90 0.90 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 2900 0 0 0 6990 9 0 0 25 0 1 0 487752624 13479936 2878 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2878 603 41 0 3250 0
vsize: 13164
[startup+80.0027 s]
Raw data (loadavg): 0.92 0.91 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 2962 0 0 0 7990 9 0 0 25 0 1 0 487752624 13746176 2940 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3356 2940 603 41 0 3315 0
vsize: 13424
[startup+90.0021 s]
Raw data (loadavg): 0.93 0.91 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 3177 0 0 0 8990 9 0 0 25 0 1 0 487752624 14553088 3155 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3553 3155 603 41 0 3512 0
vsize: 14212
[startup+100.002 s]
Raw data (loadavg): 0.94 0.91 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 3539 0 0 0 9989 11 0 0 25 0 1 0 487752624 16056320 3517 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3920 3517 603 41 0 3879 0
vsize: 15680
[startup+110.003 s]
Raw data (loadavg): 0.95 0.91 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 3545 0 0 0 10989 11 0 0 25 0 1 0 487752624 16203776 3523 4294967295 134512640 134672761 3221224576 3221223728 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3956 3523 603 41 0 3915 0
vsize: 15824
[startup+120.003 s]
Raw data (loadavg): 0.95 0.92 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 3547 0 0 0 11989 11 0 0 25 0 1 0 487752624 16203776 3525 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3956 3525 603 41 0 3915 0
vsize: 15824
[startup+130.004 s]
Raw data (loadavg): 0.96 0.92 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 3635 0 0 0 12989 11 0 0 25 0 1 0 487752624 16474112 3613 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4022 3613 603 41 0 3981 0
vsize: 16088
[startup+140.004 s]
Raw data (loadavg): 0.97 0.92 0.88 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4573 0 0 0 13988 13 0 0 25 0 1 0 487752624 20373504 4551 4294967295 134512640 134672761 3221224576 3221223644 1074972061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4974 4551 603 41 0 4933 0
vsize: 19896
[startup+150.003 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4573 0 0 0 14988 13 0 0 25 0 1 0 487752624 20373504 4551 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4974 4551 603 41 0 4933 0
vsize: 19896
[startup+160.003 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4875 0 0 0 15987 14 0 0 25 0 1 0 487752624 21581824 4853 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4853 603 41 0 5228 0
vsize: 21076
[startup+170.003 s]
Raw data (loadavg): 0.98 0.93 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4875 0 0 0 16987 14 0 0 25 0 1 0 487752624 21581824 4853 4294967295 134512640 134672761 3221224576 3221223744 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4853 603 41 0 5228 0
vsize: 21076
[startup+180.003 s]
Raw data (loadavg): 0.98 0.93 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4875 0 0 0 17987 14 0 0 25 0 1 0 487752624 21581824 4853 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4853 603 41 0 5228 0
vsize: 21076
[startup+190.003 s]
Raw data (loadavg): 0.98 0.93 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4876 0 0 0 18988 14 0 0 25 0 1 0 487752624 21581824 4854 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4854 603 41 0 5228 0
vsize: 21076
[startup+200.003 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4876 0 0 0 19988 14 0 0 25 0 1 0 487752624 21581824 4854 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4854 603 41 0 5228 0
vsize: 21076
[startup+210.003 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4876 0 0 0 20988 14 0 0 25 0 1 0 487752624 21581824 4854 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4854 603 41 0 5228 0
vsize: 21076
[startup+220.003 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 21988 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+230.004 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 22988 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223680 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+240.003 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 23989 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+250.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 24989 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+260.004 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 25989 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+270.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 26989 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+280.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 27989 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+290.004 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 28988 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+300.003 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 29987 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+310.003 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 30987 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+320.004 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4877 0 0 0 31988 14 0 0 25 0 1 0 487752624 21581824 4855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4855 603 41 0 5228 0
vsize: 21076
[startup+330.004 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 32988 14 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+340.004 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 33988 14 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+350.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 34988 14 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+360.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 35988 14 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223760 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+370.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 36988 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+380.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 37989 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+390.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 38989 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+400.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 39989 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223760 134558859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+410.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 40989 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+420.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 41989 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+430.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 42990 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+440.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 43990 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+450.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 44990 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+460.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 45990 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+470.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 46990 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134564695 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+480.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 47991 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223760 134559482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 48991 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 49991 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 50991 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 51991 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 52991 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 53991 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 54992 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 55992 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 56992 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 57992 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 58992 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 59992 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 60993 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4878 0 0 0 61993 15 0 0 25 0 1 0 487752624 21581824 4856 4294967295 134512640 134672761 3221224576 3221223680 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5269 4856 603 41 0 5228 0
vsize: 21076
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 4900 0 0 0 62993 15 0 0 25 0 1 0 487752624 21725184 4878 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5304 4878 603 41 0 5263 0
vsize: 21216
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5430 0 0 0 63992 16 0 0 25 0 1 0 487752624 23871488 5408 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5828 5408 603 41 0 5787 0
vsize: 23312
[startup+650.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5465 0 0 0 64992 16 0 0 25 0 1 0 487752624 24006656 5443 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5861 5443 603 41 0 5820 0
vsize: 23444
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5485 0 0 0 65992 16 0 0 25 0 1 0 487752624 24170496 5463 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5463 603 41 0 5860 0
vsize: 23604
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 66992 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223760 134559594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 67992 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 68993 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 69993 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 70993 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 71993 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 72993 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223760 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+740.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 73994 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+750.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 74994 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+760.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 75994 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+770.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 76994 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 77994 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 78995 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5487 0 0 0 79995 16 0 0 25 0 1 0 487752624 24170496 5465 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5465 603 41 0 5860 0
vsize: 23604
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5489 0 0 0 80994 17 0 0 25 0 1 0 487752624 24170496 5467 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5901 5467 603 41 0 5860 0
vsize: 23604
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5489 0 0 0 81994 17 0 0 25 0 1 0 487752624 24170496 5467 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5467 603 41 0 5860 0
vsize: 23604
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5489 0 0 0 82994 17 0 0 25 0 1 0 487752624 24170496 5467 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5467 603 41 0 5860 0
vsize: 23604
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5489 0 0 0 83995 17 0 0 25 0 1 0 487752624 24170496 5467 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5467 603 41 0 5860 0
vsize: 23604
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5489 0 0 0 84995 17 0 0 25 0 1 0 487752624 24170496 5467 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5467 603 41 0 5860 0
vsize: 23604
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5489 0 0 0 85995 17 0 0 25 0 1 0 487752624 24170496 5467 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5467 603 41 0 5860 0
vsize: 23604
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5502 0 0 0 86995 17 0 0 25 0 1 0 487752624 24170496 5480 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5480 603 41 0 5860 0
vsize: 23604
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5512 0 0 0 87995 17 0 0 25 0 1 0 487752624 24170496 5490 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5490 603 41 0 5860 0
vsize: 23604
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5537 0 0 0 88995 17 0 0 25 0 1 0 487752624 24322048 5515 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5938 5515 603 41 0 5897 0
vsize: 23752
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5540 0 0 0 89996 17 0 0 25 0 1 0 487752624 24322048 5518 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5938 5518 603 41 0 5897 0
vsize: 23752
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5545 0 0 0 90996 17 0 0 25 0 1 0 487752624 24485888 5523 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5978 5523 603 41 0 5937 0
vsize: 23912
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5546 0 0 0 91996 17 0 0 25 0 1 0 487752624 24485888 5524 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5978 5524 603 41 0 5937 0
vsize: 23912
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5551 0 0 0 92996 17 0 0 25 0 1 0 487752624 24485888 5529 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5978 5529 603 41 0 5937 0
vsize: 23912
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5551 0 0 0 93996 17 0 0 25 0 1 0 487752624 24485888 5529 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5978 5529 603 41 0 5937 0
vsize: 23912
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5651 0 0 0 94996 17 0 0 25 0 1 0 487752624 24891392 5629 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6077 5629 603 41 0 6036 0
vsize: 24308
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5651 0 0 0 95997 17 0 0 25 0 1 0 487752624 24891392 5629 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6077 5629 603 41 0 6036 0
vsize: 24308
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5660 0 0 0 96997 17 0 0 25 0 1 0 487752624 24891392 5638 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6077 5638 603 41 0 6036 0
vsize: 24308
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5688 0 0 0 97997 17 0 0 25 0 1 0 487752624 25026560 5666 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6110 5666 603 41 0 6069 0
vsize: 24440
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5688 0 0 0 98997 17 0 0 25 0 1 0 487752624 25026560 5666 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6110 5666 603 41 0 6069 0
vsize: 24440
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5820 0 0 0 99997 17 0 0 25 0 1 0 487752624 25567232 5798 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6242 5798 603 41 0 6201 0
vsize: 24968
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5820 0 0 0 100997 17 0 0 25 0 1 0 487752624 25567232 5798 4294967295 134512640 134672761 3221224576 3221223672 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6242 5798 603 41 0 6201 0
vsize: 24968
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5833 0 0 0 101997 17 0 0 25 0 1 0 487752624 25714688 5811 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6278 5811 603 41 0 6237 0
vsize: 25112
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5833 0 0 0 102998 17 0 0 25 0 1 0 487752624 25714688 5811 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6278 5811 603 41 0 6237 0
vsize: 25112
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5834 0 0 0 103998 18 0 0 25 0 1 0 487752624 25714688 5812 4294967295 134512640 134672761 3221224576 3221223712 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6278 5812 603 41 0 6237 0
vsize: 25112
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5835 0 0 0 104996 18 0 0 25 0 1 0 487752624 25714688 5813 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6278 5813 603 41 0 6237 0
vsize: 25112
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5835 0 0 0 105996 18 0 0 25 0 1 0 487752624 25714688 5813 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6278 5813 603 41 0 6237 0
vsize: 25112
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5835 0 0 0 106997 18 0 0 25 0 1 0 487752624 25714688 5813 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6278 5813 603 41 0 6237 0
vsize: 25112
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 5835 0 0 0 107997 18 0 0 25 0 1 0 487752624 25714688 5813 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6278 5813 603 41 0 6237 0
vsize: 25112
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6062 0 0 0 108996 19 0 0 25 0 1 0 487752624 26513408 6040 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6473 6040 603 41 0 6432 0
vsize: 25892
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6079 0 0 0 109996 19 0 0 25 0 1 0 487752624 26660864 6057 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6509 6057 603 41 0 6468 0
vsize: 26036
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 110996 19 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223776 134557806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 111996 20 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 112996 20 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223680 134559802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 113996 20 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223776 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 114997 20 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 115997 20 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 116997 20 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 117997 20 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 118997 20 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27062
Raw data (stat): 27062 (minisat+) R 27061 10614 10613 0 -1 0 6359 0 0 0 119998 20 0 0 25 0 1 0 487752624 27860992 6337 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6802 6337 603 41 0 6761 0
vsize: 27208
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27062
Raw data (stat): 27062 (minisat+) Z 27061 10614 10613 0 -1 12 6362 0 0 0 119998 21 0 0 25 0 1 0 487752624 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.03
CPU time (s): 1200.19
CPU user time (s): 1199.98
CPU system time (s): 0.212967
CPU usage (%): 100.013
Max. virtual memory (Kb): 27208
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####