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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-misc07.opb
MD5SUM	b95827c7e083aae37933a3b226b8189b
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1076833280
Optimality of the best value was proved	NO
Number of terms in the objective function	31
Biggest coefficient in the objective function	1073741824
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	2147483647
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	1073741824
Number of bits of the biggest number in a constraint	31
Biggest sum of numbers in a constraint	3287948287
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1243.78
Number of variables	290
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	263
Trace number 30834

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-05-25 20:00:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22230 boxname=wulflinc30 idbench=1046 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  b95827c7e083aae37933a3b226b8189b  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-misc07.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-misc07.opb
IDLAUNCH: 22230
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        893556 kB
Buffers:          5684 kB
Cached:         114404 kB
SwapCached:        612 kB
Active:          16844 kB
Inactive:       105272 kB
HighTotal:      131008 kB
HighFree:        20916 kB
LowTotal:       903652 kB
LowFree:        872640 kB
SwapTotal:     2097892 kB
SwapFree:      2096344 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5020 kB
Slab:            13300 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 20:20:41 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 22230 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1708   maxlim: 1073742847   bits: 32/31
c ---[ 243]---> BDD-cost:   51
c ---[ 241]---> BDD-cost:   51
c ---[ 239]---> BDD-cost:   51
c ---[ 237]---> BDD-cost:   51
c ---[ 235]---> BDD-cost:   51
c ---[ 233]---> BDD-cost:   51
c ---[ 231]---> BDD-cost:   51
c ---[ 230]---> BDD-cost:  239
c ---[ 229]---> BDD-cost:  239
c ---[ 228]---> BDD-cost:  239
c ---[  99]---> Sorter-cost:  127     Base:
c ---[  97]---> Sorter-cost:  127     Base:
c ---[  95]---> Sorter-cost:  127     Base:
c ---[  93]---> Sorter-cost:  127     Base:
c ---[  91]---> Sorter-cost:  127     Base:
c ---[  89]---> Sorter-cost:  127     Base:
c ---[  87]---> Sorter-cost:  127     Base:
c ---[  85]---> Sorter-cost:  127     Base:
c ---[  83]---> Sorter-cost:  127     Base:
c ---[  81]---> Sorter-cost:  127     Base:
c ---[  79]---> Sorter-cost:  127     Base:
c ---[  77]---> Sorter-cost:  127     Base:
c ---[  75]---> Sorter-cost:  127     Base:
c ---[  73]---> Sorter-cost:  127     Base:
c ---[  71]---> Sorter-cost:  127     Base:
c ---[  69]---> Sorter-cost:  127     Base:
c ---[  67]---> Sorter-cost:  127     Base:
c ---[  65]---> Sorter-cost:  127     Base:
c ---[  63]---> Sorter-cost:  127     Base:
c ---[  61]---> Sorter-cost:  127     Base:
c ---[  59]---> Sorter-cost:  127     Base:
c ---[  57]---> Sorter-cost:  127     Base:
c ---[  55]---> Sorter-cost:  127     Base:
c ---[  53]---> Sorter-cost:  127     Base:
c ---[  51]---> Sorter-cost:  127     Base:
c ---[  49]---> Sorter-cost:  127     Base:
c ---[  47]---> Sorter-cost:  127     Base:
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   50
c ---[  34]---> BDD-cost:   50
c ---[  33]---> BDD-cost:   50
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   48
c ---[  28]---> BDD-cost:   48
c ---[  27]---> BDD-cost:   48
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   50
c ---[  22]---> BDD-cost:   50
c ---[  21]---> BDD-cost:   50
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   48
c ---[  16]---> BDD-cost:   48
c ---[  15]---> BDD-cost:   48
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   50
c ---[  10]---> BDD-cost:   50
c ---[   9]---> BDD-cost:   50
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:   48
c ---[   3]---> BDD-cost:   48
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25851    84536 |    8617       0        0     nan |  0.000 % |
c |       104 |   25851    84536 |    9478     104     7124    68.5 |  2.893 % |
c |       256 |   25851    84536 |   10426     256    17140    67.0 |  2.893 % |
c ==============================================================================
c [1mFound solution: 1079690240[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       296 |   25863    84565 |    8621     295    19414    65.8 |  2.893 % |
c ==============================================================================
c [1mFound solution: 1078323200[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       323 |   25870    84582 |    8623     321    21042    65.6 |  2.893 % |
c ==============================================================================
c [1mFound solution: 1078266880[0m
c ---[   0]---> BDD-cost:   20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       372 |   25894    84635 |    8631     370    28469    76.9 |  2.893 % |
c |       472 |   25894    84635 |    9494     470    29235    62.2 |  3.011 % |
c ==============================================================================
c [1mFound solution: 1077698560[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       494 |   25910    84673 |    8636     492    29561    60.1 |  3.011 % |
c ==============================================================================
c [1mFound solution: 1077314560[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       517 |   25929    84717 |    8643     515    30376    59.0 |  3.011 % |
c |       618 |   25922    84702 |    9507     615    41587    67.6 |  3.063 % |
c |       769 |   25911    84678 |   10458     765    49337    64.5 |  3.106 % |
c |       995 |   25911    84678 |   11503     991    56584    57.1 |  3.106 % |
c |      1333 |   25911    84678 |   12654    1329   112538    84.7 |  3.106 % |
c |      1840 |   25911    84678 |   13919    1836   148255    80.7 |  3.106 % |
c |      2600 |   25911    84678 |   15311    2596   244986    94.4 |  3.106 % |
c |      3739 |   25911    84678 |   16842    3735   348506    93.3 |  3.106 % |
c |      5448 |   25890    84603 |   18527    5440   514853    94.6 |  3.120 % |
c |      8010 |   25879    84579 |   20379    8001   765920    95.7 |  3.163 % |
c ==============================================================================
c [1mFound solution: 1077242880[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10195 |   25827    84467 |    8609   10176  1004432    98.7 |  3.163 % |
c |     10297 |   25816    84443 |    9469    5189   444650    85.7 |  3.516 % |
c |     10447 |   25816    84443 |   10416    5339   462777    86.7 |  3.516 % |
c |     10674 |   25805    84419 |   11458    5564   476714    85.7 |  3.559 % |
c |     11012 |   25805    84419 |   12604    5902   500179    84.7 |  3.559 % |
c |     11520 |   25805    84419 |   13864    6410   561591    87.6 |  3.559 % |
c |     12280 |   25805    84419 |   15251    7170   618280    86.2 |  3.559 % |
c ==============================================================================
c [1mFound solution: 1077038080[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12859 |   25826    84466 |    8608    7749   708816    91.5 |  3.559 % |
c |     12959 |   25826    84466 |    9468    7849   712677    90.8 |  3.569 % |
c ==============================================================================
c [1mFound solution: 1076966400[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13059 |   25848    84516 |    8616    7949   721699    90.8 |  3.569 % |
c |     13162 |   25841    84501 |    9477    8051   726099    90.2 |  3.608 % |
c |     13312 |   25841    84501 |   10425    8201   733729    89.5 |  3.608 % |
c |     13537 |   25826    84448 |   11467    8424   754034    89.5 |  3.622 % |
c |     13876 |   25826    84448 |   12614    8763   772627    88.2 |  3.622 % |
c |     14382 |   25778    84276 |   13876    9260   841268    90.8 |  3.650 % |
c |     15141 |   25751    84181 |   15263   10017   958101    95.6 |  3.679 % |
c |     16281 |   25700    84002 |   16790   11154  1049169    94.1 |  3.736 % |
c |     17990 |   25700    84002 |   18469   12863  1231456    95.7 |  3.736 % |
c |     20553 |   25672    83912 |   20316   15417  1531371    99.3 |  3.779 % |
c |     24399 |   25610    83711 |   22347   19256  1962822   101.9 |  3.893 % |
c ==============================================================================
c [1mFound solution: 1076894720[0m
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28190 |   25507    83322 |    8502   11546   969479    84.0 |  3.893 % |
c |     28290 |   25507    83322 |    9352    5873   358661    61.1 |  4.089 % |
c |     28441 |   25494    83292 |   10287    6023   366709    60.9 |  4.132 % |
c |     28666 |   25487    83277 |   11316    6247   377997    60.5 |  4.161 % |
c |     29005 |   25457    83210 |   12447    6582   419453    63.7 |  4.289 % |
c |     29511 |   25429    83148 |   13692    7085   466980    65.9 |  4.403 % |
c |     30271 |   25429    83148 |   15061    7845   576063    73.4 |  4.403 % |
c |     31411 |   25396    83075 |   16567    8979   701551    78.1 |  4.545 % |
c |     33120 |   25396    83075 |   18224   10688   814670    76.2 |  4.545 % |
c |     35682 |   25364    82976 |   20047   13245  1087489    82.1 |  4.602 % |
c |     39526 |   25349    82943 |   22051   17087  1405644    82.3 |  4.659 % |
c |     45293 |   25336    82913 |   24257   22851  2037510    89.2 |  4.702 % |
c ==============================================================================
c [1mFound solution: 1076874240[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52953 |   25322    82886 |    8440   17704  1479433    83.6 |  4.702 % |
c |     53054 |   25322    82886 |    9284    4527   245352    54.2 |  4.827 % |
c |     53204 |   25322    82886 |   10212    4677   262079    56.0 |  4.827 % |
c |     53429 |   25322    82886 |   11233    4902   294471    60.1 |  4.827 % |
c |     53770 |   25311    82862 |   12357    5239   313658    59.9 |  4.870 % |
c |     54278 |   25311    82862 |   13592    5747   374383    65.1 |  4.870 % |
c ==============================================================================
c [1mFound solution: 1076782080[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54685 |   25331    82909 |    8443    6154   409485    66.5 |  4.870 % |
c |     54785 |   25331    82909 |    9287    6254   428634    68.5 |  4.878 % |
c |     54935 |   25289    82761 |   10216    6397   431936    67.5 |  4.921 % |
c |     55160 |   25289    82761 |   11237    6622   466517    70.4 |  4.921 % |
c |     55499 |   25289    82761 |   12361    6961   487416    70.0 |  4.921 % |
c |     56006 |   25289    82761 |   13597    7468   532027    71.2 |  4.921 % |
c |     56766 |   25289    82761 |   14957    8228   668807    81.3 |  4.921 % |
c |     57905 |   25258    82689 |   16453    9362   742735    79.3 |  5.049 % |
c |     59615 |   25258    82689 |   18098   11072  1088873    98.3 |  5.049 % |
c |     62177 |   25247    82665 |   19908   13633  1412537   103.6 |  5.092 % |
c |     66022 |   25247    82665 |   21898   17478  2033583   116.4 |  5.092 % |
c |     71788 |   25203    82569 |   24088   23235  2733119   117.6 |  5.262 % |
c ==============================================================================
c [1mFound solution: 1076761600[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74726 |   25195    82553 |    8398   13734  1260018    91.7 |  5.262 % |
c |     74826 |   25195    82553 |    9237    6967   453239    65.1 |  5.385 % |
c ==============================================================================
c [1mFound solution: 1076751360[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74874 |   25212    82593 |    8404    7015   459095    65.4 |  5.385 % |
c |     74975 |   25212    82593 |    9244    7116   477340    67.1 |  5.394 % |
c |     75125 |   25212    82593 |   10168    7266   494117    68.0 |  5.394 % |
c |     75350 |   25212    82593 |   11185    7491   522357    69.7 |  5.394 % |
c |     75688 |   25197    82540 |   12304    7825   538749    68.8 |  5.408 % |
c |     76194 |   25197    82540 |   13534    8331   606164    72.8 |  5.408 % |
c |     76954 |   25197    82540 |   14888    9091   654969    72.0 |  5.408 % |
c ==============================================================================
c [1mFound solution: 1076674560[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77808 |   25215    82581 |    8405    9945   737772    74.2 |  5.408 % |
c |     77909 |   25215    82581 |    9245    5074   240734    47.4 |  5.417 % |
c |     78063 |   25215    82581 |   10170    5228   257316    49.2 |  5.417 % |
c |     78289 |   25215    82581 |   11187    5454   294967    54.1 |  5.417 % |
c |     78627 |   25181    82505 |   12305    5787   344344    59.5 |  5.559 % |
c |     79135 |   25136    82350 |   13536    6289   388408    61.8 |  5.630 % |
c |     79895 |   25119    82312 |   14889    7046   480518    68.2 |  5.701 % |
c |     81034 |   25076    82177 |   16378    8173   542345    66.4 |  5.786 % |
c |     82746 |   25076    82177 |   18016    9885   688880    69.7 |  5.786 % |
c |     85308 |   25003    81922 |   19818   12441   892373    71.7 |  5.913 % |
c |     89152 |   25003    81922 |   21800   16285  1441242    88.5 |  5.913 % |
c |     94918 |   24935    81769 |   23980   22039  2177928    98.8 |  6.183 % |
c |    103571 |   24896    81636 |   26378   18314  1491054    81.4 |  6.254 % |
c |    116545 |   24814    81440 |   29016   17743  1495439    84.3 |  6.580 % |
c |    136006 |   24799    81407 |   31917   21079  1891760    89.7 |  6.636 % |
c |    165198 |   24688    81017 |   35109   33834  3143968    92.9 |  6.807 % |
c |    208987 |   24673    80984 |   38620   19203  1780897    92.7 |  6.863 % |
c ==============================================================================
c [1mFound solution: 1076618240[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    253521 |   24607    80838 |    8202   18865  1615533    85.6 |  6.863 % |
c |    253621 |   24607    80838 |    9022    4817   175033    36.3 |  7.239 % |
c |    253771 |   24512    80515 |    9924    4961   179668    36.2 |  7.409 % |
c |    253997 |   24503    80484 |   10916    5186   188074    36.3 |  7.423 % |
c |    254338 |   24503    80484 |   12008    5527   210289    38.0 |  7.423 % |
c |    254844 |   24503    80484 |   13209    6033   293382    48.6 |  7.423 % |
c |    255604 |   24482    80409 |   14530    6788   345575    50.9 |  7.437 % |
c |    256744 |   24423    80204 |   15983    7921   446794    56.4 |  7.536 % |
c |    258452 |   24423    80204 |   17581    9629   603606    62.7 |  7.537 % |
c |    261014 |   24412    80180 |   19339   12190   855267    70.2 |  7.579 % |
c |    264859 |   24395    80142 |   21273   16034  1234638    77.0 |  7.650 % |
c |    270626 |   24377    80103 |   23401   21798  1861692    85.4 |  7.721 % |
c |    279276 |   24377    80103 |   25741   18005  1530883    85.0 |  7.721 % |
c |    292253 |   24377    80103 |   28315   16155  1842790   114.1 |  7.721 % |
c |    311714 |   24362    80062 |   31147   20479  1375415    67.2 |  7.763 % |
c |    340906 |   24340    80013 |   34261   16236  1091140    67.2 |  7.862 % |
c |    384695 |   24340    80013 |   37687   19232  1909595    99.3 |  7.862 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 10370 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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): 1.00 0.99 0.96 2/54 10366
Raw data (stat): 10366 (runsolver) R 10365 22056 22055 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841586462 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.99996 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10370
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0001 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10370
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0008 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10370
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0003 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10370
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10370
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0013 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10370
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.004 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.004 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.005 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.004 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.005 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.005 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.005 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.008 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.008 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.008 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.009 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.009 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.01 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.01 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.01 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10372
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.01 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.009 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.01 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.01 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.01 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.011 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.011 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.012 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.012 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.012 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.012 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.012 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.013 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.013 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.013 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.013 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.024 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.024 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.025 s]
Raw data (loadavg): 1.00 0.99 0.96 3/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.026 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.026 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.026 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.027 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.96 3/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.68 s]
Raw data (loadavg): 1.00 0.99 0.96 1/53 10374
Raw data (stat): 10366 (minisat+_script) S 10365 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841586462 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.68
CPU time (s): 1229.85
CPU user time (s): 1229.48
CPU system time (s): 0.371943
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####