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/synthesis-ptl-cmos-circuits/normalized-c8.opb
MD5SUM	9b291040ec2b77d0bffb739c0db80d53
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1194
Optimality of the best value was proved	NO
Number of terms in the objective function	239
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	10012
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	10012
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.941856
Number of variables	239
Total number of constraints	524
Number of constraints which are clauses	520
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	4
Minimum length of a constraint	1
Maximum length of a constraint	36
Trace number 6341

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 04:22:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4762 boxname=wulflinc32 idbench=250 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9b291040ec2b77d0bffb739c0db80d53  /oldhome/oroussel/tmp/wulflinc32/normalized-c8.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc32/normalized-c8.opb /oldhome/oroussel/tmp/wulflinc32/normalized-c8.opb
IDLAUNCH: 4762
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        701596 kB
Buffers:         35396 kB
Cached:         186228 kB
SwapCached:       1212 kB
Active:         147412 kB
Inactive:       154520 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        701340 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25356 kB
Committed_AS:   173948 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:42:31 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 4762 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 519 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 |     519     2283 |     173       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1761[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:29493     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   79687   187621 |   26562       1       14    14.0 |  0.000 % |
c |       103 |   79687   187621 |   29218     103      748     7.3 |  0.008 % |
c |       253 |   78234   184318 |   32140     244     1522     6.2 |  1.474 % |
c |       478 |   78107   184025 |   35354     467    14033    30.0 |  1.618 % |
c |       816 |   78107   184025 |   38889     805    28261    35.1 |  1.618 % |
c ==============================================================================
c [1mFound solution: 1730[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:24438     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       938 |  143228   336543 |   47742     926    31530    34.0 |  1.618 % |
c |      1039 |  143228   336543 |   52516    1027    33278    32.4 |  0.954 % |
c |      1189 |  143114   336281 |   57767    1176    36705    31.2 |  1.028 % |
c |      1416 |  143114   336281 |   63544    1403    43211    30.8 |  1.028 % |
c |      1753 |  143114   336281 |   69899    1740    51933    29.8 |  1.028 % |
c |      2260 |  143086   336219 |   76888    2246    57506    25.6 |  1.042 % |
c |      3019 |  143086   336219 |   84577    3005    80511    26.8 |  1.042 % |
c |      4158 |  143055   336150 |   93035    4140   116981    28.3 |  1.059 % |
c |      5866 |  142470   334814 |  102339    5827   145040    24.9 |  1.415 % |
c |      8432 |  142236   334289 |  112573    8392   206387    24.6 |  1.536 % |
c |     12276 |  142154   334105 |  123830   12234   802916    65.6 |  1.574 % |
c ==============================================================================
c [1mFound solution: 1720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:22389     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12994 |  201030   472036 |   67010   12952   853095    65.9 |  1.574 % |
c ==============================================================================
c [1mFound solution: 1674[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13050 |  201833   474049 |   67277   13008   859122    66.0 |  1.574 % |
c |     13150 |  201833   474049 |   74004   13108   859982    65.6 |  1.158 % |
c |     13302 |  201833   474049 |   81405   13260   865311    65.3 |  1.158 % |
c |     13528 |  201833   474049 |   89545   13486   880597    65.3 |  1.158 % |
c |     13866 |  201611   473552 |   98500   13821   910726    65.9 |  1.241 % |
c |     14372 |  201592   473508 |  108350   14326   915870    63.9 |  1.249 % |
c |     15131 |  201568   473454 |  119185   15083   945763    62.7 |  1.258 % |
c |     16270 |  201544   473400 |  131103   16221  1019506    62.9 |  1.266 % |
c ==============================================================================
c [1mFound solution: 1660[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17434 |  201519   473340 |   67173   17384  1363941    78.5 |  1.266 % |
c |     17534 |  201519   473340 |   73890   17484  1366763    78.2 |  1.277 % |
c |     17684 |  201300   472844 |   81279   17627  1368663    77.6 |  1.364 % |
c |     17909 |  201300   472844 |   89407   17852  1375123    77.0 |  1.364 % |
c |     18246 |  201269   472773 |   98347   18184  1380020    75.9 |  1.378 % |
c |     18753 |  201269   472773 |  108182   18691  1389788    74.4 |  1.378 % |
c |     19515 |  201269   472773 |  119001   19453  1404838    72.2 |  1.378 % |
c |     20655 |  201269   472773 |  130901   20593  1497831    72.7 |  1.378 % |
c |     22363 |  201269   472773 |  143991   22301  1812246    81.3 |  1.378 % |
c |     24925 |  201269   472773 |  158390   24863  2042741    82.2 |  1.378 % |
c |     28769 |  200665   471398 |  174229   28642  2310458    80.7 |  1.626 % |
c ==============================================================================
c [1mFound solution: 1618[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31759 |  200972   472218 |   66990   31531  2360139    74.9 |  1.626 % |
c ==============================================================================
c [1mFound solution: 1617[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31815 |  201041   472417 |   67013   31587  2364168    74.8 |  1.626 % |
c |     31915 |  201041   472417 |   73714   31687  2368514    74.7 |  1.748 % |
c |     32067 |  201041   472417 |   81085   31839  2371888    74.5 |  1.748 % |
c |     32296 |  201041   472417 |   89194   32068  2375208    74.1 |  1.748 % |
c |     32634 |  201041   472417 |   98113   32406  2379144    73.4 |  1.748 % |
c |     33140 |  201041   472417 |  107925   32912  2388235    72.6 |  1.748 % |
c ==============================================================================
c [1mFound solution: 1614[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33221 |  201046   472430 |   67015   32993  2391482    72.5 |  1.748 % |
c |     33322 |  201046   472430 |   73716   33094  2395317    72.4 |  1.749 % |
c |     33473 |  201046   472430 |   81088   33245  2396679    72.1 |  1.749 % |
c |     33698 |  201046   472430 |   89196   33470  2399346    71.7 |  1.749 % |
c |     34035 |  201046   472430 |   98116   33807  2406228    71.2 |  1.749 % |
c |     34543 |  201046   472430 |  107928   34315  2416206    70.4 |  1.749 % |
c ==============================================================================
c [1mFound solution: 1594[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35243 |  201055   472454 |   67018   35014  2430599    69.4 |  1.749 % |
c |     35343 |  201055   472454 |   73719   35114  2437472    69.4 |  1.752 % |
c ==============================================================================
c [1mFound solution: 1586[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35405 |  201067   472484 |   67022   35176  2439108    69.3 |  1.752 % |
c |     35506 |  201067   472484 |   73724   35277  2442506    69.2 |  1.753 % |
c |     35659 |  201067   472484 |   81096   35430  2449118    69.1 |  1.753 % |
c |     35884 |  201067   472484 |   89206   35655  2454796    68.8 |  1.753 % |
c |     36221 |  201067   472484 |   98126   35992  2482545    69.0 |  1.753 % |
c |     36727 |  201067   472484 |  107939   36498  2494266    68.3 |  1.753 % |
c |     37488 |  201067   472484 |  118733   37259  2517500    67.6 |  1.754 % |
c |     38627 |  201028   472398 |  130606   38361  2559271    66.7 |  1.770 % |
c ==============================================================================
c [1mFound solution: 1561[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39401 |  200806   471900 |   66935   38949  2576059    66.1 |  1.770 % |
c |     39502 |  200806   471900 |   73628   39050  2579285    66.1 |  1.889 % |
c |     39652 |  200806   471900 |   80991   39200  2581838    65.9 |  1.889 % |
c |     39877 |  200806   471900 |   89090   39425  2604198    66.1 |  1.889 % |
c |     40217 |  200806   471900 |   97999   39765  2613128    65.7 |  1.889 % |
c |     40724 |  200806   471900 |  107799   40272  2634753    65.4 |  1.889 % |
c |     41483 |  200806   471900 |  118579   41031  2669184    65.1 |  1.889 % |
c |     42622 |  200733   471732 |  130437   42115  2725713    64.7 |  1.923 % |
c |     44330 |  200733   471732 |  143481   43823  3125826    71.3 |  1.923 % |
c |     46892 |  200733   471732 |  157829   46385  3232552    69.7 |  1.923 % |
c ==============================================================================
c [1mFound solution: 1546[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46928 |  200747   471768 |   66915   46421  3236785    69.7 |  1.923 % |
c |     47028 |  200747   471768 |   73606   46521  3238554    69.6 |  1.925 % |
c |     47179 |  200747   471768 |   80967   46672  3260816    69.9 |  1.925 % |
c |     47406 |  200747   471768 |   89063   46899  3266970    69.7 |  1.925 % |
c |     47743 |  200747   471768 |   97970   47236  3270737    69.2 |  1.925 % |
c |     48249 |  200714   471691 |  107767   47727  3325063    69.7 |  1.938 % |
c |     49008 |  200714   471691 |  118544   48486  3363237    69.4 |  1.938 % |
c |     50147 |  200714   471691 |  130398   49625  3446361    69.4 |  1.938 % |
c |     51855 |  200714   471691 |  143438   51333  3511389    68.4 |  1.938 % |
c |     54417 |  200714   471691 |  157782   53895  3985313    73.9 |  1.938 % |
c |     58261 |  200714   471691 |  173560   57739  4777709    82.7 |  1.938 % |
c |     64031 |  200714   471691 |  190916   63509  5427356    85.5 |  1.938 % |
c |     72680 |  200714   471691 |  210007   72158  6948707    96.3 |  1.938 % |
c |     85658 |  200714   471691 |  231008   85136  8788268   103.2 |  1.938 % |
c |    105121 |  200714   471691 |  254109  104599 10820565   103.4 |  1.938 % |
#### 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.83 0.94 0.90 2/53 15561
Raw data (stat): 15561 (runsolver) R 15560 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481672092 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.86 0.94 0.90 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 4472 0 0 0 987 11 0 0 25 0 1 0 481672092 20951040 4258 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5115 4258 603 41 0 5074 0
vsize: 20460
[startup+20.0022 s]
Raw data (loadavg): 0.88 0.94 0.90 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 4554 0 0 0 1986 11 0 0 25 0 1 0 481672092 21213184 4340 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5179 4340 603 41 0 5138 0
vsize: 20716
[startup+30.0029 s]
Raw data (loadavg): 0.90 0.94 0.90 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 4628 0 0 0 2986 12 0 0 25 0 1 0 481672092 21483520 4414 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5245 4414 603 41 0 5204 0
vsize: 20980
[startup+40.0037 s]
Raw data (loadavg): 0.91 0.94 0.90 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 4805 0 0 0 3985 12 0 0 25 0 1 0 481672092 22290432 4591 4294967295 134512640 134672761 3221224576 3221223760 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5442 4591 603 41 0 5401 0
vsize: 21768
[startup+50.0044 s]
Raw data (loadavg): 0.93 0.94 0.90 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 5073 0 0 0 4984 13 0 0 25 0 1 0 481672092 23355392 4859 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5702 4859 603 41 0 5661 0
vsize: 22808
[startup+60.0055 s]
Raw data (loadavg): 0.94 0.95 0.90 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 5291 0 0 0 5983 14 0 0 25 0 1 0 481672092 24289280 5077 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5930 5077 603 41 0 5889 0
vsize: 23720
[startup+70.006 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 6948 0 0 0 6977 20 0 0 25 0 1 0 481672092 34328576 6729 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 6729 603 41 0 8340 0
vsize: 33524
[startup+80.0067 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 7007 0 0 0 7977 20 0 0 25 0 1 0 481672092 34598912 6788 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8447 6788 603 41 0 8406 0
vsize: 33788
[startup+90.0075 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 7145 0 0 0 8977 20 0 0 25 0 1 0 481672092 35217408 6926 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8598 6926 603 41 0 8557 0
vsize: 34392
[startup+100.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 7495 0 0 0 9976 21 0 0 25 0 1 0 481672092 36413440 7249 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8890 7249 603 41 0 8849 0
vsize: 35560
[startup+110.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 7520 0 0 0 10976 21 0 0 25 0 1 0 481672092 36544512 7274 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8922 7274 603 41 0 8881 0
vsize: 35688
[startup+120.01 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 7631 0 0 0 11976 22 0 0 25 0 1 0 481672092 37085184 7385 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9054 7385 603 41 0 9013 0
vsize: 36216
[startup+130.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 7922 0 0 0 12975 23 0 0 25 0 1 0 481672092 38166528 7676 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9318 7676 603 41 0 9277 0
vsize: 37272
[startup+140.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8081 0 0 0 13974 24 0 0 25 0 1 0 481672092 38838272 7835 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9482 7835 603 41 0 9441 0
vsize: 37928
[startup+150.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8228 0 0 0 14974 24 0 0 25 0 1 0 481672092 39501824 7982 4294967295 134512640 134672761 3221224576 3221223712 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9644 7983 603 41 0 9603 0
vsize: 38576
[startup+160.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8362 0 0 0 15974 25 0 0 25 0 1 0 481672092 40042496 8116 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9776 8116 603 41 0 9735 0
vsize: 39104
[startup+170.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8522 0 0 0 16973 26 0 0 25 0 1 0 481672092 40583168 8276 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9908 8276 603 41 0 9867 0
vsize: 39632
[startup+180.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8651 0 0 0 17972 26 0 0 25 0 1 0 481672092 40853504 8348 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 8348 603 41 0 9933 0
vsize: 39896
[startup+190.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8721 0 0 0 18973 26 0 0 25 0 1 0 481672092 41242624 8413 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 8413 603 41 0 10028 0
vsize: 40276
[startup+200.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8814 0 0 0 19973 27 0 0 25 0 1 0 481672092 41410560 8455 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10110 8455 603 41 0 10069 0
vsize: 40440
[startup+210.018 s]
Raw data (loadavg): 1.07 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8870 0 0 0 20972 27 0 0 25 0 1 0 481672092 41676800 8511 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 8511 603 41 0 10134 0
vsize: 40700
[startup+220.018 s]
Raw data (loadavg): 1.06 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8918 0 0 0 21973 27 0 0 25 0 1 0 481672092 41943040 8559 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10240 8559 603 41 0 10199 0
vsize: 40960
[startup+230.019 s]
Raw data (loadavg): 1.05 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 8941 0 0 0 22973 27 0 0 25 0 1 0 481672092 41943040 8582 4294967295 134512640 134672761 3221224576 3221223712 134560606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10240 8582 603 41 0 10199 0
vsize: 40960
[startup+240.02 s]
Raw data (loadavg): 1.04 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 9060 0 0 0 23972 28 0 0 25 0 1 0 481672092 42225664 8628 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10309 8628 603 41 0 10268 0
vsize: 41236
[startup+250.022 s]
Raw data (loadavg): 1.04 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 9102 0 0 0 24972 28 0 0 25 0 1 0 481672092 42360832 8670 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10342 8670 603 41 0 10301 0
vsize: 41368
[startup+260.022 s]
Raw data (loadavg): 1.03 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 9144 0 0 0 25972 28 0 0 25 0 1 0 481672092 42491904 8712 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10374 8712 603 41 0 10333 0
vsize: 41496
[startup+270.023 s]
Raw data (loadavg): 1.02 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 9201 0 0 0 26972 29 0 0 25 0 1 0 481672092 42762240 8769 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10440 8769 603 41 0 10399 0
vsize: 41760
[startup+280.024 s]
Raw data (loadavg): 1.02 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 9452 0 0 0 27972 29 0 0 25 0 1 0 481672092 43692032 9020 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10667 9020 603 41 0 10626 0
vsize: 42668
[startup+290.025 s]
Raw data (loadavg): 1.02 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 9672 0 0 0 28971 30 0 0 25 0 1 0 481672092 44625920 9240 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10895 9240 603 41 0 10854 0
vsize: 43580
[startup+300.026 s]
Raw data (loadavg): 1.01 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 9801 0 0 0 29970 31 0 0 25 0 1 0 481672092 44998656 9342 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10986 9342 603 41 0 10945 0
vsize: 43944
[startup+310.027 s]
Raw data (loadavg): 1.01 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 9910 0 0 0 30970 31 0 0 25 0 1 0 481672092 45535232 9451 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11117 9451 603 41 0 11076 0
vsize: 44468
[startup+320.028 s]
Raw data (loadavg): 1.01 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 10021 0 0 0 31970 31 0 0 25 0 1 0 481672092 45940736 9562 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11216 9562 603 41 0 11175 0
vsize: 44864
[startup+330.029 s]
Raw data (loadavg): 1.01 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 10081 0 0 0 32969 32 0 0 25 0 1 0 481672092 46211072 9622 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11282 9622 603 41 0 11241 0
vsize: 45128
[startup+340.03 s]
Raw data (loadavg): 1.01 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 10257 0 0 0 33969 32 0 0 25 0 1 0 481672092 46886912 9798 4294967295 134512640 134672761 3221224576 3221223712 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11447 9798 603 41 0 11406 0
vsize: 45788
[startup+350.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 10448 0 0 0 34969 33 0 0 25 0 1 0 481672092 47693824 9989 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11644 9989 603 41 0 11603 0
vsize: 46576
[startup+360.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 10604 0 0 0 35968 34 0 0 25 0 1 0 481672092 48361472 10145 4294967295 134512640 134672761 3221224576 3221223776 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10145 603 41 0 11766 0
vsize: 47228
[startup+370.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 10826 0 0 0 36967 35 0 0 25 0 1 0 481672092 49299456 10367 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12036 10367 603 41 0 11995 0
vsize: 48144
[startup+380.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 11104 0 0 0 37966 36 0 0 25 0 1 0 481672092 50364416 10645 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12296 10645 603 41 0 12255 0
vsize: 49184
[startup+390.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 11339 0 0 0 38966 37 0 0 25 0 1 0 481672092 51310592 10880 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12527 10880 603 41 0 12486 0
vsize: 50108
[startup+400.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 11516 0 0 0 39965 38 0 0 25 0 1 0 481672092 51982336 11057 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12691 11057 603 41 0 12650 0
vsize: 50764
[startup+410.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 11615 0 0 0 40965 38 0 0 25 0 1 0 481672092 52506624 11156 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12819 11156 603 41 0 12778 0
vsize: 51276
[startup+420.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 11722 0 0 0 41965 38 0 0 25 0 1 0 481672092 52903936 11263 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12916 11263 603 41 0 12875 0
vsize: 51664
[startup+430.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 11844 0 0 0 42965 39 0 0 25 0 1 0 481672092 53313536 11385 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13016 11385 603 41 0 12975 0
vsize: 52064
[startup+440.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 11926 0 0 0 43965 39 0 0 25 0 1 0 481672092 53710848 11467 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13113 11467 603 41 0 13072 0
vsize: 52452
[startup+450.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 12050 0 0 0 44965 39 0 0 25 0 1 0 481672092 54239232 11591 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13242 11591 603 41 0 13201 0
vsize: 52968
[startup+460.041 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 12123 0 0 0 45965 40 0 0 25 0 1 0 481672092 54501376 11664 4294967295 134512640 134672761 3221224576 3221223680 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13306 11664 603 41 0 13265 0
vsize: 53224
[startup+470.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 12219 0 0 0 46964 40 0 0 25 0 1 0 481672092 54902784 11760 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13404 11760 603 41 0 13363 0
vsize: 53616
[startup+480.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 12354 0 0 0 47964 41 0 0 25 0 1 0 481672092 55435264 11895 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13534 11895 603 41 0 13493 0
vsize: 54136
[startup+490.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 12477 0 0 0 48964 41 0 0 25 0 1 0 481672092 56233984 12018 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13729 12018 603 41 0 13688 0
vsize: 54916
[startup+500.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 12630 0 0 0 49963 41 0 0 25 0 1 0 481672092 56770560 12171 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13860 12171 603 41 0 13819 0
vsize: 55440
[startup+510.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 12789 0 0 0 50963 42 0 0 25 0 1 0 481672092 57434112 12330 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14022 12330 603 41 0 13981 0
vsize: 56088
[startup+520.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 12940 0 0 0 51963 43 0 0 25 0 1 0 481672092 58105856 12481 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 12481 603 41 0 14145 0
vsize: 56744
[startup+530.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 13097 0 0 0 52962 43 0 0 25 0 1 0 481672092 58773504 12638 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14349 12638 603 41 0 14308 0
vsize: 57396
[startup+540.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 13295 0 0 0 53962 44 0 0 25 0 1 0 481672092 59572224 12836 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14544 12836 603 41 0 14503 0
vsize: 58176
[startup+550.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 13441 0 0 0 54962 44 0 0 25 0 1 0 481672092 60104704 12982 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14674 12982 603 41 0 14633 0
vsize: 58696
[startup+560.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 13611 0 0 0 55961 45 0 0 25 0 1 0 481672092 60772352 13152 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14837 13152 603 41 0 14796 0
vsize: 59348
[startup+570.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 13733 0 0 0 56960 46 0 0 25 0 1 0 481672092 61308928 13274 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14968 13274 603 41 0 14927 0
vsize: 59872
[startup+580.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 13821 0 0 0 57960 46 0 0 25 0 1 0 481672092 61714432 13362 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15067 13362 603 41 0 15026 0
vsize: 60268
[startup+590.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 13927 0 0 0 58960 46 0 0 25 0 1 0 481672092 62107648 13468 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15163 13468 603 41 0 15122 0
vsize: 60652
[startup+600.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 14064 0 0 0 59960 47 0 0 25 0 1 0 481672092 62636032 13605 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15292 13605 603 41 0 15251 0
vsize: 61168
[startup+610.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 14184 0 0 0 60960 48 0 0 25 0 1 0 481672092 63164416 13725 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15421 13725 603 41 0 15380 0
vsize: 61684
[startup+620.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 14305 0 0 0 61960 48 0 0 25 0 1 0 481672092 63696896 13846 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15551 13846 603 41 0 15510 0
vsize: 62204
[startup+630.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 14436 0 0 0 62959 48 0 0 25 0 1 0 481672092 64237568 13977 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15683 13977 603 41 0 15642 0
vsize: 62732
[startup+640.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 14601 0 0 0 63959 49 0 0 25 0 1 0 481672092 64905216 14142 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15846 14142 603 41 0 15805 0
vsize: 63384
[startup+650.057 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 14764 0 0 0 64959 50 0 0 25 0 1 0 481672092 65564672 14305 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16007 14305 603 41 0 15966 0
vsize: 64028
[startup+660.058 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 14904 0 0 0 65958 50 0 0 25 0 1 0 481672092 66088960 14445 4294967295 134512640 134672761 3221224576 3221223680 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16135 14445 603 41 0 16094 0
vsize: 64540
[startup+670.059 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15014 0 0 0 66958 51 0 0 25 0 1 0 481672092 66490368 14555 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16233 14555 603 41 0 16192 0
vsize: 64932
[startup+680.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15160 0 0 0 67958 51 0 0 25 0 1 0 481672092 67153920 14701 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16395 14701 603 41 0 16354 0
vsize: 65580
[startup+690.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15316 0 0 0 68957 52 0 0 25 0 1 0 481672092 67821568 14857 4294967295 134512640 134672761 3221224576 3221223776 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16558 14857 603 41 0 16517 0
vsize: 66232
[startup+700.061 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15447 0 0 0 69957 52 0 0 25 0 1 0 481672092 68349952 14988 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16687 14988 603 41 0 16646 0
vsize: 66748
[startup+710.062 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15553 0 0 0 70957 53 0 0 25 0 1 0 481672092 68751360 15094 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16785 15094 603 41 0 16744 0
vsize: 67140
[startup+720.063 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15658 0 0 0 71957 53 0 0 25 0 1 0 481672092 69144576 15199 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16881 15199 603 41 0 16840 0
vsize: 67524
[startup+730.063 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15729 0 0 0 72956 53 0 0 25 0 1 0 481672092 69414912 15270 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16947 15270 603 41 0 16906 0
vsize: 67788
[startup+740.064 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15778 0 0 0 73956 53 0 0 25 0 1 0 481672092 69685248 15319 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17013 15319 603 41 0 16972 0
vsize: 68052
[startup+750.065 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15859 0 0 0 74957 53 0 0 25 0 1 0 481672092 69955584 15400 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 15400 603 41 0 17038 0
vsize: 68316
[startup+760.066 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 15944 0 0 0 75957 53 0 0 25 0 1 0 481672092 70352896 15485 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17176 15485 603 41 0 17135 0
vsize: 68704
[startup+770.066 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16000 0 0 0 76957 54 0 0 25 0 1 0 481672092 70488064 15541 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17209 15541 603 41 0 17168 0
vsize: 68836
[startup+780.067 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16070 0 0 0 77957 54 0 0 25 0 1 0 481672092 70885376 15611 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17306 15611 603 41 0 17265 0
vsize: 69224
[startup+790.068 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16136 0 0 0 78957 54 0 0 25 0 1 0 481672092 71151616 15677 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17371 15677 603 41 0 17330 0
vsize: 69484
[startup+800.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16218 0 0 0 79957 54 0 0 25 0 1 0 481672092 71413760 15759 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17435 15759 603 41 0 17394 0
vsize: 69740
[startup+810.069 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16286 0 0 0 80957 54 0 0 25 0 1 0 481672092 71675904 15827 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17499 15827 603 41 0 17458 0
vsize: 69996
[startup+820.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16363 0 0 0 81957 55 0 0 25 0 1 0 481672092 72081408 15904 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17598 15904 603 41 0 17557 0
vsize: 70392
[startup+830.071 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16421 0 0 0 82956 55 0 0 25 0 1 0 481672092 72212480 15962 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17630 15962 603 41 0 17589 0
vsize: 70520
[startup+840.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16474 0 0 0 83956 56 0 0 25 0 1 0 481672092 72474624 16015 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17694 16015 603 41 0 17653 0
vsize: 70776
[startup+850.072 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16529 0 0 0 84956 56 0 0 25 0 1 0 481672092 72732672 16070 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17757 16070 603 41 0 17716 0
vsize: 71028
[startup+860.073 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16585 0 0 0 85957 56 0 0 25 0 1 0 481672092 72986624 16126 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17819 16126 603 41 0 17778 0
vsize: 71276
[startup+870.074 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16643 0 0 0 86957 56 0 0 25 0 1 0 481672092 73113600 16184 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17850 16184 603 41 0 17809 0
vsize: 71400
[startup+880.075 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16708 0 0 0 87957 56 0 0 25 0 1 0 481672092 73379840 16249 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17915 16249 603 41 0 17874 0
vsize: 71660
[startup+890.076 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16784 0 0 0 88957 57 0 0 25 0 1 0 481672092 73777152 16325 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18012 16325 603 41 0 17971 0
vsize: 72048
[startup+900.076 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16852 0 0 0 89957 57 0 0 25 0 1 0 481672092 74039296 16393 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18076 16393 603 41 0 18035 0
vsize: 72304
[startup+910.078 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 16942 0 0 0 90956 57 0 0 25 0 1 0 481672092 74424320 16483 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18170 16483 603 41 0 18129 0
vsize: 72680
[startup+920.079 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17020 0 0 0 91957 57 0 0 25 0 1 0 481672092 74690560 16561 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18235 16561 603 41 0 18194 0
vsize: 72940
[startup+930.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17102 0 0 0 92957 58 0 0 25 0 1 0 481672092 75083776 16643 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18331 16643 603 41 0 18290 0
vsize: 73324
[startup+940.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17183 0 0 0 93956 58 0 0 25 0 1 0 481672092 75350016 16724 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18396 16724 603 41 0 18355 0
vsize: 73584
[startup+950.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17262 0 0 0 94956 58 0 0 25 0 1 0 481672092 75747328 16803 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18493 16803 603 41 0 18452 0
vsize: 73972
[startup+960.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17330 0 0 0 95957 59 0 0 25 0 1 0 481672092 76013568 16871 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18558 16871 603 41 0 18517 0
vsize: 74232
[startup+970.083 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17416 0 0 0 96957 59 0 0 25 0 1 0 481672092 76300288 16957 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18628 16957 603 41 0 18587 0
vsize: 74512
[startup+980.083 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17520 0 0 0 97957 59 0 0 25 0 1 0 481672092 76693504 17061 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18724 17061 603 41 0 18683 0
vsize: 74896
[startup+990.084 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17624 0 0 0 98957 59 0 0 25 0 1 0 481672092 77221888 17165 4294967295 134512640 134672761 3221224576 3221223712 134560652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18853 17165 603 41 0 18812 0
vsize: 75412
[startup+1000.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17721 0 0 0 99957 59 0 0 25 0 1 0 481672092 77623296 17262 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18951 17262 603 41 0 18910 0
vsize: 75804
[startup+1010.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17824 0 0 0 100957 59 0 0 25 0 1 0 481672092 78073856 17365 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19061 17365 603 41 0 19020 0
vsize: 76244
[startup+1020.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 17916 0 0 0 101957 60 0 0 25 0 1 0 481672092 78344192 17457 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19127 17457 603 41 0 19086 0
vsize: 76508
[startup+1030.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 18076 0 0 0 102955 60 0 0 25 0 1 0 481672092 79007744 17617 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19289 17617 603 41 0 19248 0
vsize: 77156
[startup+1040.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 18172 0 0 0 103955 61 0 0 25 0 1 0 481672092 79409152 17713 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19387 17713 603 41 0 19346 0
vsize: 77548
[startup+1050.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 18321 0 0 0 104955 61 0 0 25 0 1 0 481672092 80068608 17862 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17862 603 41 0 19507 0
vsize: 78192
[startup+1060.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 18449 0 0 0 105955 61 0 0 25 0 1 0 481672092 80592896 17990 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19676 17990 603 41 0 19635 0
vsize: 78704
[startup+1070.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 18581 0 0 0 106955 62 0 0 25 0 1 0 481672092 81125376 18122 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19806 18122 603 41 0 19765 0
vsize: 79224
[startup+1080.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 18669 0 0 0 107955 62 0 0 25 0 1 0 481672092 81514496 18210 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19901 18210 603 41 0 19860 0
vsize: 79604
[startup+1090.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 18795 0 0 0 108955 62 0 0 25 0 1 0 481672092 82051072 18336 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20032 18336 603 41 0 19991 0
vsize: 80128
[startup+1100.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 18863 0 0 0 109955 62 0 0 25 0 1 0 481672092 82317312 18404 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20097 18404 603 41 0 20056 0
vsize: 80388
[startup+1110.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 18907 0 0 0 110955 62 0 0 25 0 1 0 481672092 82452480 18448 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20130 18448 603 41 0 20089 0
vsize: 80520
[startup+1120.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 19009 0 0 0 111955 63 0 0 25 0 1 0 481672092 82853888 18550 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20228 18550 603 41 0 20187 0
vsize: 80912
[startup+1130.09 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 19081 0 0 0 112955 63 0 0 25 0 1 0 481672092 83120128 18622 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20293 18622 603 41 0 20252 0
vsize: 81172
[startup+1140.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 19135 0 0 0 113955 63 0 0 25 0 1 0 481672092 83394560 18676 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20360 18676 603 41 0 20319 0
vsize: 81440
[startup+1150.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 19184 0 0 0 114955 63 0 0 25 0 1 0 481672092 83525632 18725 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20392 18725 603 41 0 20351 0
vsize: 81568
[startup+1160.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 19251 0 0 0 115955 64 0 0 25 0 1 0 481672092 83808256 18792 4294967295 134512640 134672761 3221224576 3221223744 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20461 18792 603 41 0 20420 0
vsize: 81844
[startup+1170.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 19364 0 0 0 116955 64 0 0 25 0 1 0 481672092 84336640 18905 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20590 18905 603 41 0 20549 0
vsize: 82360
[startup+1180.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 19429 0 0 0 117955 64 0 0 25 0 1 0 481672092 84619264 18970 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20659 18970 603 41 0 20618 0
vsize: 82636
[startup+1190.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 19486 0 0 0 118955 64 0 0 25 0 1 0 481672092 84754432 19027 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20692 19027 603 41 0 20651 0
vsize: 82768
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.98 0.91 2/53 15561
Raw data (stat): 15561 (minisat+) R 15560 7987 7986 0 -1 0 19542 0 0 0 119955 64 0 0 25 0 1 0 481672092 85024768 19083 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20758 19083 603 41 0 20717 0
vsize: 83032
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.98 0.91 1/53 15561
Raw data (stat): 15561 (minisat+) Z 15560 7987 7986 0 -1 12 19545 0 0 0 119956 68 0 0 25 0 1 0 481672092 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.15
CPU time (s): 1200.25
CPU user time (s): 1199.56
CPU system time (s): 0.686895
CPU usage (%): 100.009
Max. virtual memory (Kb): 83032
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####