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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-2.opb
MD5SUM	409f1cf0658f035df65cb61f3e4f598e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	595
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	595
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	27847
Number of constraints which are clauses	27847
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5988

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-14 02:45:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4456 boxname=wulflinc12 idbench=320 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  409f1cf0658f035df65cb61f3e4f598e  /oldhome/oroussel/tmp/wulflinc12/normalized-frb35-17-2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc12/normalized-frb35-17-2.opb /oldhome/oroussel/tmp/wulflinc12/normalized-frb35-17-2.opb
IDLAUNCH: 4456
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        904096 kB
Buffers:         35840 kB
Cached:          75324 kB
SwapCached:         16 kB
Active:          62236 kB
Inactive:        51768 kB
HighTotal:      131008 kB
HighFree:        51856 kB
LowTotal:       903652 kB
LowFree:        852240 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11164 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:06:01 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 4456 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27847 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 |   27847    55694 |    9282       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56112   122082 |   18704       0        0     nan |  0.000 % |
c |       100 |   55441   120669 |   20574      62      485     7.8 |  1.950 % |
c |       252 |   54383   118381 |   22631     186     1801     9.7 |  5.130 % |
c |       477 |   53349   116119 |   24895     313     3077     9.8 |  8.306 % |
c |       814 |   51759   112535 |   27384     516     5065     9.8 | 13.461 % |
c |      1321 |   49950   108452 |   30122     920     9543    10.4 | 19.341 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1658 |   48453   105089 |   16151    1166    13758    11.8 | 19.341 % |
c |      1758 |   48207   104544 |   17766    1257    15573    12.4 | 25.098 % |
c |      1908 |   47653   103297 |   19542    1386    16993    12.3 | 26.885 % |
c |      2133 |   47022   101840 |   21496    1582    20176    12.8 | 29.018 % |
c |      2471 |   45334    97977 |   23646    1783    22714    12.7 | 34.745 % |
c |      2977 |   43116    92786 |   26011    2128    28051    13.2 | 41.789 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3108 |   42804    92166 |   14268    2242    29536    13.2 | 41.789 % |
c |      3208 |   42633    91773 |   15694    2311    32120    13.9 | 43.581 % |
c |      3358 |   42086    90483 |   17264    2410    34663    14.4 | 45.442 % |
c |      3583 |   41186    88373 |   18990    2527    36936    14.6 | 48.512 % |
c |      3920 |   39875    85257 |   20889    2675    39865    14.9 | 53.073 % |
c |      4427 |   38250    81393 |   22978    2937    45919    15.6 | 58.815 % |
c |      5186 |   37415    79400 |   25276    3573    58638    16.4 | 61.715 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5777 |   36536    77244 |   12178    3923    69803    17.8 | 61.715 % |
c |      5877 |   36375    76873 |   13395    4009    70834    17.7 | 65.308 % |
c |      6027 |   36111    76265 |   14735    4119    72852    17.7 | 66.182 % |
c |      6252 |   35833    75598 |   16208    4304    78604    18.3 | 67.328 % |
c |      6590 |   35525    74869 |   17829    4581    87877    19.2 | 68.259 % |
c |      7096 |   35132    73939 |   19612    5015   102250    20.4 | 69.626 % |
c |      7855 |   35004    73641 |   21574    5721   119858    21.0 | 70.063 % |
c |      8994 |   34621    72729 |   23731    6710   156327    23.3 | 71.405 % |
c |     10702 |   34449    72319 |   26104    8303   266846    32.1 | 72.007 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10930 |   34398    72230 |   11466    8491   276955    32.6 | 72.007 % |
c |     11030 |   34307    72002 |   12612    8543   279040    32.7 | 72.564 % |
c |     11180 |   34307    72002 |   13873    8693   286044    32.9 | 72.564 % |
c |     11405 |   34227    71812 |   15261    8862   292699    33.0 | 72.846 % |
c |     11743 |   33985    71231 |   16787    9032   296460    32.8 | 73.704 % |
c |     12250 |   33985    71231 |   18466    9539   330834    34.7 | 73.704 % |
c |     13010 |   33963    71183 |   20312   10270   353365    34.4 | 73.770 % |
c |     14149 |   33552    70232 |   22343   11249   423515    37.6 | 75.141 % |
c |     15857 |   33222    69433 |   24578   12762   568784    44.6 | 76.291 % |
c |     18419 |   33120    69188 |   27036   15273   761555    49.9 | 76.651 % |
c |     22263 |   32930    68727 |   29739   18985  1120606    59.0 | 77.344 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26467 |   32657    68028 |   10885   22867  1465252    64.1 | 77.344 % |
c |     26567 |   32647    68006 |   11973   22966  1468382    63.9 | 78.332 % |
c |     26717 |   32647    68006 |   13170   23116  1476425    63.9 | 78.332 % |
c |     26942 |   32647    68006 |   14487   23341  1495373    64.1 | 78.332 % |
c |     27279 |   32477    67592 |   15936   23347  1512616    64.8 | 78.938 % |
c |     27785 |   32364    67313 |   17530   23764  1543363    64.9 | 79.364 % |
c |     28544 |   32254    67045 |   19283   24353  1597203    65.6 | 79.764 % |
c |     29683 |   32254    67045 |   21211   25492  1710400    67.1 | 79.764 % |
c |     31391 |   32254    67045 |   23332   27200  1919412    70.6 | 79.764 % |
c |     33955 |   32254    67045 |   25666   29764  2101826    70.6 | 79.764 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35137 |   31980    66414 |   10660   30812  2169138    70.4 | 79.764 % |
c |     35238 |   31946    66328 |   11726   15491   930133    60.0 | 80.939 % |
c |     35389 |   31915    66258 |   12898   15639   935925    59.8 | 81.041 % |
c |     35614 |   31915    66258 |   14188   15864   948886    59.8 | 81.041 % |
c |     35951 |   31915    66258 |   15607   16201   965361    59.6 | 81.041 % |
c |     36458 |   31915    66258 |   17168   16708   996138    59.6 | 81.041 % |
c |     37217 |   31915    66258 |   18884   17467  1044393    59.8 | 81.041 % |
c |     38357 |   31910    66247 |   20773   18600  1113004    59.8 | 81.056 % |
c |     40065 |   31845    66095 |   22850   20288  1216954    60.0 | 81.276 % |
c |     42627 |   31804    65994 |   25135   22834  1375865    60.3 | 81.429 % |
c |     46471 |   31804    65994 |   27649   26678  1735048    65.0 | 81.429 % |
c |     52237 |   31510    65286 |   30414   32374  2209723    68.3 | 82.477 % |
c |     60886 |   31481    65217 |   33455   40961  2771939    67.7 | 82.579 % |
c |     73860 |   31477    65205 |   36801   19710   946500    48.0 | 82.600 % |
c |     93322 |   31477    65205 |   40481   39172  2462580    62.9 | 82.600 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98887 |   31443    65100 |   10481   44676  2833202    63.4 | 82.600 % |
c |     98987 |   31443    65100 |   11529   17731   914127    51.6 | 82.724 % |
c |     99137 |   31443    65100 |   12682   17881   921601    51.5 | 82.724 % |
c |     99362 |   31405    65004 |   13950   18104   938348    51.8 | 82.867 % |
c |     99699 |   31381    64946 |   15345   18412   962309    52.3 | 82.954 % |
c |    100205 |   31381    64946 |   16879   18918  1006461    53.2 | 82.954 % |
c |    100964 |   31370    64919 |   18567   19674  1054745    53.6 | 82.995 % |
c |    102103 |   31370    64919 |   20424   20813  1143158    54.9 | 82.995 % |
c |    103813 |   31365    64908 |   22466   22519  1262523    56.1 | 83.011 % |
c |    106376 |   31365    64908 |   24713   25082  1418165    56.5 | 83.011 % |
c |    110222 |   31365    64908 |   27185   28928  1703939    58.9 | 83.011 % |
c |    115988 |   31330    64825 |   29903   34689  2037716    58.7 | 83.133 % |
c |    124637 |   31284    64708 |   32893   43252  2666638    61.7 | 83.307 % |
c |    137612 |   31239    64605 |   36183   22486   988221    43.9 | 83.450 % |
c |    157073 |   31239    64605 |   39801   41947  2056155    49.0 | 83.450 % |
c |    186265 |   31236    64598 |   43781   31773  1941768    61.1 | 83.460 % |
c |    230054 |   31231    64587 |   48159   32261  2906002    90.1 | 83.476 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    278557 |   31244    64621 |   10414   32296  2237077    69.3 | 83.476 % |
c |    278658 |   31244    64621 |   11455   16249   954352    58.7 | 83.452 % |
c |    278809 |   31244    64621 |   12600   16400   966097    58.9 | 83.452 % |
c |    279034 |   31244    64621 |   13861   16625   981948    59.1 | 83.452 % |
c |    279372 |   31244    64621 |   15247   16963  1000566    59.0 | 83.452 % |
c |    279878 |   31244    64621 |   16771   17469  1034794    59.2 | 83.452 % |
c |    280638 |   31244    64621 |   18449   18229  1067205    58.5 | 83.452 % |
c |    281777 |   31244    64621 |   20293   19368  1125638    58.1 | 83.452 % |
c |    283486 |   31244    64621 |   22323   21077  1208886    57.4 | 83.452 % |
c |    286048 |   31244    64621 |   24555   23639  1365631    57.8 | 83.452 % |
c |    289893 |   31244    64621 |   27011   27484  1608741    58.5 | 83.452 % |
c |    295659 |   31207    64527 |   29712   33206  1964370    59.2 | 83.595 % |
c |    304308 |   31207    64527 |   32683   41855  2460979    58.8 | 83.595 % |
c |    317282 |   31197    64503 |   35951   22333   712494    31.9 | 83.630 % |
c |    336743 |   31197    64503 |   39547   41794  1397205    33.4 | 83.630 % |
c |    365935 |   31193    64493 |   43501   34344   952519    27.7 | 83.646 % |
c |    409725 |   31143    64373 |   47852   34709  1222470    35.2 | 83.824 % |
c |    475409 |   31136    64358 |   52637   54302  1647686    30.3 | 83.845 % |
c |    573935 |   31106    64290 |   57900   50437  1608080    31.9 | 83.942 % |
#### 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.94 0.98 0.92 2/54 30709
Raw data (stat): 30709 (runsolver) R 30708 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422873255 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0003 s]
Raw data (loadavg): 1.11 1.01 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 2264 0 0 0 993 5 0 0 25 0 1 0 422873255 11472896 2235 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2801 2235 603 41 0 2760 0
vsize: 11204
[startup+20.0011 s]
Raw data (loadavg): 1.09 1.01 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 2389 0 0 0 1992 6 0 0 25 0 1 0 422873255 12005376 2360 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2931 2360 603 41 0 2890 0
vsize: 11724
[startup+30.0014 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 3036 0 0 0 2990 8 0 0 25 0 1 0 422873255 14725120 3007 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3007 603 41 0 3554 0
vsize: 14380
[startup+40.0027 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 3707 0 0 0 3987 11 0 0 25 0 1 0 422873255 17506304 3678 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4274 3678 603 41 0 4233 0
vsize: 17096
[startup+50.0036 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 4159 0 0 0 4985 13 0 0 25 0 1 0 422873255 19374080 4130 4294967295 134512640 134672761 3221224560 3221223800 134558237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4730 4130 603 41 0 4689 0
vsize: 18920
[startup+60.003 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 4645 0 0 0 5983 15 0 0 25 0 1 0 422873255 21237760 4616 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5185 4616 603 41 0 5144 0
vsize: 20740
[startup+70.0043 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 4664 0 0 0 6983 15 0 0 25 0 1 0 422873255 21372928 4635 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5218 4635 603 41 0 5177 0
vsize: 20872
[startup+80.0054 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 4664 0 0 0 7982 16 0 0 25 0 1 0 422873255 21372928 4635 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5218 4635 603 41 0 5177 0
vsize: 20872
[startup+90.0055 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 4830 0 0 0 8982 16 0 0 25 0 1 0 422873255 22175744 4801 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5414 4801 603 41 0 5373 0
vsize: 21656
[startup+100.006 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 5217 0 0 0 9981 17 0 0 25 0 1 0 422873255 23781376 5188 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5806 5188 603 41 0 5765 0
vsize: 23224
[startup+110.007 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 5572 0 0 0 10979 19 0 0 25 0 1 0 422873255 25116672 5543 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6132 5543 603 41 0 6091 0
vsize: 24528
[startup+120.007 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 5877 0 0 0 11978 20 0 0 25 0 1 0 422873255 26451968 5848 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6458 5848 603 41 0 6417 0
vsize: 25832
[startup+130.007 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6159 0 0 0 12977 21 0 0 25 0 1 0 422873255 27512832 6130 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6717 6130 603 41 0 6676 0
vsize: 26868
[startup+140.008 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6160 0 0 0 13977 21 0 0 25 0 1 0 422873255 27512832 6131 4294967295 134512640 134672761 3221224560 3221223664 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6717 6131 603 41 0 6676 0
vsize: 26868
[startup+150.008 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6160 0 0 0 14978 21 0 0 25 0 1 0 422873255 27512832 6131 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6717 6131 603 41 0 6676 0
vsize: 26868
[startup+160.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6160 0 0 0 15978 21 0 0 25 0 1 0 422873255 27512832 6131 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6717 6131 603 41 0 6676 0
vsize: 26868
[startup+170.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6160 0 0 0 16978 21 0 0 25 0 1 0 422873255 27512832 6131 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6717 6131 603 41 0 6676 0
vsize: 26868
[startup+180.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6160 0 0 0 17978 21 0 0 25 0 1 0 422873255 27512832 6131 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6717 6131 603 41 0 6676 0
vsize: 26868
[startup+190.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 18978 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+200.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 19978 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+210.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 20979 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+220.011 s]
Raw data (loadavg): 1.15 1.03 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 21979 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+230.01 s]
Raw data (loadavg): 1.13 1.03 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 22979 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223744 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+240.011 s]
Raw data (loadavg): 1.11 1.03 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 23979 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+250.011 s]
Raw data (loadavg): 1.09 1.03 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 24979 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+260.011 s]
Raw data (loadavg): 1.08 1.03 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 25980 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+270.011 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 26980 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223744 134559422 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+280.012 s]
Raw data (loadavg): 1.05 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 27980 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+290.012 s]
Raw data (loadavg): 1.05 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 28980 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+300.012 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 29980 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+310.012 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6180 0 0 0 30980 21 0 0 25 0 1 0 422873255 27672576 6151 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6151 603 41 0 6715 0
vsize: 27024
[startup+320.012 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6183 0 0 0 31981 21 0 0 25 0 1 0 422873255 27672576 6154 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6756 6154 603 41 0 6715 0
vsize: 27024
[startup+330.013 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6209 0 0 0 32981 21 0 0 25 0 1 0 422873255 27803648 6180 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6788 6180 603 41 0 6747 0
vsize: 27152
[startup+340.013 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6209 0 0 0 33981 21 0 0 25 0 1 0 422873255 27803648 6180 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6788 6180 603 41 0 6747 0
vsize: 27152
[startup+350.013 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6209 0 0 0 34981 21 0 0 25 0 1 0 422873255 27803648 6180 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6788 6180 603 41 0 6747 0
vsize: 27152
[startup+360.013 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6209 0 0 0 35981 21 0 0 25 0 1 0 422873255 27803648 6180 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6788 6180 603 41 0 6747 0
vsize: 27152
[startup+370.014 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6214 0 0 0 36981 21 0 0 25 0 1 0 422873255 27803648 6185 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6788 6185 603 41 0 6747 0
vsize: 27152
[startup+380.014 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6305 0 0 0 37982 21 0 0 25 0 1 0 422873255 28196864 6276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6884 6276 603 41 0 6843 0
vsize: 27536
[startup+390.015 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 6715 0 0 0 38981 22 0 0 25 0 1 0 422873255 29929472 6686 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7307 6686 603 41 0 7266 0
vsize: 29228
[startup+400.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7113 0 0 0 39980 24 0 0 25 0 1 0 422873255 31539200 7084 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7700 7084 603 41 0 7659 0
vsize: 30800
[startup+410.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7558 0 0 0 40979 25 0 0 25 0 1 0 422873255 33386496 7529 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8151 7529 603 41 0 8110 0
vsize: 32604
[startup+420.015 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7837 0 0 0 41977 26 0 0 25 0 1 0 422873255 34451456 7808 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7808 603 41 0 8370 0
vsize: 33644
[startup+430.016 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7837 0 0 0 42978 26 0 0 25 0 1 0 422873255 34451456 7808 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7808 603 41 0 8370 0
vsize: 33644
[startup+440.017 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7837 0 0 0 43978 26 0 0 25 0 1 0 422873255 34451456 7808 4294967295 134512640 134672761 3221224560 3221223760 134557959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7808 603 41 0 8370 0
vsize: 33644
[startup+450.018 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7837 0 0 0 44978 26 0 0 25 0 1 0 422873255 34451456 7808 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7808 603 41 0 8370 0
vsize: 33644
[startup+460.017 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7837 0 0 0 45978 26 0 0 25 0 1 0 422873255 34451456 7808 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7808 603 41 0 8370 0
vsize: 33644
[startup+470.018 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7837 0 0 0 46979 26 0 0 25 0 1 0 422873255 34451456 7808 4294967295 134512640 134672761 3221224560 3221223664 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7808 603 41 0 8370 0
vsize: 33644
[startup+480.018 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7837 0 0 0 47979 26 0 0 25 0 1 0 422873255 34451456 7808 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7808 603 41 0 8370 0
vsize: 33644
[startup+490.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7837 0 0 0 48979 26 0 0 25 0 1 0 422873255 34451456 7808 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7808 603 41 0 8370 0
vsize: 33644
[startup+500.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 7837 0 0 0 49979 26 0 0 25 0 1 0 422873255 34451456 7808 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7808 603 41 0 8370 0
vsize: 33644
[startup+510.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8145 0 0 0 50979 27 0 0 25 0 1 0 422873255 35782656 8116 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8736 8116 603 41 0 8695 0
vsize: 34944
[startup+520.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8422 0 0 0 51977 28 0 0 25 0 1 0 422873255 36843520 8393 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8995 8393 603 41 0 8954 0
vsize: 35980
[startup+530.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8689 0 0 0 52976 30 0 0 25 0 1 0 422873255 38178816 8660 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9321 8660 603 41 0 9280 0
vsize: 37284
[startup+540.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 53976 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+550.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 54976 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+560.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 55976 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+570.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 56976 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+580.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 57975 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+590.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 58976 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+600.023 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 59976 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+610.023 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 60976 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+620.023 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 61976 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+630.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 62976 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+640.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 63977 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+650.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 64977 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+660.024 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 65977 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+670.025 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 66977 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+680.025 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 67977 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+690.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 68977 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+700.025 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 69978 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+710.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 70978 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+720.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 71978 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223744 134559272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+730.026 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 72978 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+740.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8721 0 0 0 73978 30 0 0 25 0 1 0 422873255 38313984 8692 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8692 603 41 0 9313 0
vsize: 37416
[startup+750.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 74979 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+760.027 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 75979 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+770.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 76979 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+780.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 77979 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+790.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 78979 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+800.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 79979 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+810.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 80980 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+820.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 81980 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+830.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 82980 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+840.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 30709
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 83980 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+850.034 s]
Raw data (loadavg): 1.08 1.02 0.95 3/58 30762
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 84981 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+860.034 s]
Raw data (loadavg): 1.07 1.02 0.95 2/54 30762
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 85981 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+870.035 s]
Raw data (loadavg): 1.06 1.01 0.95 2/54 30762
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 86981 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223664 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+880.034 s]
Raw data (loadavg): 1.05 1.01 0.95 2/54 30762
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 87981 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+890.035 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 30762
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 88982 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+900.035 s]
Raw data (loadavg): 1.03 1.01 0.95 2/54 30762
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 89982 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+910.035 s]
Raw data (loadavg): 1.03 1.01 0.95 2/54 30762
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 90982 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+920.036 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 30762
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 91982 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+930.036 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 92982 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223720 134560076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+940.037 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 93982 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+950.037 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 94983 30 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+960.037 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 95982 31 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+970.038 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8722 0 0 0 96981 31 0 0 25 0 1 0 422873255 38313984 8693 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8693 603 41 0 9313 0
vsize: 37416
[startup+980.038 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8723 0 0 0 97981 31 0 0 25 0 1 0 422873255 38313984 8694 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8694 603 41 0 9313 0
vsize: 37416
[startup+990.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 98982 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 99982 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 100982 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 101982 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 102982 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 103982 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 104983 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 105983 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 106983 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8726 0 0 0 107983 31 0 0 25 0 1 0 422873255 38313984 8697 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8697 603 41 0 9313 0
vsize: 37416
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 108983 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 109984 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 110984 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 111984 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 112984 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 113984 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 114985 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 115983 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 116982 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30764
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 117982 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30766
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8727 0 0 0 118982 31 0 0 25 0 1 0 422873255 38313984 8698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8698 603 41 0 9313 0
vsize: 37416
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 30766
Raw data (stat): 30709 (minisat+) R 30708 25285 25284 0 -1 0 8731 0 0 0 119982 31 0 0 25 0 1 0 422873255 38313984 8702 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9354 8702 603 41 0 9313 0
vsize: 37416
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 30766
Raw data (stat): 30709 (minisat+) Z 30708 25285 25284 0 -1 12 8734 0 0 0 119982 33 0 0 25 0 1 0 422873255 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.06
CPU time (s): 1200.16
CPU user time (s): 1199.83
CPU system time (s): 0.334949
CPU usage (%): 100.008
Max. virtual memory (Kb): 37416
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####