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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod013.opb
MD5SUM	b964292d4197638ce79b3f213e8fe89b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5130240
Optimality of the best value was proved	NO
Number of terms in the objective function	1008
Biggest coefficient in the objective function	366477312
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	12643636975
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	366477312
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	12643636975
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	1008
Total number of constraints	110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	48
Number of constraints which are nor clauses,nor cardinality constraints	62
Minimum length of a constraint	1
Maximum length of a constraint	160
Trace number 19059

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 17:45:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17053 boxname=wulflinc23 idbench=1312 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b964292d4197638ce79b3f213e8fe89b  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-mod013.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-mod013.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-mod013.opb
IDLAUNCH: 17053
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        639656 kB
Buffers:         26832 kB
Cached:         342688 kB
SwapCached:        536 kB
Active:          32524 kB
Inactive:       339108 kB
HighTotal:      131008 kB
HighFree:        15232 kB
LowTotal:       903652 kB
LowFree:        624424 kB
SwapTotal:     2097136 kB
SwapFree:      2095852 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            17748 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:05:14 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 17053 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 76 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############
c   -- Clauses(.)/Splits(s): (none)
c ---[  74]---> Adder-cost: 118   maxlim: 16250   bits: 15/14
c ---[  72]---> Adder-cost: 118   maxlim: 16890   bits: 15/15
c ---[  70]---> Adder-cost: 110   maxlim: 9338   bits: 14/14
c ---[  68]---> Adder-cost: 110   maxlim: 9978   bits: 14/14
c ---[  66]---> Adder-cost: 110   maxlim: 9978   bits: 14/14
c ---[  64]---> Adder-cost: 100   maxlim: 5498   bits: 13/13
c ---[  63]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  62]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  61]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  60]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  58]---> Adder-cost: 164   maxlim: 21880   bits: 15/15
c ---[  57]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  56]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  54]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  53]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  52]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  51]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  50]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  49]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  48]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  46]---> Adder-cost: 164   maxlim: 22520   bits: 15/15
c ---[  45]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  44]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  42]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  41]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  40]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  37]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  36]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  34]---> Adder-cost: 162   maxlim: 19704   bits: 15/15
c ---[  33]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  32]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  31]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  30]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  29]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  28]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  27]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  26]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  25]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  24]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  22]---> Adder-cost: 162   maxlim: 20984   bits: 15/15
c ---[  21]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  20]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  19]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  18]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  17]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  16]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  13]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  10]---> Adder-cost: 154   maxlim: 14072   bits: 14/14
c ---[   9]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   8]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   7]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   6]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   4]---> Adder-cost: 140   maxlim: 7544   bits: 13/13
c ---[   2]---> Adder-cost: 120   maxlim: 23162   bits: 15/15
c ---[   0]---> Adder-cost: 118   maxlim: 15610   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   13808    50794 |    4602       0        0     nan |  0.000 % |
c |       100 |   13744    50576 |    5062      92      283     3.1 | 35.244 % |
c |       250 |   13704    50442 |    5568     237      745     3.1 | 35.424 % |
c |       475 |   13672    50338 |    6125     456     1706     3.7 | 35.577 % |
c |       813 |   13654    50280 |    6737     792     4957     6.3 | 35.680 % |
c |      1319 |   13573    50011 |    7411    1287     7669     6.0 | 36.038 % |
c |      2078 |   13498    49766 |    8152    2039    11548     5.7 | 36.396 % |
c |      3218 |   13482    49714 |    8967    3176    17040     5.4 | 36.473 % |
c |      4926 |   13442    49584 |    9864    4877    27277     5.6 | 36.652 % |
c ==============================================================================
c [1mFound solution: 11650248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4308   maxlim: 19314215   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6913 |   43477   156878 |   14492    6864    44665     6.5 | 36.652 % |
c |      7014 |   43477   156878 |   15941    6965    45886     6.6 | 17.550 % |
c |      7164 |   43477   156878 |   17535    7115    47236     6.6 | 17.550 % |
c |      7389 |   43477   156878 |   19288    7340    49176     6.7 | 17.550 % |
c |      7726 |   43477   156878 |   21217    7677    52233     6.8 | 17.550 % |
c |      8232 |   43477   156878 |   23339    8183    58518     7.2 | 17.550 % |
c |      8991 |   43468   156847 |   25673    8940    65360     7.3 | 17.563 % |
c ==============================================================================
c [1mFound solution: 11428377[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 19536086   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10075 |   43508   157142 |   14502   10023    93340     9.3 | 17.563 % |
c |     10175 |   43508   157142 |   15952   10123    93847     9.3 | 17.668 % |
c |     10325 |   43508   157142 |   17547   10273    95813     9.3 | 17.668 % |
c |     10552 |   43508   157142 |   19302   10500    98114     9.3 | 17.668 % |
c |     10890 |   43508   157142 |   21232   10838   108261    10.0 | 17.668 % |
c ==============================================================================
c [1mFound solution: 10284612[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 20679851   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11098 |   43523   157305 |   14507   11044   110794    10.0 | 17.668 % |
c |     11198 |   43523   157305 |   15957   11144   111982    10.0 | 17.784 % |
c |     11350 |   43523   157305 |   17553   11296   114799    10.2 | 17.784 % |
c |     11575 |   43523   157305 |   19308   11521   118207    10.3 | 17.784 % |
c |     11912 |   43523   157305 |   21239   11858   126477    10.7 | 17.784 % |
c |     12418 |   43523   157305 |   23363   12364   138928    11.2 | 17.784 % |
c |     13177 |   43523   157305 |   25700   13123   164382    12.5 | 17.784 % |
c |     14317 |   43523   157305 |   28270   14263   240603    16.9 | 17.784 % |
c |     16025 |   43515   157275 |   31097   15969   308459    19.3 | 17.796 % |
c ==============================================================================
c [1mFound solution: 9366912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21597551   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16670 |   43533   157435 |   14511   16614   326170    19.6 | 17.796 % |
c |     16770 |   43533   157435 |   15962    8407   211742    25.2 | 17.891 % |
c |     16922 |   43533   157435 |   17558    8559   213722    25.0 | 17.891 % |
c |     17147 |   43533   157435 |   19314    8784   219266    25.0 | 17.891 % |
c |     17485 |   43527   157415 |   21245    9120   224460    24.6 | 17.903 % |
c |     17991 |   43527   157415 |   23370    9626   230072    23.9 | 17.903 % |
c |     18750 |   43527   157415 |   25707   10385   257814    24.8 | 17.903 % |
c |     19890 |   43527   157415 |   28277   11525   275613    23.9 | 17.903 % |
c |     21599 |   43511   157363 |   31105   13231   558066    42.2 | 17.940 % |
c |     24161 |   43511   157363 |   34216   15793   654415    41.4 | 17.940 % |
c |     28005 |   43511   157363 |   37637   19637   952454    48.5 | 17.940 % |
c |     33772 |   43511   157363 |   41401   25404  1367741    53.8 | 17.940 % |
c |     42422 |   43511   157363 |   45541   34054  1903967    55.9 | 17.940 % |
c ==============================================================================
c [1mFound solution: 7250685[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23713778   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42632 |   43536   157619 |   14512   34264  1914365    55.9 | 17.940 % |
c |     42734 |   43536   157619 |   15963   14879   795071    53.4 | 18.075 % |
c |     42887 |   43536   157619 |   17559   15032   795789    52.9 | 18.075 % |
c |     43112 |   43521   157572 |   19315   15256   797556    52.3 | 18.112 % |
c |     43449 |   43521   157572 |   21247   15593   800027    51.3 | 18.112 % |
c |     43955 |   43521   157572 |   23371   16099   803170    49.9 | 18.112 % |
c |     44715 |   43515   157552 |   25708   16856   957063    56.8 | 18.124 % |
c |     45855 |   43515   157552 |   28279   17996   972735    54.1 | 18.124 % |
c |     47564 |   43515   157552 |   31107   19705  1013050    51.4 | 18.124 % |
c |     50126 |   43508   157529 |   34218   22256  1099639    49.4 | 18.136 % |
c ==============================================================================
c [1mFound solution: 6927348[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24037115   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50417 |   43525   157728 |   14508   22547  1103615    48.9 | 18.136 % |
c |     50517 |   43525   157728 |   15958   11374   348890    30.7 | 18.243 % |
c |     50667 |   43525   157728 |   17554   11524   349861    30.4 | 18.243 % |
c |     50893 |   43525   157728 |   19310   11750   364605    31.0 | 18.243 % |
c |     51231 |   43525   157728 |   21241   12088   421203    34.8 | 18.243 % |
c |     51737 |   43525   157728 |   23365   12594   429666    34.1 | 18.243 % |
c |     52496 |   43525   157728 |   25701   13353   439711    32.9 | 18.243 % |
c |     53635 |   43525   157728 |   28271   14492   495504    34.2 | 18.243 % |
c |     55343 |   43525   157728 |   31099   16200   807445    49.8 | 18.243 % |
c |     57905 |   43525   157728 |   34209   18762   995008    53.0 | 18.243 % |
c |     61754 |   43525   157728 |   37630   22611  1376134    60.9 | 18.243 % |
c |     67521 |   43525   157728 |   41393   28378  2727461    96.1 | 18.243 % |
c |     76174 |   43525   157728 |   45532   37031  3329674    89.9 | 18.243 % |
c |     89149 |   43525   157728 |   50085   16406  1803370   109.9 | 18.243 % |
c ==============================================================================
c [1mFound solution: 6716471[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24247992   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91296 |   43545   157951 |   14515   18553  1930604   104.1 | 18.243 % |
c |     91396 |   43545   157951 |   15966    9377   570050    60.8 | 18.368 % |
c |     91546 |   43545   157951 |   17563    9527   570872    59.9 | 18.368 % |
c |     91771 |   43545   157951 |   19319    9752   572155    58.7 | 18.368 % |
c |     92109 |   43545   157951 |   21251   10090   578280    57.3 | 18.368 % |
c |     92615 |   43545   157951 |   23376   10596   590712    55.7 | 18.368 % |
c |     93374 |   43545   157951 |   25714   11355   602746    53.1 | 18.368 % |
c |     94515 |   43545   157951 |   28285   12496   628263    50.3 | 18.368 % |
c |     96223 |   43545   157951 |   31114   14204   659132    46.4 | 18.368 % |
c |     98786 |   43545   157951 |   34225   16767   768285    45.8 | 18.368 % |
c |    102630 |   43540   157935 |   37648   20608   970759    47.1 | 18.380 % |
c |    108396 |   43525   157888 |   41412   26373  1404726    53.3 | 18.416 % |
c |    117045 |   43525   157888 |   45554   35022  2315406    66.1 | 18.416 % |
c |    130020 |   43525   157888 |   50109   47997  3633998    75.7 | 18.416 % |
c |    149482 |   43525   157888 |   55120   29693  3473409   117.0 | 18.416 % |
c |    178677 |   43525   157888 |   60632   17345  1565117    90.2 | 18.416 % |
c |    222466 |   43525   157888 |   66696   61134  8779501   143.6 | 18.416 % |
c |    288150 |   43516   157857 |   73365   69577 14031723   201.7 | 18.428 % |
c |    386676 |   43516   157857 |   80702   53326  6888762   129.2 | 18.428 % |
c ==============================================================================
c [1mFound solution: 6714822[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24249641   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    496584 |   43526   157969 |   14508   24596  3645214   148.2 | 18.428 % |
c |    496684 |   43526   157969 |   15958   12398  1462130   117.9 | 18.478 % |
c |    496834 |   43526   157969 |   17554   12548  1464648   116.7 | 18.478 % |
c |    497060 |   43526   157969 |   19310   12774  1467618   114.9 | 18.478 % |
c |    497397 |   43526   157969 |   21241   13111  1475828   112.6 | 18.478 % |
c |    497904 |   43526   157969 |   23365   13618  1479736   108.7 | 18.478 % |
c |    498664 |   43526   157969 |   25701   14378  1495392   104.0 | 18.478 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C1_0x2e__bit_7 C1_0x2e__bit_6 -C1_0x2e__bit_5 C1_0x2e__bit_4 C1_0x2e__bit_3 -C1_0x2e__bit_2 C1_0x2e__bit_1 C1_0x2e__bit0 C1_0x2e__bit1 C1_0x2e__bit2 -C1_0x2e__bit3 -C1_0x2e__bit4 -C1_0x2e__bit5 -C1_0x2e__bit6 -C1_0x2e__bit7 -C1_0x2e__bit8 -C1_0x2e__bit9 -C1_0x2e__bit10 -C1_0x2e__bit11 -C1_0x2e__bit12 -C2_0x2e__bit_7 -C2_0x2e__bit_6 -C2_0x2e__bit_5 -C2_0x2e__bit_4 -C2_0x2e__bit_3 -C2_0x2e__bit_2 -C2_0x2e__bit_1 -C2_0x2e__bit0 C2_0x2e__bit1 C2_0x2e__bit2 C2_0x2e__bit3 -C2_0x2e__bit4 -C2_0x2e__bit5 -C2_0x2e__bit6 -C2_0x2e__bit7 -C2_0x2e__bit8 -C2_0x2e__bit9 -C2_0x2e__bit10 -C2_0x2e__bit11 -C2_0x2e__bit12 -C3_0x2e__bit_7 C3_0x2e__bit_6 C3_0x2e__bit_5 C3_0x2e__bit_4 C3_0x2e__bit_3 -C3_0x2e__bit_2 C3_0x2e__bit_1 -C3_0x2e__bit0 -C3_0x2e__bit1 -C3_0x2e__bit2 -C3_0x2e__bit3 -C3_0x2e__bit4 -C3_0x2e__bit5 -C3_0x2e__bit6 -C3_0x2e__bit7 -C3_0x2e__bit8 -C3_0x2e__bit9 -C3_0x2e__bit10 -C3_0x2e__bit11 -C3_0x2e__bit12 C4_0x2e__bit_7 -C4_0x2e__bit_6 C4_0x2e__bit_5 -C4_0x2e__bit_4 C4_0x2e__bit_3 C4_0x2e__bit_2 -C4_0x2e__bit_1 C4_0x2e__bit0 C4_0x2e__bit1 C4_0x2e__bit2 C4_0x2e__bit3 -C4_0x2e__bit4 -C4_0x2e__bit5 -C4_0x2e__bit6 -C4_0x2e__bit7 -C4_0x2e__bit8 -C4_0x2e__bit9 -C4_0x2e__bit10 -C4_0x2e__bit11 -C4_0x2e__bit12 -C5_0x2e__bit_7 C5_0x2e__bit_6 -C5_0x2e__bit_5 -C5_0x2e__bit_4 C5_0x2e__bit_3 -C5_0x2e__bit_2 -C5_0x2e__bit_1 C5_0x2e__bit0 -C5_0x2e__bit1 C5_0x2e__bit2 -C5_0x2e__bit3 -C5_0x2e__bit4 -C5_0x2e__bit5 -C5_0x2e__bit6 -C5_0x2e__bit7 -C5_0x2e__bit8 -C5_0x2e__bit9 -C5_0x2e__bit10 -C5_0x2e__bit11 -C5_0x2e__bit12 -C6_0x2e__bit_7 -C6_0x2e__bit_6 -C6_0x2e__bit_5 -C6_0x2e__bit_4 -C6_0x2e__bit_3 -C6_0x2e__bit_2 -C6_0x2e__bit_1 -C6_0x2e__bit0 C6_0x2e__bit1 -C6_0x2e__bit2 -C6_0x2e__bit3 -C6_0x2e__bit4 -C6_0x2e__bit5 -C6_0x2e__bit6 -C6_0x2e__bit7 -C6_0x2e__bit8 -C6_0x2e__bit9 -C6_0x2e__bit10 -C6_0x2e__bit11 -C6_0x2e__bit12 -C7_0x2e__bit_7 -C7_0x2e__bit_6 -C7_0x2e__bit_5 -C7_0x2e__bit_4 -C7_0x2e__bit_3 -C7_0x2e__bit_2 -C7_0x2e__bit_1 -C7_0x2e__bit0 -C7_0x2e__bit1 -C7_0x2e__bit2 -C7_0x2e__bit3 -C7_0x2e__bit4 -C7_0x2e__bit5 -C7_0x2e__bit6 -C7_0x2e__bit7 -C7_0x2e__bit8 -C7_0x2e__bit9 -C7_0x2e__bit10 -C7_0x2e__bit11 -C7_0x2e__bit12 -C8_0x2e__bit_7 -C8_0x2e__bit_6 -C8_0x2e__bit_5 -C8_0x2e__bit_4 -C8_0x2e__bit_3 -C8_0x2e__bit_2 -C8_0x2e__bit_1 -C8_0x2e__bit0 -C8_0x2e__bit1 -C8_0x2e__bit2 -C8_0x2e__bit3 -C8_0x2e__bit4 -C8_0x2e__bit5 -C8_0x2e__bit6 -C8_0x2e__bit7 -C8_0x2e__bit8 -C8_0x2e__bit9 -C8_0x2e__bit10 -C8_0x2e__bit11 -C8_0x2e__bit12 -C9_0x2e__bit_7 -C9_0x2e__bit_6 -C9_0x2e__bit_5 -C9_0x2e__bit_4 -C9_0x2e__bit_3 -C9_0x2e__bit_2 -C9_0x2e__bit_1 -C9_0x2e__bit0 -C9_0x2e__bit1 -C9_0x2e__bit2 -C9_0x2e__bit3 C9_0x2e__bit4 -C9_0x2e__bit5 -C9_0x2e__bit6 -C9_0x2e__bit7 -C9_0x2e__bit8 -C9_0x2e__bit9 -C9_0x2e__bit10 -C9_0x2e__bit11 -C9_0x2e__bit12 -C10_0x2e__bit_7 -C10_0x2e__bit_6 -C10_0x2e__bit_5 -C10_0x2e__bit_4 -C10_0x2e__bit_3 -C10_0x2e__bit_2 -C10_0x2e__bit_1 -C10_0x2e__bit0 -C10_0x2e__bit1 -C10_0x2e__bit2 -C10_0x2e__bit3 C10_0x2e__bit4 -C10_0x2e__bit5 -C10_0x2e__bit6 -C10_0x2e__bit7 -C10_0x2e__bit8 -C10_0x2e__bit9 -C10_0x2e__bit10 -C10_0x2e__bit11 -C10_0x2e__bit12 -C11_0x2e__bit_7 -C11_0x2e__bit_6 -C11_0x2e__bit_5 -C11_0x2e__bit_4 -C11_0x2e__bit_3 -C11_0x2e__bit_2 -C11_0x2e__bit_1 -C11_0x2e__bit0 -C11_0x2e__bit1 -C11_0x2e__bit2 -C11_0x2e__bit3 -C11_0x2e__bit4 -C11_0x2e__bit5 -C11_0x2e__bit6 -C11_0x2e__bit7 -C11_0x2e__bit8 -C11_0x2e__bit9 -C11_0x2e__bit10 -C11_0x2e__bit11 -C11_0x2e__bit12 -C12_0x2e__bit_7 -C12_0x2e__bit_6 -C12_0x2e__bit_5 -C12_0x2e__bit_4 -C12_0x2e__bit_3 -C12_0x2e__bit_2 -C12_0x2e__bit_1 -C12_0x2e__bit0 -C12_0x2e__bit1 -C12_0x2e__bit2 -C12_0x2e__bit3 -C12_0x2e__bit4 -C12_0x2e__bit5 -C12_0x2e__bit6 -C12_0x2e__bit7 -C12_0x2e__bit8 -C12_0x2e__bit9 -C12_0x2e__bit10 -C12_0x2e__bit11 -C12_0x2e__bit12 -C13_0x2e__bit_7 -C13_0x2e__bit_6 -C13_0x2e__bit_5 -C13_0x2e__bit_4 -C13_0x2e__bit_3 -C13_0x2e__bit_2 -C13_0x2e__bit_1 -C13_0x2e__bit0 -C13_0x2e__bit1 -C13_0x2e__bit2 -C13_0x2e__bit3 -C13_0x2e__bit4 -C13_0x2e__bit5 -C13_0x2e__bit6 -C13_0x2e__bit7 -C13_0x2e__bit8 -C13_0x2e__bit9 -C13_0x2e__bit10 -C13_0x2e__bit11 -C13_0x2e__bit12 -C14_0x2e__bit_7 -C14_0x2e__bit_6 -C14_0x2e__bit_5 -C14_0x2e__bit_4 -C14_0x2e__bit_3 -C14_0x2e__bit_2 -C14_0x2e__bit_1 -C14_0x2e__bit0 -C14_0x2e__bit1 -C14_0x2e__bit2 C14_0x2e__bit3 -C14_0x2e__bit4 -C14_0x2e__bit5 -C14_0x2e__bit6 -C14_0x2e__bit7 -C14_0x2e__bit8 -C14_0x2e__bit9 -C14_0x2e__bit10 -C14_0x2e__bit11 -C14_0x2e__bit12 -C15_0x2e__bit_7 -C15_0x2e__bit_6 -C15_0x2e__bit_5 -C15_0x2e__bit_4 -C15_0x2e__bit_3 -C15_0x2e__bit_2 -C15_0x2e__bit_1 -C15_0x2e__bit0 -C15_0x2e__bit1 -C15_0x2e__bit2 -C15_0x2e__bit3 -C15_0x2e__bit4 -C15_0x2e__bit5 -C15_0x2e__bit6 -C15_0x2e__bit7 -C15_0x2e__bit8 -C15_0x2e__bit9 -C15_0x2e__bit10 -C15_0x2e__bit11 -C15_0x2e__bit12 -C16_0x2e__bit_7 -C16_0x2e__bit_6 -C16_0x2e__bit_5 -C16_0x2e__bit_4 -C16_0x2e__bit_3 -C16_0x2e__bit_2 -C16_0x2e__bit_1 -C16_0x2e__bit0 -C16_0x2e__bit1 -C16_0x2e__bit2 -C16_0x2e__bit3 -C16_0x2e__bit4 -C16_0x2e__bit5 -C16_0x2e__bit6 -C16_0x2e__bit7 -C16_0x2e__bit8 -C16_0x2e__bit9 -C16_0x2e__bit10 -C16_0x2e__bit11 -C16_0x2e__bit12 -C17_0x2e__bit_7 C17_0x2e__bit_6 C17_0x2e__bit_5 C17_0x2e__bit_4 C17_0x2e__bit_3 -C17_0x2e__bit_2 C17_0x2e__bit_1 C17_0x2e__bit0 -C17_0x2e__bit1 C17_0x2e__bit2 -C17_0x2e__bit3 -C17_0x2e__bit4 -C17_0x2e__bit5 -C17_0x2e__bit6 -C17_0x2e__bit7 -C17_0x2e__bit8 -C17_0x2e__bit9 -C17_0x2e__bit10 -C17_0x2e__bit11 -C17_0x2e__bit12 -C18_0x2e__bit_7 -C18_0x2e__bit_6 -C18_0x2e__bit_5 -C18_0x2e__bit_4 -C18_0x2e__bit_3 -C18_0x2e__bit_2 -C18_0x2e__bit_1 -C18_0x2e__bit0 -C18_0x2e__bit1 -C18_0x2e__bit2 -C18_0x2e__bit3 -C18_0x2e__bit4 -C18_0x2e__bit5 -C18_0x2e__bit6 -C18_0x2e__bit7 -C18_0x2e__bit8 -C18_0x2e__bit9 -C18_0x2e__bit10 -C18_0x2e__bit11 -C18_0x2e__bit12 -C19_0x2e__bit_7 C19_0x2e__bit_6 -C19_0x2e__bit_5 -C19_0x2e__bit_4 -C19_0x2e__bit_3 C19_0x2e__bit_2 -C19_0x2e__bit_1 -C19_0x2e__bit0 -C19_0x2e__bit1 -C19_0x2e__bit2 C19_0x2e__bit3 C19_0x2e__bit4 -C19_0x2e__bit5 -C19_0x2e__bit6 -C19_0x2e__bit7 -C19_0x2e__bit8 -C19_0x2e__bit9 -C19_0x2e__bit10 -C19_0x2e__bit11 -C19_0x2e__bit12 -C20_0x2e__bit_7 -C20_0x2e__bit_6 -C20_0x2e__bit_5 -C20_0x2e__bit_4 -C20_0x2e__bit_3 -C20_0x2e__bit_2 -C20_0x2e__bit_1 -C20_0x2e__bit0 -C20_0x2e__bit1 -C20_0x2e__bit2 -C20_0x2e__bit3 -C20_0x2e__bit4 -C20_0x2e__bit5 -C20_0x2e__bit6 -C20_0x2e__bit7 -C20_0x2e__bit8 -C20_0x2e__bit9 -C20_0x2e__bit10 -C20_0x2e__bit11 -C20_0x2e__bit12 -C21_0x2e__bit_7 -C21_0x2e__bit_6 -C21_0x2e__bit_5 -C21_0x2e__bit_4 -C21_0x2e__bit_3 -C21_0x2e__bit_2 -C21_0x2e__bit_1 -C21_0x2e__bit0 -C21_0x2e__bit1 -C21_0x2e__bit2 -C21_0x2e__bit3 -C21_0x2e__bit4 -C21_0x2e__bit5 -C21_0x2e__bit6 -C21_0x2e__bit7 -C21_0x2e__bit8 -C21_0x2e__bit9 -C21_0x2e__bit10 -C21_0x2e__bit11 -C21_0x2e__bit12 -C22_0x2e__bit_7 -C22_0x2e__bit_6 -C22_0x2e__bit_5 -C22_0x2e__bit_4 -C22_0x2e__bit_3 -C22_0x2e__bit_2 -C22_0x2e__bit_1 -C22_0x2e__bit0 -C22_0x2e__bit1 -C22_0x2e__bit2 -C22_0x2e__bit3 -C22_0x2e__bit4 -C22_0x2e__bit5 -C22_0x2e__bit6 -C22_0x2e__bit7 -C22_0x2e__bit8 -C22_0x2e__bit9 -C22_0x2e__bit10 -C22_0x2e__bit11 -C22_0x2e__bit12 -C23_0x2e__bit_7 -C23_0x2e__bit_6 -C23_0x2e__bit_5 -C23_0x2e__bit_4 -C23_0x2e__bit_3 -C23_0x2e__bit_2 -C23_0x2e__bit_1 -C23_0x2e__bit0 -C23_0x2e__bit1 -C23_0x2e__bit2 -C23_0x2e__bit3 -C23_0x2e__bit4 -C23_0x2e__bit5 -C23_0x2e__bit6 -C23_0x2e__bit7 -C23_0x2e__bit8 -C23_0x2e__bit9 -C23_0x2e__bit10 -C23_0x2e__bit11 -C23_0x2e__bit12 -C24_0x2e__bit_7 -C24_0x2e__bit_6 -C24_0x2e__bit_5 -C24_0x2e__bit_4 -C24_0x2e__bit_3 -C24_0x2e__bit_2 -C24_0x2e__bit_1 -C24_0x2e__bit0 -C24_0x2e__bit1 -C24_0x2e__bit2 -C24_0x2e__bit3 -C24_0x2e__bit4 -C24_0x2e__bit5 -C24_0x2e__bit6 -C24_0x2e__bit7 -C24_0x2e__bit8 -C24_0x2e__bit9 -C24_0x2e__bit10 -C24_0x2e__bit11 -C24_0x2e__bit12 C25_0x2e__bit_7 -C25_0x2e__bit_6 -C25_0x2e__bit_5 C25_0x2e__bit_4 -C25_0x2e__bit_3 C25_0x2e__bit_2 C25_0x2e__bit_1 C25_0x2e__bit0 -C25_0x2e__bit1 -C25_0x2e__bit2 -C25_0x2e__bit3 -C25_0x2e__bit4 -C25_0x2e__bit5 -C25_0x2e__bit6 -C25_0x2e__bit7 -C25_0x2e__bit8 -C25_0x2e__bit9 -C25_0x2e__bit10 -C25_0x2e__bit11 -C25_0x2e__bit12 -C26_0x2e__bit_7 -C26_0x2e__bit_6 -C26_0x2e__bit_5 -C26_0x2e__bit_4 -C26_0x2e__bit_3 -C26_0x2e__bit_2 -C26_0x2e__bit_1 -C26_0x2e__bit0 -C26_0x2e__bit1 -C26_0x2e__bit2 -C26_0x2e__bit3 -C26_0x2e__bit4 -C26_0x2e__bit5 -C26_0x2e__bit6 -C26_0x2e__bit7 -C26_0x2e__bit8 -C26_0x2e__bit9 -C26_0x2e__bit10 -C26_0x2e__bit11 -C26_0x2e__bit12 -C27_0x2e__bit_7 -C27_0x2e__bit_6 -C27_0x2e__bit_5 -C27_0x2e__bit_4 -C27_0x2e__bit_3 -C27_0x2e__bit_2 -C27_0x2e__bit_1 -C27_0x2e__bit0 -C27_0x2e__bit1 -C27_0x2e__bit2 -C27_0x2e__bit3 -C27_0x2e__bit4 -C27_0x2e__bit5 -C27_0x2e__bit6 -C27_0x2e__bit7 -C27_0x2e__bit8 -C27_0x2e__bit9 -C27_0x2e__bit10 -C27_0x2e__bit11 -C27_0x2e__bit12 C28_0x2e__bit_7 -C28_0x2e__bit_6 -C28_0x2e__bit_5 C28_0x2e__bit_4 -C28_0x2e__bit_3 C28_0x2e__bit_2 -C28_0x2e__bit_1 C28_0x2e__bit0 -C28_0x2e__bit1 -C28_0x2e__bit2 -C28_0x2e__bit3 -C28_0x2e__bit4 -C28_0x2e__bit5 -C28_0x2e__bit6 -C28_0x2e__bit7 -C28_0x2e__bit8 -C28_0x2e__bit9 -C28_0x2e__bit10 -C28_0x2e__bit11 -C28_0x2e__bit12 -C29_0x2e__bit_7 C29_0x2e__bit_6 C29_0x2e__bit_5 C29_0x2e__bit_4 -C29_0x2e__bit_3 C29_0x2e__bit_2 C29_0x2e__bit_1 C29_0x2e__bit0 -C29_0x2e__bit1 -C29_0x2e__bit2 C29_0x2e__bit3 -C29_0x2e__bit4 -C29_0x2e__bit5 -C29_0x2e__bit6 -C29_0x2e__bit7 -C29_0x2e__bit8 -C29_0x2e__bit9 -C29_0x2e__bit10 -C29_0x2e__bit11 -C29_0x2e__bit12 -C30_0x2e__bit_7 -C30_0x2e__bit_6 -C30_0x2e__bit_5 -C30_0x2e__bit_4 -C30_0x2e__bit_3 -C30_0x2e__bit_2 -C30_0x2e__bit_1 -C30_0x2e__bit0 -C30_0x2e__bit1 -C30_0x2e__bit2 -C30_0x2e__bit3 -C30_0x2e__bit4 -C30_0x2e__bit5 -C30_0x2e__bit6 -C30_0x2e__bit7 -C30_0x2e__bit8 -C30_0x2e__bit9 -C30_0x2e__bit10 -C30_0x2e__bit11 -C30_0x2e__bit12 -C31_0x2e__bit_7 -C31_0x2e__bit_6 -C31_0x2e__bit_5 -C31_0x2e__bit_4 -C31_0x2e__bit_3 -C31_0x2e__bit_2 -C31_0x2e__bit_1 C31_0x2e__bit0 -C31_0x2e__bit1 C31_0x2e__bit2 -C31_0x2e__bit3 -C31_0x2e__bit4 -C31_0x2e__bit5 -C31_0x2e__bit6 -C31_0x2e__bit7 -C31_0x2e__bit8 -C31_0x2e__bit9 -C31_0x2e__bit10 -C31_0x2e__bit11 -C31_0x2e__bit12 -C32_0x2e__bit_7 -C32_0x2e__bit_6 -C32_0x2e__bit_5 -C32_0x2e__bit_4 -C32_0x2e__bit_3 -C32_0x2e__bit_2 -C32_0x2e__bit_1 -C32_0x2e__bit0 C32_0x2e__bit1 -C32_0x2e__bit2 -C32_0x2e__bit3 -C32_0x2e__bit4 -C32_0x2e__bit5 -C32_0x2e__bit6 -C32_0x2e__bit7 -C32_0x2e__bit8 -C32_0x2e__bit9 -C32_0x2e__bit10 -C32_0x2e__bit11 -C32_0x2e__bit12 -C33_0x2e__bit_7 C33_0x2e__bit_6 C33_0x2e__bit_5 C33_0x2e__bit_4 C33_0x2e__bit_3 -C33_0x2e__bit_2 C33_0x2e__bit_1 C33_0x2e__bit0 -C33_0x2e__bit1 -C33_0x2e__bit2 -C33_0x2e__bit3 -C33_0x2e__bit4 -C33_0x2e__bit5 -C33_0x2e__bit6 -C33_0x2e__bit7 -C33_0x2e__bit8 -C33_0x2e__bit9 -C33_0x2e__bit10 -C33_0x2e__bit11 -C33_0x2e__bit12 -C34_0x2e__bit_7 -C34_0x2e__bit_6 -C34_0x2e__bit_5 -C34_0x2e__bit_4 -C34_0x2e__bit_3 -C34_0x2e__bit_2 -C34_0x2e__bit_1 -C34_0x2e__bit0 -C34_0x2e__bit1 -C34_0x2e__bit2 -C34_0x2e__bit3 -C34_0x2e__bit4 -C34_0x2e__bit5 -C34_0x2e__bit6 -C34_0x2e__bit7 -C34_0x2e__bit8 -C34_0x2e__bit9 -C34_0x2e__bit10 -C34_0x2e__bit11 -C34_0x2e__bit12 -C35_0x2e__bit_7 -C35_0x2e__bit_6 -C35_0x2e__bit_5 -C35_0x2e__bit_4 -C35_0x2e__bit_3 -C35_0x2e__bit_2 -C35_0x2e__bit_1 -C35_0x2e__bit0 -C35_0x2e__bit1 -C35_0x2e__bit2 -C35_0x2e__bit3 -C35_0x2e__bit4 -C35_0x2e__bit5 -C35_0x2e__bit6 -C35_0x2e__bit7 -C35_0x2e__bit8 -C35_0x2e__bit9 -C35_0x2e__bit10 -C35_0x2e__bit11 -C35_0x2e__bit12 -C36_0x2e__bit_7 C36_0x2e__bit_6 -C36_0x2e__bit_5 -C36_0x2e__bit_4 -C36_0x2e__bit_3 C36_0x2e__bit_2 -C36_0x2e__bit_1 C36_0x2e__bit0 C36_0x2e__bit1 -C36_0x2e__bit2 -C36_0x2e__bit3 -C36_0x2e__bit4 -C36_0x2e__bit5 -C36_0x2e__bit6 -C36_0x2e__bit7 -C36_0x2e__bit8 -C36_0x2e__bit9 -C36_0x2e__bit10 -C36_0x2e__bit11 -C36_0x2e__bit12 -C37_0x2e__bit_7 -C37_0x2e__bit_6 -C37_0x2e__bit_5 -C37_0x2e__bit_4 -C37_0x2e__bit_3 -C37_0x2e__bit_2 -C37_0x2e__bit_1 -C37_0x2e__bit0 -C37_0x2e__bit1 -C37_0x2e__bit2 -C37_0x2e__bit3 -C37_0x2e__bit4 -C37_0x2e__bit5 -C37_0x2e__bit6 -C37_0x2e__bit7 -C37_0x2e__bit8 -C37_0x2e__bit9 -C37_0x2e__bit10 -C37_0x2e__bit11 -C37_0x2e__bit12 -C38_0x2e__bit_7 -C38_0x2e__bit_6 -C38_0x2e__bit_5 -C38_0x2e__bit_4 -C38_0x2e__bit_3 -C38_0x2e__bit_2 -C38_0x2e__bit_1 -C38_0x2e__bit0 -C38_0x2e__bit1 -C38_0x2e__bit2 -C38_0x2e__bit3 -C38_0x2e__bit4 -C38_0x2e__bit5 -C38_0x2e__bit6 -C38_0x2e__bit7 -C38_0x2e__bit8 -C38_0x2e__bit9 -C38_0x2e__#### 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.48 0.83 0.91 2/54 9523
Raw data (stat): 9523 (runsolver) R 9522 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546981338 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.56 0.83 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 1717 0 0 0 994 5 0 0 25 0 1 0 546981338 9150464 1694 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2234 1694 603 41 0 2193 0
vsize: 8936
[startup+20.0004 s]
Raw data (loadavg): 0.62 0.84 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 2275 0 0 0 1992 6 0 0 25 0 1 0 546981338 11431936 2252 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2791 2252 603 41 0 2750 0
vsize: 11164
[startup+30.001 s]
Raw data (loadavg): 0.68 0.84 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 3103 0 0 0 2989 9 0 0 25 0 1 0 546981338 14790656 3080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3611 3080 603 41 0 3570 0
vsize: 14444
[startup+40.0003 s]
Raw data (loadavg): 0.73 0.85 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 3523 0 0 0 3987 11 0 0 25 0 1 0 546981338 16613376 3500 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4056 3500 603 41 0 4015 0
vsize: 16224
[startup+50.0014 s]
Raw data (loadavg): 0.77 0.85 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 3524 0 0 0 4987 12 0 0 25 0 1 0 546981338 16613376 3501 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4056 3501 603 41 0 4015 0
vsize: 16224
[startup+60.002 s]
Raw data (loadavg): 0.81 0.86 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 3524 0 0 0 5987 12 0 0 25 0 1 0 546981338 16613376 3501 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4056 3501 603 41 0 4015 0
vsize: 16224
[startup+70.0022 s]
Raw data (loadavg): 0.84 0.86 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 3915 0 0 0 6986 13 0 0 25 0 1 0 546981338 18227200 3892 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4450 3892 603 41 0 4409 0
vsize: 17800
[startup+80.0033 s]
Raw data (loadavg): 0.86 0.86 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 4748 0 0 0 7982 17 0 0 25 0 1 0 546981338 21553152 4725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5262 4725 603 41 0 5221 0
vsize: 21048
[startup+90.0029 s]
Raw data (loadavg): 0.88 0.87 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 5514 0 0 0 8978 20 0 0 25 0 1 0 546981338 24780800 5491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6050 5491 603 41 0 6009 0
vsize: 24200
[startup+100.003 s]
Raw data (loadavg): 0.90 0.87 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6225 0 0 0 9976 23 0 0 25 0 1 0 546981338 27578368 6202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6733 6202 603 41 0 6692 0
vsize: 26932
[startup+110.004 s]
Raw data (loadavg): 0.91 0.88 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6798 0 0 0 10974 25 0 0 25 0 1 0 546981338 29962240 6775 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6775 603 41 0 7274 0
vsize: 29260
[startup+120.005 s]
Raw data (loadavg): 0.93 0.88 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6800 0 0 0 11974 26 0 0 25 0 1 0 546981338 29962240 6777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6777 603 41 0 7274 0
vsize: 29260
[startup+130.005 s]
Raw data (loadavg): 0.94 0.88 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6800 0 0 0 12973 26 0 0 25 0 1 0 546981338 29962240 6777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6777 603 41 0 7274 0
vsize: 29260
[startup+140.005 s]
Raw data (loadavg): 0.95 0.89 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6800 0 0 0 13973 26 0 0 25 0 1 0 546981338 29962240 6777 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6777 603 41 0 7274 0
vsize: 29260
[startup+150.006 s]
Raw data (loadavg): 0.95 0.89 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6800 0 0 0 14973 27 0 0 25 0 1 0 546981338 29962240 6777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6777 603 41 0 7274 0
vsize: 29260
[startup+160.006 s]
Raw data (loadavg): 0.96 0.89 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6800 0 0 0 15973 27 0 0 25 0 1 0 546981338 29962240 6777 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6777 603 41 0 7274 0
vsize: 29260
[startup+170.016 s]
Raw data (loadavg): 0.97 0.90 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6805 0 0 0 16974 27 0 0 25 0 1 0 546981338 29962240 6782 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6782 603 41 0 7274 0
vsize: 29260
[startup+180.017 s]
Raw data (loadavg): 0.97 0.90 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6805 0 0 0 17974 27 0 0 25 0 1 0 546981338 29962240 6782 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6782 603 41 0 7274 0
vsize: 29260
[startup+190.017 s]
Raw data (loadavg): 0.98 0.90 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6805 0 0 0 18974 28 0 0 25 0 1 0 546981338 29962240 6782 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6782 603 41 0 7274 0
vsize: 29260
[startup+200.018 s]
Raw data (loadavg): 0.98 0.90 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6805 0 0 0 19974 28 0 0 25 0 1 0 546981338 29962240 6782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6782 603 41 0 7274 0
vsize: 29260
[startup+210.019 s]
Raw data (loadavg): 1.05 0.92 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6805 0 0 0 20973 28 0 0 25 0 1 0 546981338 29962240 6782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6782 603 41 0 7274 0
vsize: 29260
[startup+220.019 s]
Raw data (loadavg): 1.04 0.93 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 6805 0 0 0 21973 29 0 0 25 0 1 0 546981338 29962240 6782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7315 6782 603 41 0 7274 0
vsize: 29260
[startup+230.02 s]
Raw data (loadavg): 1.04 0.93 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 7074 0 0 0 22971 30 0 0 25 0 1 0 546981338 31031296 7051 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7576 7051 603 41 0 7535 0
vsize: 30304
[startup+240.02 s]
Raw data (loadavg): 1.03 0.93 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 7538 0 0 0 23969 32 0 0 25 0 1 0 546981338 32911360 7515 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8035 7515 603 41 0 7994 0
vsize: 32140
[startup+250.02 s]
Raw data (loadavg): 1.02 0.93 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 7984 0 0 0 24967 35 0 0 25 0 1 0 546981338 34791424 7961 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 7961 603 41 0 8453 0
vsize: 33976
[startup+260.021 s]
Raw data (loadavg): 1.02 0.93 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 8181 0 0 0 25966 36 0 0 25 0 1 0 546981338 35598336 8158 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8691 8158 603 41 0 8650 0
vsize: 34764
[startup+270.02 s]
Raw data (loadavg): 1.02 0.94 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 8181 0 0 0 26966 36 0 0 25 0 1 0 546981338 35598336 8158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8691 8158 603 41 0 8650 0
vsize: 34764
[startup+280.021 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 8181 0 0 0 27966 36 0 0 25 0 1 0 546981338 35598336 8158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8691 8158 603 41 0 8650 0
vsize: 34764
[startup+290.022 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 8181 0 0 0 28966 37 0 0 25 0 1 0 546981338 35598336 8158 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8691 8158 603 41 0 8650 0
vsize: 34764
[startup+300.022 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 8181 0 0 0 29965 37 0 0 25 0 1 0 546981338 35598336 8158 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8691 8158 603 41 0 8650 0
vsize: 34764
[startup+310.023 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 8181 0 0 0 30965 37 0 0 25 0 1 0 546981338 35598336 8158 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8691 8158 603 41 0 8650 0
vsize: 34764
[startup+320.023 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 8524 0 0 0 31964 38 0 0 25 0 1 0 546981338 36925440 8501 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9015 8501 603 41 0 8974 0
vsize: 36060
[startup+330.023 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 9611 0 0 0 32960 43 0 0 25 0 1 0 546981338 41369600 9588 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10100 9588 603 41 0 10059 0
vsize: 40400
[startup+340.023 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 10284 0 0 0 33959 44 0 0 25 0 1 0 546981338 44183552 10261 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10787 10261 603 41 0 10746 0
vsize: 43148
[startup+350.023 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 11020 0 0 0 34957 46 0 0 25 0 1 0 546981338 47132672 10997 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11507 10997 603 41 0 11466 0
vsize: 46028
[startup+360.024 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 11482 0 0 0 35956 48 0 0 25 0 1 0 546981338 49278976 11459 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12031 11459 603 41 0 11990 0
vsize: 48124
[startup+370.024 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 12123 0 0 0 36954 49 0 0 25 0 1 0 546981338 51970048 12100 4294967295 134512640 134672761 3221224544 3221223728 134558875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12688 12100 603 41 0 12647 0
vsize: 50752
[startup+380.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 12753 0 0 0 37952 51 0 0 25 0 1 0 546981338 54517760 12730 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13310 12730 603 41 0 13269 0
vsize: 53240
[startup+390.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13431 0 0 0 38950 53 0 0 25 0 1 0 546981338 57335808 13408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13998 13408 603 41 0 13957 0
vsize: 55992
[startup+400.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 39949 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223500 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+410.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 40949 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+420.025 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 41949 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+430.026 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 42949 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+440.025 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 43949 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+450.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 44950 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+460.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 45950 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+470.025 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 46950 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+480.025 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 47950 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+490.025 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 48950 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+500.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 49950 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+510.025 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 50951 54 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+520.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 13735 0 0 0 51951 55 0 0 25 0 1 0 546981338 58548224 13712 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14294 13712 603 41 0 14253 0
vsize: 57176
[startup+530.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 14031 0 0 0 52950 55 0 0 25 0 1 0 546981338 59756544 14008 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14589 14008 603 41 0 14548 0
vsize: 58356
[startup+540.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 14535 0 0 0 53949 56 0 0 25 0 1 0 546981338 61784064 14512 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15084 14512 603 41 0 15043 0
vsize: 60336
[startup+550.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 15160 0 0 0 54947 58 0 0 25 0 1 0 546981338 64327680 15137 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15705 15137 603 41 0 15664 0
vsize: 62820
[startup+560.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 16108 0 0 0 55946 60 0 0 25 0 1 0 546981338 68231168 16085 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16658 16085 603 41 0 16617 0
vsize: 66632
[startup+570.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 16753 0 0 0 56943 63 0 0 25 0 1 0 546981338 70909952 16730 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17312 16730 603 41 0 17271 0
vsize: 69248
[startup+580.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 57941 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+590.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 58942 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+600.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 59942 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+610.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 60942 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+620.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 61941 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+630.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 62942 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+640.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 63942 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+650.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 64942 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+660.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 65942 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+670.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 66942 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+680.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 67942 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+690.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 68941 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+700.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 69940 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+710.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 70940 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+720.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 71940 64 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+730.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 72940 65 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+740.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17004 0 0 0 73940 65 0 0 25 0 1 0 546981338 71847936 16981 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16981 603 41 0 17500 0
vsize: 70164
[startup+750.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 74940 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+760.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 75940 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+770.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 76941 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+780.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 77941 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+790.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 78941 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+800.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 79941 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223728 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+810.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 80941 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+820.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 81942 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+830.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 82941 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+840.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 83942 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+850.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 84942 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+860.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 85941 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+870.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 86940 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+880.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 87940 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+890.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9523
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17005 0 0 0 88940 65 0 0 25 0 1 0 546981338 71847936 16982 4294967295 134512640 134672761 3221224544 3221223600 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16982 603 41 0 17500 0
vsize: 70164
[startup+900.028 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 9576
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17006 0 0 0 89937 68 0 0 25 0 1 0 546981338 71847936 16983 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16983 603 41 0 17500 0
vsize: 70164
[startup+910.027 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 9576
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17006 0 0 0 90937 68 0 0 25 0 1 0 546981338 71847936 16983 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16983 603 41 0 17500 0
vsize: 70164
[startup+920.027 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 9576
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17006 0 0 0 91937 68 0 0 25 0 1 0 546981338 71847936 16983 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16983 603 41 0 17500 0
vsize: 70164
[startup+930.027 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 9576
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17007 0 0 0 92937 68 0 0 25 0 1 0 546981338 71847936 16984 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16984 603 41 0 17500 0
vsize: 70164
[startup+940.028 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 9576
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17009 0 0 0 93937 68 0 0 25 0 1 0 546981338 71847936 16986 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16986 603 41 0 17500 0
vsize: 70164
[startup+950.028 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 9576
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17012 0 0 0 94938 68 0 0 25 0 1 0 546981338 71847936 16989 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16989 603 41 0 17500 0
vsize: 70164
[startup+960.027 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 9576
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17170 0 0 0 95937 69 0 0 25 0 1 0 546981338 72515584 17147 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17704 17147 603 41 0 17663 0
vsize: 70816
[startup+970.027 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 96936 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+980.027 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 97937 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+990.027 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 98937 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1000.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 99937 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1010.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 100937 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1020.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 101937 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1030.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 102937 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 103937 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 104938 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 105938 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 106938 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 107938 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 108938 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 17543 0 0 0 109938 70 0 0 25 0 1 0 546981338 74117120 17520 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 17520 603 41 0 18054 0
vsize: 72380
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 18009 0 0 0 110937 72 0 0 25 0 1 0 546981338 76005376 17986 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18556 17986 603 41 0 18515 0
vsize: 74224
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 18549 0 0 0 111934 75 0 0 25 0 1 0 546981338 78168064 18526 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 18526 603 41 0 19043 0
vsize: 76336
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 19083 0 0 0 112933 76 0 0 25 0 1 0 546981338 80441344 19060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19639 19060 603 41 0 19598 0
vsize: 78556
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 19577 0 0 0 113932 77 0 0 25 0 1 0 546981338 82460672 19554 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20132 19554 603 41 0 20091 0
vsize: 80528
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 20090 0 0 0 114930 79 0 0 25 0 1 0 546981338 84475904 20067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20624 20067 603 41 0 20583 0
vsize: 82496
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 20545 0 0 0 115929 81 0 0 25 0 1 0 546981338 86355968 20522 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21083 20522 603 41 0 21042 0
vsize: 84332
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 21011 0 0 0 116928 82 0 0 25 0 1 0 546981338 88248320 20988 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21545 20988 603 41 0 21504 0
vsize: 86180
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 21574 0 0 0 117926 84 0 0 25 0 1 0 546981338 90669056 21551 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22136 21551 603 41 0 22095 0
vsize: 88544
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 22130 0 0 0 118925 86 0 0 25 0 1 0 546981338 92938240 22107 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22690 22107 603 41 0 22649 0
vsize: 90760
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 9578
Raw data (stat): 9523 (minisat+) R 9522 3260 3259 0 -1 0 22130 0 0 0 119925 86 0 0 25 0 1 0 546981338 92938240 22107 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22690 22107 603 41 0 22649 0
vsize: 90760
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 9578
Raw data (stat): 9523 (minisat+) Z 9522 3260 3259 0 -1 12 22133 0 0 0 119925 90 0 0 25 0 1 0 546981338 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.07
CPU time (s): 1200.16
CPU user time (s): 1199.26
CPU system time (s): 0.901862
CPU usage (%): 100.007
Max. virtual memory (Kb): 90760
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####