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-4.opb
MD5SUM	e3892e1941a878802a8ccbbd36201a02
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-27
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	27842
Number of constraints which are clauses	27842
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 6366

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        854408 kB
Buffers:         35680 kB
Cached:         124636 kB
SwapCached:        164 kB
Active:          55716 kB
Inactive:       107640 kB
HighTotal:      131008 kB
HighFree:         2744 kB
LowTotal:       903652 kB
LowFree:        851664 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11300 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:58:12 (client local time) WITH STATUS 10 IN 1200.03 SECONDS
stats: 4834 7 1200.03 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 27842 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 |   27842    55684 |    9280       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -26[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 |   84684   188766 |   28228       0        0     nan |  0.000 % |
c |       100 |   84609   188598 |   31050      99      726     7.3 |  0.129 % |
c |       250 |   83830   186820 |   34155     226     1296     5.7 |  1.313 % |
c |       475 |   82570   183967 |   37571     422     2933     7.0 |  3.136 % |
c |       812 |   80088   178283 |   41328     694     4917     7.1 |  6.996 % |
c |      1318 |   74964   166495 |   45461    1001     8482     8.5 | 15.207 % |
c |      2077 |   66450   146830 |   50007    1508    14025     9.3 | 29.153 % |
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 |      3051 |   56951   124665 |   18983    2012    18294     9.1 | 29.153 % |
c |      3151 |   55838   122063 |   20881    2063    19231     9.3 | 47.587 % |
c |      3301 |   53608   116890 |   22969    2070    19206     9.3 | 51.379 % |
c |      3526 |   52210   113607 |   25266    2202    19821     9.0 | 53.997 % |
c |      3863 |   51409   111740 |   27793    2480    22302     9.0 | 55.227 % |
c |      4370 |   49609   107540 |   30572    2821    25453     9.0 | 58.334 % |
c |      5129 |   47267   102054 |   33629    3299    30360     9.2 | 62.460 % |
c |      6268 |   43210    92484 |   36992    3735    37572    10.1 | 69.688 % |
c |      7978 |   41063    87456 |   40691    4967    73222    14.7 | 73.542 % |
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 |      9434 |   38575    81578 |   12858    5590    91427    16.4 | 73.542 % |
c |      9534 |   38575    81578 |   14143    5690    95682    16.8 | 78.025 % |
c |      9686 |   38575    81578 |   15558    5842    99646    17.1 | 78.025 % |
c |      9911 |   38569    81564 |   17113    6064   106235    17.5 | 78.035 % |
c |     10248 |   38484    81361 |   18825    6329   122955    19.4 | 78.194 % |
c |     10755 |   38262    80844 |   20707    6733   139254    20.7 | 78.575 % |
c |     11514 |   38079    80416 |   22778    7404   161761    21.8 | 78.899 % |
c |     12653 |   36922    77692 |   25056    7897   185797    23.5 | 80.962 % |
c |     14361 |   36807    77423 |   27562    9567   275163    28.8 | 81.168 % |
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 |     15818 |   36851    77537 |   12283   11018   378811    34.4 | 81.168 % |
c |     15918 |   36809    77436 |   13511   11090   382124    34.5 | 81.220 % |
c |     16068 |   36633    77024 |   14862   11001   381451    34.7 | 81.543 % |
c |     16293 |   36633    77024 |   16348   11226   392682    35.0 | 81.543 % |
c |     16630 |   36581    76900 |   17983   11512   405852    35.3 | 81.641 % |
c |     17136 |   36581    76900 |   19781   12018   439551    36.6 | 81.641 % |
c |     17895 |   36581    76900 |   21760   12777   495976    38.8 | 81.641 % |
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 |     17978 |   36547    76799 |   12182   12785   493808    38.6 | 81.641 % |
c |     18078 |   36537    76776 |   13400   12866   497350    38.7 | 81.694 % |
c |     18229 |   36537    76776 |   14740   13017   504172    38.7 | 81.694 % |
c |     18454 |   36537    76776 |   16214   13242   518882    39.2 | 81.694 % |
c |     18791 |   36537    76776 |   17835   13579   532553    39.2 | 81.694 % |
c |     19297 |   36537    76776 |   19619   14085   564031    40.0 | 81.694 % |
c |     20058 |   36537    76776 |   21581   14846   622922    42.0 | 81.694 % |
c |     21197 |   36454    76585 |   23739   15970   704866    44.1 | 81.828 % |
c |     22905 |   36355    76354 |   26113   17591   798841    45.4 | 82.002 % |
c |     25468 |   36355    76354 |   28724   20154  1011995    50.2 | 82.002 % |
c |     29312 |   36355    76354 |   31596   23998  1315489    54.8 | 82.002 % |
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 |     31756 |   36423    76526 |   12141   26442  1479534    56.0 | 82.002 % |
c |     31856 |   36259    76143 |   13355   26515  1483078    55.9 | 82.268 % |
c |     32006 |   36233    76083 |   14690   26600  1488822    56.0 | 82.309 % |
c |     32231 |   36217    76046 |   16159   26820  1493796    55.7 | 82.334 % |
c |     32568 |   35758    74968 |   17775   26685  1505319    56.4 | 83.163 % |
c |     33074 |   35758    74968 |   19553   27191  1531390    56.3 | 83.163 % |
c |     33834 |   35758    74968 |   21508   27951  1574471    56.3 | 83.163 % |
c |     34973 |   35758    74968 |   23659   29090  1616999    55.6 | 83.163 % |
c |     36681 |   35669    74761 |   26025   30640  1702617    55.6 | 83.311 % |
c |     39243 |   35669    74761 |   28627   33202  1893063    57.0 | 83.311 % |
c |     43087 |   35669    74761 |   31490   37046  2275172    61.4 | 83.311 % |
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 |     47181 |   35531    74428 |   11843   40918  2516498    61.5 | 83.311 % |
c |     47281 |   35531    74428 |   13027   16632   931293    56.0 | 83.538 % |
c |     47431 |   35531    74428 |   14330   16782   936127    55.8 | 83.538 % |
c |     47656 |   35531    74428 |   15763   17007   952014    56.0 | 83.538 % |
c |     47993 |   35531    74428 |   17339   17344   976780    56.3 | 83.538 % |
c |     48499 |   35531    74428 |   19073   17850   989720    55.4 | 83.538 % |
c |     49258 |   35531    74428 |   20980   18609  1034408    55.6 | 83.538 % |
c |     50398 |   35531    74428 |   23078   19749  1102471    55.8 | 83.538 % |
c |     52106 |   35531    74428 |   25386   21457  1250589    58.3 | 83.538 % |
c |     54668 |   35511    74382 |   27925   23965  1412788    59.0 | 83.569 % |
c |     58512 |   35491    74335 |   30717   27801  1704707    61.3 | 83.604 % |
c |     64278 |   35247    73760 |   33789   33360  2022945    60.6 | 84.065 % |
c |     72928 |   35232    73727 |   37168   42009  2490240    59.3 | 84.085 % |
c |     85902 |   35232    73727 |   40885   54983  3108642    56.5 | 84.085 % |
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 |     96545 |   35269    73817 |   11756   24248   979273    40.4 | 84.085 % |
c |     96645 |   35269    73817 |   12931   24348   983292    40.4 | 84.045 % |
c |     96795 |   35269    73817 |   14224   24498   988636    40.4 | 84.045 % |
c |     97020 |   35269    73817 |   15647   24723   998921    40.4 | 84.045 % |
c |     97357 |   35269    73817 |   17211   25060  1013858    40.5 | 84.045 % |
c |     97865 |   35269    73817 |   18933   25568  1035205    40.5 | 84.045 % |
c |     98625 |   35269    73817 |   20826   26328  1082027    41.1 | 84.045 % |
c |     99766 |   35269    73817 |   22909   27469  1155041    42.0 | 84.045 % |
c |    101474 |   35269    73817 |   25200   29177  1235136    42.3 | 84.045 % |
c |    104036 |   35269    73817 |   27720   31739  1361837    42.9 | 84.045 % |
c |    107880 |   35269    73817 |   30492   35583  1525149    42.9 | 84.045 % |
c |    113647 |   35269    73817 |   33541   41350  1753319    42.4 | 84.045 % |
c |    122297 |   35263    73803 |   36895   49998  2104149    42.1 | 84.055 % |
c |    135272 |   35263    73803 |   40584   26892   797013    29.6 | 84.055 % |
c |    154733 |   35106    73434 |   44643   46333  1585541    34.2 | 84.341 % |
c |    183925 |   34938    73037 |   49107   30959   848438    27.4 | 84.663 % |
c |    227714 |   34918    72990 |   54018   29011   764428    26.3 | 84.699 % |
c |    293398 |   34845    72817 |   59420   44869  1306310    29.1 | 84.842 % |
c |    391924 |   34845    72817 |   65362   33075   842623    25.5 | 84.842 % |
c |    539713 |   34750    72586 |   71898   55691  1547900    27.8 | 85.036 % |
#### 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.91 0.95 0.90 2/54 2150
Raw data (stat): 2150 (runsolver) R 2149 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423556489 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99945 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 2350 0 0 0 993 4 0 0 25 0 1 0 423556489 11939840 2321 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2915 2321 603 41 0 2874 0
vsize: 11660
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 2424 0 0 0 1993 5 0 0 25 0 1 0 423556489 12275712 2395 4294967295 134512640 134672761 3221224560 3221223652 1075351210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2997 2395 603 41 0 2956 0
vsize: 11988
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 2916 0 0 0 2991 6 0 0 25 0 1 0 423556489 14290944 2887 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3489 2887 603 41 0 3448 0
vsize: 13956
[startup+40.0003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 3563 0 0 0 3989 8 0 0 25 0 1 0 423556489 16986112 3534 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4147 3534 603 41 0 4106 0
vsize: 16588
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 4019 0 0 0 4987 10 0 0 25 0 1 0 423556489 18845696 3990 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4601 3990 603 41 0 4560 0
vsize: 18404
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 4379 0 0 0 5986 11 0 0 25 0 1 0 423556489 20316160 4350 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4960 4350 603 41 0 4919 0
vsize: 19840
[startup+70.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 4900 0 0 0 6983 14 0 0 25 0 1 0 423556489 22581248 4871 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5513 4871 603 41 0 5472 0
vsize: 22052
[startup+80.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 5205 0 0 0 7982 15 0 0 25 0 1 0 423556489 23805952 5176 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5812 5176 603 41 0 5771 0
vsize: 23248
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 5205 0 0 0 8982 15 0 0 25 0 1 0 423556489 23805952 5176 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5812 5176 603 41 0 5771 0
vsize: 23248
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 5205 0 0 0 9981 16 0 0 25 0 1 0 423556489 23805952 5176 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5812 5176 603 41 0 5771 0
vsize: 23248
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 5205 0 0 0 10981 16 0 0 25 0 1 0 423556489 23805952 5176 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5812 5176 603 41 0 5771 0
vsize: 23248
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 5246 0 0 0 11981 16 0 0 25 0 1 0 423556489 24072192 5217 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5877 5217 603 41 0 5836 0
vsize: 23508
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 5508 0 0 0 12980 17 0 0 25 0 1 0 423556489 25137152 5479 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6137 5479 603 41 0 6096 0
vsize: 24548
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 5716 0 0 0 13979 18 0 0 25 0 1 0 423556489 25935872 5687 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6332 5687 603 41 0 6291 0
vsize: 25328
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 5904 0 0 0 14978 19 0 0 25 0 1 0 423556489 26730496 5875 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6526 5875 603 41 0 6485 0
vsize: 26104
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6125 0 0 0 15976 20 0 0 25 0 1 0 423556489 27521024 6096 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6719 6096 603 41 0 6678 0
vsize: 26876
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6158 0 0 0 16976 20 0 0 25 0 1 0 423556489 27652096 6129 4294967295 134512640 134672761 3221224560 3221223744 134559381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6751 6129 603 41 0 6710 0
vsize: 27004
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6164 0 0 0 17976 21 0 0 25 0 1 0 423556489 27807744 6135 4294967295 134512640 134672761 3221224560 3221223744 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6135 603 41 0 6748 0
vsize: 27156
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6164 0 0 0 18976 21 0 0 25 0 1 0 423556489 27807744 6135 4294967295 134512640 134672761 3221224560 3221223664 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6135 603 41 0 6748 0
vsize: 27156
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6166 0 0 0 19975 22 0 0 25 0 1 0 423556489 27807744 6137 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6137 603 41 0 6748 0
vsize: 27156
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6166 0 0 0 20975 22 0 0 25 0 1 0 423556489 27807744 6137 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6137 603 41 0 6748 0
vsize: 27156
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6166 0 0 0 21974 22 0 0 25 0 1 0 423556489 27807744 6137 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6137 603 41 0 6748 0
vsize: 27156
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6172 0 0 0 22974 23 0 0 25 0 1 0 423556489 27807744 6143 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6143 603 41 0 6748 0
vsize: 27156
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6173 0 0 0 23973 23 0 0 25 0 1 0 423556489 27807744 6144 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6144 603 41 0 6748 0
vsize: 27156
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6173 0 0 0 24973 23 0 0 25 0 1 0 423556489 27807744 6144 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6144 603 41 0 6748 0
vsize: 27156
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6178 0 0 0 25973 23 0 0 25 0 1 0 423556489 27807744 6149 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6149 603 41 0 6748 0
vsize: 27156
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6187 0 0 0 26973 24 0 0 25 0 1 0 423556489 27807744 6158 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6158 603 41 0 6748 0
vsize: 27156
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6189 0 0 0 27973 24 0 0 25 0 1 0 423556489 27807744 6160 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6789 6160 603 41 0 6748 0
vsize: 27156
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6194 0 0 0 28972 24 0 0 25 0 1 0 423556489 27971584 6165 4294967295 134512640 134672761 3221224560 3221223684 134566082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6165 603 41 0 6788 0
vsize: 27316
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6196 0 0 0 29972 24 0 0 25 0 1 0 423556489 27971584 6167 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6167 603 41 0 6788 0
vsize: 27316
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6196 0 0 0 30972 24 0 0 25 0 1 0 423556489 27971584 6167 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6167 603 41 0 6788 0
vsize: 27316
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6198 0 0 0 31971 25 0 0 25 0 1 0 423556489 27971584 6169 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6169 603 41 0 6788 0
vsize: 27316
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6201 0 0 0 32971 25 0 0 25 0 1 0 423556489 27971584 6172 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6172 603 41 0 6788 0
vsize: 27316
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6201 0 0 0 33971 25 0 0 25 0 1 0 423556489 27971584 6172 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6172 603 41 0 6788 0
vsize: 27316
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6201 0 0 0 34970 26 0 0 25 0 1 0 423556489 27971584 6172 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6172 603 41 0 6788 0
vsize: 27316
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6201 0 0 0 35970 26 0 0 25 0 1 0 423556489 27971584 6172 4294967295 134512640 134672761 3221224560 3221223664 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6172 603 41 0 6788 0
vsize: 27316
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6201 0 0 0 36970 26 0 0 25 0 1 0 423556489 27971584 6172 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6172 603 41 0 6788 0
vsize: 27316
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6201 0 0 0 37969 27 0 0 25 0 1 0 423556489 27971584 6172 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6172 603 41 0 6788 0
vsize: 27316
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6201 0 0 0 38969 27 0 0 25 0 1 0 423556489 27971584 6172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6172 603 41 0 6788 0
vsize: 27316
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6211 0 0 0 39969 27 0 0 25 0 1 0 423556489 27971584 6182 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6182 603 41 0 6788 0
vsize: 27316
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6211 0 0 0 40968 27 0 0 25 0 1 0 423556489 27971584 6182 4294967295 134512640 134672761 3221224560 3221223744 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6182 603 41 0 6788 0
vsize: 27316
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6213 0 0 0 41968 28 0 0 25 0 1 0 423556489 27971584 6184 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6829 6184 603 41 0 6788 0
vsize: 27316
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6225 0 0 0 42968 28 0 0 25 0 1 0 423556489 28233728 6196 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6196 603 41 0 6852 0
vsize: 27572
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6227 0 0 0 43967 28 0 0 25 0 1 0 423556489 28233728 6198 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6198 603 41 0 6852 0
vsize: 27572
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6228 0 0 0 44967 28 0 0 25 0 1 0 423556489 28233728 6199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6199 603 41 0 6852 0
vsize: 27572
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6228 0 0 0 45967 29 0 0 25 0 1 0 423556489 28233728 6199 4294967295 134512640 134672761 3221224560 3221223664 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6199 603 41 0 6852 0
vsize: 27572
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6228 0 0 0 46966 29 0 0 25 0 1 0 423556489 28233728 6199 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6199 603 41 0 6852 0
vsize: 27572
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6228 0 0 0 47966 29 0 0 25 0 1 0 423556489 28233728 6199 4294967295 134512640 134672761 3221224560 3221223664 134560306 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6199 603 41 0 6852 0
vsize: 27572
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6228 0 0 0 48965 30 0 0 25 0 1 0 423556489 28233728 6199 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6199 603 41 0 6852 0
vsize: 27572
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6229 0 0 0 49965 30 0 0 25 0 1 0 423556489 28233728 6200 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6200 603 41 0 6852 0
vsize: 27572
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6229 0 0 0 50965 30 0 0 25 0 1 0 423556489 28233728 6200 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6893 6200 603 41 0 6852 0
vsize: 27572
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6239 0 0 0 51965 30 0 0 25 0 1 0 423556489 28430336 6210 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6210 603 41 0 6900 0
vsize: 27764
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6255 0 0 0 52964 31 0 0 25 0 1 0 423556489 28430336 6226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6226 603 41 0 6900 0
vsize: 27764
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6255 0 0 0 53963 31 0 0 25 0 1 0 423556489 28430336 6226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6226 603 41 0 6900 0
vsize: 27764
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6255 0 0 0 54963 32 0 0 25 0 1 0 423556489 28430336 6226 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6226 603 41 0 6900 0
vsize: 27764
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6255 0 0 0 55963 32 0 0 25 0 1 0 423556489 28430336 6226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6226 603 41 0 6900 0
vsize: 27764
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6255 0 0 0 56962 32 0 0 25 0 1 0 423556489 28430336 6226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6226 603 41 0 6900 0
vsize: 27764
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6255 0 0 0 57962 32 0 0 25 0 1 0 423556489 28430336 6226 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6226 603 41 0 6900 0
vsize: 27764
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6255 0 0 0 58962 33 0 0 25 0 1 0 423556489 28430336 6226 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6226 603 41 0 6900 0
vsize: 27764
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6255 0 0 0 59961 33 0 0 25 0 1 0 423556489 28430336 6226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6226 603 41 0 6900 0
vsize: 27764
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6255 0 0 0 60961 33 0 0 25 0 1 0 423556489 28430336 6226 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6226 603 41 0 6900 0
vsize: 27764
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6266 0 0 0 61961 34 0 0 25 0 1 0 423556489 28430336 6237 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6237 603 41 0 6900 0
vsize: 27764
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6267 0 0 0 62961 34 0 0 25 0 1 0 423556489 28430336 6238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6238 603 41 0 6900 0
vsize: 27764
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6270 0 0 0 63960 34 0 0 25 0 1 0 423556489 28430336 6241 4294967295 134512640 134672761 3221224560 3221223744 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6241 603 41 0 6900 0
vsize: 27764
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6272 0 0 0 64959 35 0 0 25 0 1 0 423556489 28430336 6243 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6243 603 41 0 6900 0
vsize: 27764
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6272 0 0 0 65959 35 0 0 25 0 1 0 423556489 28430336 6243 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6243 603 41 0 6900 0
vsize: 27764
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6272 0 0 0 66959 35 0 0 25 0 1 0 423556489 28430336 6243 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6243 603 41 0 6900 0
vsize: 27764
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6283 0 0 0 67958 36 0 0 25 0 1 0 423556489 28626944 6254 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6254 603 41 0 6948 0
vsize: 27956
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6283 0 0 0 68958 36 0 0 25 0 1 0 423556489 28626944 6254 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6254 603 41 0 6948 0
vsize: 27956
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6283 0 0 0 69958 36 0 0 25 0 1 0 423556489 28626944 6254 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6254 603 41 0 6948 0
vsize: 27956
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6283 0 0 0 70958 36 0 0 25 0 1 0 423556489 28626944 6254 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6254 603 41 0 6948 0
vsize: 27956
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6283 0 0 0 71957 37 0 0 25 0 1 0 423556489 28626944 6254 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6254 603 41 0 6948 0
vsize: 27956
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6296 0 0 0 72957 37 0 0 25 0 1 0 423556489 28626944 6267 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6267 603 41 0 6948 0
vsize: 27956
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6297 0 0 0 73956 37 0 0 25 0 1 0 423556489 28626944 6268 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6268 603 41 0 6948 0
vsize: 27956
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6297 0 0 0 74957 37 0 0 25 0 1 0 423556489 28626944 6268 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6268 603 41 0 6948 0
vsize: 27956
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6298 0 0 0 75957 37 0 0 25 0 1 0 423556489 28626944 6269 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6269 603 41 0 6948 0
vsize: 27956
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6299 0 0 0 76957 37 0 0 25 0 1 0 423556489 28626944 6270 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6270 603 41 0 6948 0
vsize: 27956
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6299 0 0 0 77957 37 0 0 25 0 1 0 423556489 28626944 6270 4294967295 134512640 134672761 3221224560 3221223684 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6270 603 41 0 6948 0
vsize: 27956
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6299 0 0 0 78957 37 0 0 25 0 1 0 423556489 28626944 6270 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6270 603 41 0 6948 0
vsize: 27956
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6299 0 0 0 79957 37 0 0 25 0 1 0 423556489 28626944 6270 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6270 603 41 0 6948 0
vsize: 27956
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6299 0 0 0 80957 37 0 0 25 0 1 0 423556489 28626944 6270 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6270 603 41 0 6948 0
vsize: 27956
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6299 0 0 0 81957 37 0 0 25 0 1 0 423556489 28626944 6270 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6270 603 41 0 6948 0
vsize: 27956
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6299 0 0 0 82957 37 0 0 25 0 1 0 423556489 28626944 6270 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6270 603 41 0 6948 0
vsize: 27956
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6299 0 0 0 83957 37 0 0 25 0 1 0 423556489 28626944 6270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6270 603 41 0 6948 0
vsize: 27956
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6299 0 0 0 84958 37 0 0 25 0 1 0 423556489 28626944 6270 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6270 603 41 0 6948 0
vsize: 27956
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6312 0 0 0 85958 37 0 0 25 0 1 0 423556489 28626944 6283 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6283 603 41 0 6948 0
vsize: 27956
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6333 0 0 0 86958 37 0 0 25 0 1 0 423556489 28823552 6304 4294967295 134512640 134672761 3221224560 3221223728 134561130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6304 603 41 0 6996 0
vsize: 28148
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6344 0 0 0 87958 37 0 0 25 0 1 0 423556489 28823552 6315 4294967295 134512640 134672761 3221224560 3221223656 1075347361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6315 603 41 0 6996 0
vsize: 28148
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6347 0 0 0 88958 37 0 0 25 0 1 0 423556489 28823552 6318 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6318 603 41 0 6996 0
vsize: 28148
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6352 0 0 0 89959 37 0 0 25 0 1 0 423556489 28823552 6323 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6323 603 41 0 6996 0
vsize: 28148
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6352 0 0 0 90959 37 0 0 25 0 1 0 423556489 28823552 6323 4294967295 134512640 134672761 3221224560 3221223776 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6323 603 41 0 6996 0
vsize: 28148
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6352 0 0 0 91959 37 0 0 25 0 1 0 423556489 28823552 6323 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6323 603 41 0 6996 0
vsize: 28148
[startup+930.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6352 0 0 0 92959 37 0 0 25 0 1 0 423556489 28823552 6323 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6323 603 41 0 6996 0
vsize: 28148
[startup+940.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6352 0 0 0 93959 37 0 0 25 0 1 0 423556489 28823552 6323 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6323 603 41 0 6996 0
vsize: 28148
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6361 0 0 0 94959 37 0 0 25 0 1 0 423556489 29020160 6332 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6332 603 41 0 7044 0
vsize: 28340
[startup+960.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6368 0 0 0 95960 37 0 0 25 0 1 0 423556489 29020160 6339 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6339 603 41 0 7044 0
vsize: 28340
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6371 0 0 0 96960 37 0 0 25 0 1 0 423556489 29020160 6342 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6342 603 41 0 7044 0
vsize: 28340
[startup+980.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6371 0 0 0 97960 37 0 0 25 0 1 0 423556489 29020160 6342 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6342 603 41 0 7044 0
vsize: 28340
[startup+990.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6371 0 0 0 98960 37 0 0 25 0 1 0 423556489 29020160 6342 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6342 603 41 0 7044 0
vsize: 28340
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6371 0 0 0 99961 37 0 0 25 0 1 0 423556489 29020160 6342 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6342 603 41 0 7044 0
vsize: 28340
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6372 0 0 0 100961 37 0 0 25 0 1 0 423556489 29020160 6343 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6343 603 41 0 7044 0
vsize: 28340
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 101961 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 102961 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 103961 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 104961 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 105962 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 106962 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 107962 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 108962 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 109962 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 110963 37 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 111962 38 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 112962 38 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 113962 38 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 114963 38 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 115963 38 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 116963 38 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 117963 38 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6375 0 0 0 118963 38 0 0 25 0 1 0 423556489 29020160 6346 4294967295 134512640 134672761 3221224560 3221223728 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6346 603 41 0 7044 0
vsize: 28340
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2150
Raw data (stat): 2150 (minisat+) R 2149 25347 25346 0 -1 0 6379 0 0 0 119964 38 0 0 25 0 1 0 423556489 29020160 6350 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7085 6350 603 41 0 7044 0
vsize: 28340
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2150
Raw data (stat): 2150 (minisat+) Z 2149 25347 25346 0 -1 12 6382 0 0 0 119964 39 0 0 25 0 1 0 423556489 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.03
CPU user time (s): 1199.64
CPU system time (s): 0.39194
CPU usage (%): 99.9998
Max. virtual memory (Kb): 28340
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####