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/miplib3/normalized-mps-v2-13-7-gt2.opb
MD5SUM	f1382105ee9fb79777762a53cf6a73c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	21166
Optimality of the best value was proved	NO
Number of terms in the objective function	304
Biggest coefficient in the objective function	62376
Number of bits for the biggest coefficient in the objective function	16
Sum of the numbers in the objective function	3092598
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	62376
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	3092598
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.14
Number of variables	556
Total number of constraints	217
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	26
Number of constraints which are nor clauses,nor cardinality constraints	191
Minimum length of a constraint	1
Maximum length of a constraint	48
Trace number 18217

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 13:58:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18439 boxname=wulflinc13 idbench=1419 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  f1382105ee9fb79777762a53cf6a73c1  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-gt2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-gt2.opb
IDLAUNCH: 18439
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        384896 kB
Buffers:         35392 kB
Cached:         592072 kB
SwapCached:        176 kB
Active:         270664 kB
Inactive:       359628 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        384644 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            13872 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:18:07 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 18439 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................ssssssssss
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  71]---> BDD-cost:    2
c ---[  70]---> BDD-cost:    2
c ---[  68]---> BDD-cost:    2
c ---[  64]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  37]---> BDD-cost:  107
c ---[  36]---> Sorter-cost:  778     Base: 2 2 2
c ---[  35]---> Sorter-cost:  777     Base: 2 2 2
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:  183
c ---[  31]---> BDD-cost:   25
c ---[  30]---> Sorter-cost:  379     Base: 2 2 2
c ---[  29]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  128
c ---[  27]---> BDD-cost:  105
c ---[  26]---> Sorter-cost:  778     Base: 2 2 2
c ---[  25]---> BDD-cost:  111
c ---[  24]---> BDD-cost:  105
c ---[  23]---> BDD-cost:   54
c ---[  22]---> BDD-cost:   54
c ---[  21]---> BDD-cost:   21
c ---[  15]---> Adder-cost: 273   maxlim: 12127   bits: 15/14
c ---[   9]---> Sorter-cost: 2085     Base: 2 5 2 2 2
c ---[   8]---> BDD-cost:   76
c ---[   7]---> Sorter-cost: 2550     Base: 2 5 2 2 2
c ---[   6]---> Adder-cost: 223   maxlim: 249   bits: 9/8
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:  114
c ---[   3]---> BDD-cost:   55
c ---[   2]---> Sorter-cost: 2935     Base: 2 5 2 2 2 2
c ---[   1]---> Adder-cost: 212   maxlim: 230   bits: 9/8
c ---[   0]---> BDD-cost:   92
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   30742    79537 |   10247       0        0     nan |  0.000 % |
c |       100 |   30742    79537 |   11271     100      544     5.4 |  0.987 % |
c |       250 |   30742    79537 |   12398     250     2459     9.8 |  0.986 % |
c |       477 |   30742    79537 |   13638     477     3973     8.3 |  0.986 % |
c ==============================================================================
c [1mFound solution: 175459[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:92424     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       637 |  284458   671673 |   94819     637    11349    17.8 |  0.986 % |
c |       737 |  284437   671627 |  104300     735    12835    17.5 |  0.117 % |
c |       887 |  284035   670723 |  114730     880    13845    15.7 |  0.221 % |
c |      1114 |  284035   670723 |  126204    1107    15250    13.8 |  0.221 % |
c |      1451 |  284035   670723 |  138824    1444    17597    12.2 |  0.221 % |
c |      1958 |  282828   667995 |  152706    1939    63559    32.8 |  0.549 % |
c |      2717 |  282661   667617 |  167977    2697   148878    55.2 |  0.596 % |
c |      3856 |  271841   642801 |  184775    3781   190178    50.3 |  3.911 % |
c |      5565 |  267485   632765 |  203252    5455   244772    44.9 |  5.294 % |
c |      8129 |  258374   611785 |  223578    7920   366516    46.3 |  8.175 % |
c |     11974 |  255958   606212 |  245936   11748   726453    61.8 |  8.939 % |
c |     17740 |  250695   594032 |  270529   17444  1194291    68.5 | 10.666 % |
c |     26390 |  249167   590517 |  297582   26068  1851301    71.0 | 11.165 % |
c |     39364 |  243608   577673 |  327340   38951  2440127    62.6 | 12.969 % |
c ==============================================================================
c [1mFound solution: 174126[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70620     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57904 |  404098   950841 |  134699   57401  4098734    71.4 | 12.969 % |
c |     58008 |  403639   949827 |  148168   57502  4100867    71.3 | 14.245 % |
c |     58159 |  402994   948375 |  162985   57644  4103732    71.2 | 14.375 % |
c |     58384 |  402994   948375 |  179284   57869  4109174    71.0 | 14.375 % |
c |     58721 |  401268   944466 |  197212   58185  4111678    70.7 | 14.715 % |
c |     59229 |  401268   944466 |  216934   58693  4136023    70.5 | 14.715 % |
c |     59988 |  401268   944466 |  238627   59452  4283010    72.0 | 14.715 % |
c |     61127 |  401110   944098 |  262490   60582  4296313    70.9 | 14.748 % |
c |     62836 |  400965   943764 |  288739   62290  4391753    70.5 | 14.776 % |
c |     65398 |  397076   934924 |  317613   64748  4501421    69.5 | 15.543 % |
c |     69242 |  396305   933196 |  349374   68585  4939320    72.0 | 15.693 % |
c ==============================================================================
c [1mFound solution: 172189[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:69141     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73398 |  544035  1277084 |  181345   72562  5065701    69.8 | 15.693 % |
c |     73498 |  544035  1277084 |  199479   72662  5068684    69.8 | 16.507 % |
c |     73648 |  544035  1277084 |  219427   72812  5070213    69.6 | 16.507 % |
c |     73873 |  543068  1274852 |  241370   72952  5097260    69.9 | 16.641 % |
c |     74210 |  540987  1270145 |  265507   73257  5099628    69.6 | 16.928 % |
c |     74716 |  540190  1268331 |  292057   73706  5103053    69.2 | 17.043 % |
c |     75475 |  536077  1259024 |  321263   74187  5111911    68.9 | 17.612 % |
c |     76614 |  536077  1259024 |  353390   75326  5156748    68.5 | 17.612 % |
c |     78323 |  530933  1247267 |  388729   76556  5221852    68.2 | 18.328 % |
c ==============================================================================
c [1mFound solution: 165654[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78741 |  531464  1248864 |  177154   76974  5254301    68.3 | 18.328 % |
c |     78842 |  530814  1247415 |  194869   77072  5256580    68.2 | 18.396 % |
c |     78994 |  530399  1246465 |  214356   77218  5264119    68.2 | 18.455 % |
c |     79219 |  530399  1246465 |  235791   77443  5280849    68.2 | 18.455 % |
c |     79556 |  530293  1246228 |  259371   77779  5290167    68.0 | 18.466 % |
c |     80062 |  530239  1246109 |  285308   78283  5319511    68.0 | 18.473 % |
c |     80821 |  530239  1246109 |  313839   79042  5399819    68.3 | 18.473 % |
c |     81960 |  530034  1245656 |  345223   80180  5665661    70.7 | 18.500 % |
c |     83669 |  524072  1232048 |  379745   81399  5764458    70.8 | 19.341 % |
c |     86231 |  522340  1228063 |  417719   83937  5900609    70.3 | 19.584 % |
c ==============================================================================
c [1mFound solution: 165192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:68242     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87232 |  675287  1583479 |  225095   84938  6115837    72.0 | 19.584 % |
c |     87332 |  675287  1583479 |  247604   85038  6117351    71.9 | 19.030 % |
c |     87483 |  673704  1579889 |  272364   85180  6121380    71.9 | 19.205 % |
c |     87709 |  673704  1579889 |  299601   85406  6147900    72.0 | 19.205 % |
c |     88046 |  673704  1579889 |  329561   85743  6190662    72.2 | 19.205 % |
c |     88553 |  673704  1579889 |  362517   86250  6204900    71.9 | 19.205 % |
c |     89314 |  673704  1579889 |  398769   87011  6265601    72.0 | 19.205 % |
c |     90456 |  668664  1568463 |  438646   88034  6376824    72.4 | 19.756 % |
c |     92164 |  666346  1563278 |  482511   89724  6660716    74.2 | 20.003 % |
c |     94726 |  666346  1563278 |  530762   92286  7009786    76.0 | 20.003 % |
c |     98570 |  664362  1558830 |  583838   96127  7652673    79.6 | 20.223 % |
c ==============================================================================
c [1mFound solution: 164617[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98680 |  664408  1559385 |  221469   96237  7659605    79.6 | 20.223 % |
c |     98781 |  664408  1559385 |  243615   96338  7666260    79.6 | 20.222 % |
c |     98931 |  663882  1558213 |  267977   96478  7669094    79.5 | 20.280 % |
c |     99156 |  663882  1558213 |  294775   96703  7674639    79.4 | 20.280 % |
c |     99494 |  663882  1558213 |  324252   97041  7682075    79.2 | 20.280 % |
c |    100000 |  662711  1555549 |  356678   97537  7702428    79.0 | 20.411 % |
c |    100761 |  658022  1544826 |  392345   98090  7724938    78.8 | 20.924 % |
c |    101902 |  657896  1544545 |  431580   99228  7828742    78.9 | 20.939 % |
c |    103612 |  656006  1540264 |  474738  100809  7919978    78.6 | 21.151 % |
c |    106174 |  653447  1534433 |  522212  103311  8338281    80.7 | 21.441 % |
c |    110018 |  653447  1534433 |  574433  107155  8992194    83.9 | 21.441 % |
c |    115784 |  650518  1527749 |  631876  112772  9214928    81.7 | 21.761 % |
c |    124433 |  650518  1527749 |  695064  121421  9889029    81.4 | 21.761 % |
c ==============================================================================
c [1mFound solution: 163483[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131430 |  646191  1517922 |  215397  128336 10361434    80.7 | 21.761 % |
c |    131530 |  646191  1517922 |  236936  128436 10366789    80.7 | 22.242 % |
c |    131680 |  646026  1517552 |  260630  128583 10382200    80.7 | 22.260 % |
c |    131906 |  646026  1517552 |  286693  128809 10384118    80.6 | 22.260 % |
c |    132243 |  646026  1517552 |  315362  129146 10387012    80.4 | 22.260 % |
c |    132750 |  645201  1515676 |  346899  129631 10391486    80.2 | 22.349 % |
c |    133510 |  642926  1510464 |  381588  130236 10419037    80.0 | 22.602 % |
c |    134650 |  642926  1510464 |  419747  131376 10465729    79.7 | 22.602 % |
c ==============================================================================
c [1mFound solution: 161824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    135225 |  642822  1510228 |  214274  131950 10510329    79.7 | 22.602 % |
c |    135328 |  642822  1510228 |  235701  132053 10515914    79.6 | 22.614 % |
c |    135478 |  642047  1508455 |  259271  132190 10518344    79.6 | 22.694 % |
c |    135703 |  642047  1508455 |  285198  132415 10522658    79.5 | 22.694 % |
c |    136040 |  641491  1507180 |  313718  132743 10524190    79.3 | 22.755 % |
c |    136547 |  641393  1506955 |  345090  133249 10584627    79.4 | 22.766 % |
c |    137306 |  641201  1506523 |  379599  134000 10677526    79.7 | 22.785 % |
c |    138445 |  640805  1505618 |  417559  135124 10695361    79.2 | 22.828 % |
c |    140154 |  637215  1497411 |  459315  136401 10708038    78.5 | 23.224 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x_0x2e__0x2e__0x2e_0101_bit0 -x_0x2e__0x2e__0x2e_0101_bit1 -x_0x2e__0x2e__0x2e_0101_bit2 -x_0x2e__0x2e__0x2e_0101_bit3 -x_0x2e__0x2e__0x2e_0201_bit0 -x_0x2e__0x2e__0x2e_0201_bit1 -x_0x2e__0x2e__0x2e_0201_bit2 -x_0x2e__0x2e__0x2e_0201_bit3 -x_0x2e__0x2e__0x2e_0301_bit0 -x_0x2e__0x2e__0x2e_0301_bit1 x_0x2e__0x2e__0x2e_0301_bit2 -x_0x2e__0x2e__0x2e_0301_bit3 -x_0x2e__0x2e__0x2e_0401_bit0 -x_0x2e__0x2e__0x2e_0401_bit1 -x_0x2e__0x2e__0x2e_0401_bit2 -x_0x2e__0x2e__0x2e_0401_bit3 -x_0x2e__0x2e__0x2e_0701_bit0 -x_0x2e__0x2e__0x2e_0701_bit1 -x_0x2e__0x2e__0x2e_0701_bit2 -x_0x2e__0x2e__0x2e_0701_bit3 -x_0x2e__0x2e__0x2e_0801_bit0 -x_0x2e__0x2e__0x2e_0801_bit1 -x_0x2e__0x2e__0x2e_0801_bit2 -x_0x2e__0x2e__0x2e_0801_bit3 x_0x2e__0x2e__0x2e_0901_bit0 -x_0x2e__0x2e__0x2e_0901_bit1 x_0x2e__0x2e__0x2e_0901_bit2 -x_0x2e__0x2e__0x2e_0901_bit3 -x_0x2e__0x2e__0x2e_1001_bit0 -x_0x2e__0x2e__0x2e_1001_bit1 -x_0x2e__0x2e__0x2e_1001_bit2 -x_0x2e__0x2e__0x2e_1001_bit3 -x_0x2e__0x2e__0x2e_0102_bit0 -x_0x2e__0x2e__0x2e_0102_bit1 -x_0x2e__0x2e__0x2e_0102_bit2 -x_0x2e__0x2e__0x2e_0102_bit3 -x_0x2e__0x2e__0x2e_0202_bit0 -x_0x2e__0x2e__0x2e_0202_bit1 -x_0x2e__0x2e__0x2e_0202_bit2 -x_0x2e__0x2e__0x2e_0202_bit3 -x_0x2e__0x2e__0x2e_0302_bit0 -x_0x2e__0x2e__0x2e_0302_bit1 -x_0x2e__0x2e__0x2e_0302_bit2 x_0x2e__0x2e__0x2e_0302_bit3 -x_0x2e__0x2e__0x2e_0402_bit0 -x_0x2e__0x2e__0x2e_0402_bit1 -x_0x2e__0x2e__0x2e_0402_bit2 -x_0x2e__0x2e__0x2e_0402_bit3 -x_0x2e__0x2e__0x2e_0502_bit0 -x_0x2e__0x2e__0x2e_0502_bit1 x_0x2e__0x2e__0x2e_0502_bit2 -x_0x2e__0x2e__0x2e_0502_bit3 -x_0x2e__0x2e__0x2e_0602_bit0 -x_0x2e__0x2e__0x2e_0602_bit1 -x_0x2e__0x2e__0x2e_0602_bit2 -x_0x2e__0x2e__0x2e_0602_bit3 -x_0x2e__0x2e__0x2e_0702_bit0 -x_0x2e__0x2e__0x2e_0702_bit1 -x_0x2e__0x2e__0x2e_0702_bit2 -x_0x2e__0x2e__0x2e_0702_bit3 -x_0x2e__0x2e__0x2e_0802_bit0 -x_0x2e__0x2e__0x2e_0802_bit1 -x_0x2e__0x2e__0x2e_0802_bit2 -x_0x2e__0x2e__0x2e_0802_bit3 -x_0x2e__0x2e__0x2e_0902_bit0 -x_0x2e__0x2e__0x2e_0902_bit1 -x_0x2e__0x2e__0x2e_0902_bit2 -x_0x2e__0x2e__0x2e_0902_bit3 -x_0x2e__0x2e__0x2e_1002_bit0 -x_0x2e__0x2e__0x2e_1002_bit1 -x_0x2e__0x2e__0x2e_1002_bit2 -x_0x2e__0x2e__0x2e_1002_bit3 -x_0x2e__0x2e__0x2e_1102_bit0 x_0x2e__0x2e__0x2e_1102_bit1 -x_0x2e__0x2e__0x2e_1102_bit2 -x_0x2e__0x2e__0x2e_1102_bit3 -x_0x2e__0x2e__0x2e_1202_bit0 -x_0x2e__0x2e__0x2e_1202_bit1 -x_0x2e__0x2e__0x2e_1202_bit2 -x_0x2e__0x2e__0x2e_1202_bit3 x_0x2e__0x2e__0x2e_0103_bit0 -x_0x2e__0x2e__0x2e_0103_bit1 -x_0x2e__0x2e__0x2e_0103_bit2 -x_0x2e__0x2e__0x2e_0103_bit3 x_0x2e__0x2e__0x2e_0203_bit0 -x_0x2e__0x2e__0x2e_0203_bit1 x_0x2e__0x2e__0x2e_0203_bit2 -x_0x2e__0x2e__0x2e_0203_bit3 -x_0x2e__0x2e__0x2e_0303_bit0 x_0x2e__0x2e__0x2e_0303_bit1 -x_0x2e__0x2e__0x2e_0303_bit2 -x_0x2e__0x2e__0x2e_0303_bit3 x_0x2e__0x2e__0x2e_0403_bit0 -x_0x2e__0x2e__0x2e_0403_bit1 -x_0x2e__0x2e__0x2e_0403_bit2 -x_0x2e__0x2e__0x2e_0403_bit3 -x_0x2e__0x2e__0x2e_0503_bit0 -x_0x2e__0x2e__0x2e_0503_bit1 -x_0x2e__0x2e__0x2e_0503_bit2 -x_0x2e__0x2e__0x2e_0503_bit3 -x_0x2e__0x2e__0x2e_0603_bit0 -x_0x2e__0x2e__0x2e_0603_bit1 -x_0x2e__0x2e__0x2e_0603_bit2 -x_0x2e__0x2e__0x2e_0603_bit3 x_0x2e__0x2e__0x2e_0703_bit0 -x_0x2e__0x2e__0x2e_0703_bit1 -x_0x2e__0x2e__0x2e_0703_bit2 -x_0x2e__0x2e__0x2e_0703_bit3 x_0x2e__0x2e__0x2e_0803_bit0 -x_0x2e__0x2e__0x2e_0803_bit1 -x_0x2e__0x2e__0x2e_0803_bit2 -x_0x2e__0x2e__0x2e_0803_bit3 -x_0x2e__0x2e__0x2e_0903_bit0 x_0x2e__0x2e__0x2e_0903_bit1 -x_0x2e__0x2e__0x2e_0903_bit2 -x_0x2e__0x2e__0x2e_0903_bit3 x_0x2e__0x2e__0x2e_1003_bit0 -x_0x2e__0x2e__0x2e_1003_bit1 -x_0x2e__0x2e__0x2e_1003_bit2 -x_0x2e__0x2e__0x2e_1003_bit3 -x_0x2e__0x2e__0x2e_1103_bit0 -x_0x2e__0x2e__0x2e_1103_bit1 -x_0x2e__0x2e__0x2e_1103_bit2 -x_0x2e__0x2e__0x2e_1103_bit3 -x_0x2e__0x2e__0x2e_1203_bit0 -x_0x2e__0x2e__0x2e_1203_bit1 -x_0x2e__0x2e__0x2e_1203_bit2 -x_0x2e__0x2e__0x2e_1203_bit3 -x_0x2e__0x2e__0x2e_0104_bit0 -x_0x2e__0x2e__0x2e_0204_bit0 -x_0x2e__0x2e__0x2e_0304_bit0 -x_0x2e__0x2e__0x2e_0404_bit0 -x_0x2e__0x2e__0x2e_0504_bit0 -x_0x2e__0x2e__0x2e_0604_bit0 -x_0x2e__0x2e__0x2e_0704_bit0 -x_0x2e__0x2e__0x2e_0804_bit0 -x_0x2e__0x2e__0x2e_0904_bit0 -x_0x2e__0x2e__0x2e_1004_bit0 -x_0x2e__0x2e__0x2e_1104_bit0 x_0x2e__0x2e__0x2e_1204_bit0 -x_0x2e__0x2e__0x2e_0105_bit0 -x_0x2e__0x2e__0x2e_0105_bit1 -x_0x2e__0x2e__0x2e_0105_bit2 -x_0x2e__0x2e__0x2e_0205_bit0 -x_0x2e__0x2e__0x2e_0205_bit1 -x_0x2e__0x2e__0x2e_0205_bit2 -x_0x2e__0x2e__0x2e_0305_bit0 -x_0x2e__0x2e__0x2e_0305_bit1 -x_0x2e__0x2e__0x2e_0305_bit2 -x_0x2e__0x2e__0x2e_0405_bit0 -x_0x2e__0x2e__0x2e_0405_bit1 -x_0x2e__0x2e__0x2e_0405_bit2 x_0x2e__0x2e__0x2e_0505_bit0 -x_0x2e__0x2e__0x2e_0505_bit1 -x_0x2e__0x2e__0x2e_0505_bit2 x_0x2e__0x2e__0x2e_0605_bit0 -x_0x2e__0x2e__0x2e_0605_bit1 -x_0x2e__0x2e__0x2e_0605_bit2 -x_0x2e__0x2e__0x2e_0705_bit0 -x_0x2e__0x2e__0x2e_0705_bit1 -x_0x2e__0x2e__0x2e_0705_bit2 -x_0x2e__0x2e__0x2e_0805_bit0 -x_0x2e__0x2e__0x2e_0805_bit1 -x_0x2e__0x2e__0x2e_0805_bit2 -x_0x2e__0x2e__0x2e_0905_bit0 -x_0x2e__0x2e__0x2e_0905_bit1 -x_0x2e__0x2e__0x2e_0905_bit2 -x_0x2e__0x2e__0x2e_1005_bit0 -x_0x2e__0x2e__0x2e_1005_bit1 -x_0x2e__0x2e__0x2e_1005_bit2 x_0x2e__0x2e__0x2e_1105_bit0 -x_0x2e__0x2e__0x2e_1105_bit1 -x_0x2e__0x2e__0x2e_1105_bit2 x_0x2e__0x2e__0x2e_1205_bit0 -x_0x2e__0x2e__0x2e_1205_bit1 -x_0x2e__0x2e__0x2e_1205_bit2 -x_0x2e__0x2e__0x2e_0106_bit0 -x_0x2e__0x2e__0x2e_0106_bit1 -x_0x2e__0x2e__0x2e_0106_bit2 -x_0x2e__0x2e__0x2e_0106_bit3 -x_0x2e__0x2e__0x2e_0206_bit0 -x_0x2e__0x2e__0x2e_0206_bit1 -x_0x2e__0x2e__0x2e_0206_bit2 -x_0x2e__0x2e__0x2e_0206_bit3 -x_0x2e__0x2e__0x2e_0306_bit0 -x_0x2e__0x2e__0x2e_0306_bit1 x_0x2e__0x2e__0x2e_0306_bit2 -x_0x2e__0x2e__0x2e_0306_bit3 -x_0x2e__0x2e__0x2e_0406_bit0 -x_0x2e__0x2e__0x2e_0406_bit1 -x_0x2e__0x2e__0x2e_0406_bit2 -x_0x2e__0x2e__0x2e_0406_bit3 -x_0x2e__0x2e__0x2e_0506_bit0 -x_0x2e__0x2e__0x2e_0506_bit1 -x_0x2e__0x2e__0x2e_0506_bit2 -x_0x2e__0x2e__0x2e_0506_bit3 -x_0x2e__0x2e__0x2e_0606_bit0 -x_0x2e__0x2e__0x2e_0606_bit1 -x_0x2e__0x2e__0x2e_0606_bit2 -x_0x2e__0x2e__0x2e_0606_bit3 -x_0x2e__0x2e__0x2e_0706_bit0 -x_0x2e__0x2e__0x2e_0706_bit1 -x_0x2e__0x2e__0x2e_0706_bit2 -x_0x2e__0x2e__0x2e_0706_bit3 -x_0x2e__0x2e__0x2e_0806_bit0 -x_0x2e__0x2e__0x2e_0806_bit1 -x_0x2e__0x2e__0x2e_0806_bit2 -x_0x2e__0x2e__0x2e_0806_bit3 -x_0x2e__0x2e__0x2e_0906_bit0 -x_0x2e__0x2e__0x2e_0906_bit1 x_0x2e__0x2e__0x2e_0906_bit2 -x_0x2e__0x2e__0x2e_0906_bit3 -x_0x2e__0x2e__0x2e_1006_bit0 -x_0x2e__0x2e__0x2e_1006_bit1 -x_0x2e__0x2e__0x2e_1006_bit2 -x_0x2e__0x2e__0x2e_1006_bit3 -x_0x2e__0x2e__0x2e_1106_bit0 -x_0x2e__0x2e__0x2e_1106_bit1 -x_0x2e__0x2e__0x2e_1106_bit2 -x_0x2e__0x2e__0x2e_1106_bit3 -x_0x2e__0x2e__0x2e_1206_bit0 -x_0x2e__0x2e__0x2e_1206_bit1 -x_0x2e__0x2e__0x2e_1206_bit2 -x_0x2e__0x2e__0x2e_1206_bit3 x_0x2e__0x2e__0x2e_0507_bit0 -x_0x2e__0x2e__0x2e_0507_bit1 -x_0x2e__0x2e__0x2e_0507_bit2 x_0x2e__0x2e__0x2e_0607_bit0 -x_0x2e__0x2e__0x2e_0607_bit1 -x_0x2e__0x2e__0x2e_0607_bit2 x_0x2e__0x2e__0x2e_1107_bit0 -x_0x2e__0x2e__0x2e_1107_bit1 -x_0x2e__0x2e__0x2e_1107_bit2 x_0x2e__0x2e__0x2e_1207_bit0 -x_0x2e__0x2e__0x2e_1207_bit1 -x_0x2e__0x2e__0x2e_1207_bit2 -x_0x2e__0x2e__0x2e_0108_bit0 -x_0x2e__0x2e__0x2e_0108_bit1 -x_0x2e__0x2e__0x2e_0108_bit2 -x_0x2e__0x2e__0x2e_0108_bit3 -x_0x2e__0x2e__0x2e_0208_bit0 -x_0x2e__0x2e__0x2e_0208_bit1 -x_0x2e__0x2e__0x2e_0208_bit2 -x_0x2e__0x2e__0x2e_0208_bit3 -x_0x2e__0x2e__0x2e_0308_bit0 x_0x2e__0x2e__0x2e_0308_bit1 -x_0x2e__0x2e__0x2e_0308_bit2 x_0x2e__0x2e__0x2e_0308_bit3 -x_0x2e__0x2e__0x2e_0408_bit0 -x_0x2e__0x2e__0x2e_0408_bit1 -x_0x2e__0x2e__0x2e_0408_bit2 -x_0x2e__0x2e__0x2e_0408_bit3 -x_0x2e__0x2e__0x2e_0708_bit0 -x_0x2e__0x2e__0x2e_0708_bit1 -x_0x2e__0x2e__0x2e_0708_bit2 -x_0x2e__0x2e__0x2e_0708_bit3 -x_0x2e__0x2e__0x2e_0808_bit0 -x_0x2e__0x2e__0x2e_0808_bit1 -x_0x2e__0x2e__0x2e_0808_bit2 -x_0x2e__0x2e__0x2e_0808_bit3 -x_0x2e__0x2e__0x2e_0908_bit0 x_0x2e__0x2e__0x2e_0908_bit1 -x_0x2e__0x2e__0x2e_0908_bit2 -x_0x2e__0x2e__0x2e_0908_bit3 -x_0x2e__0x2e__0x2e_1008_bit0 -x_0x2e__0x2e__0x2e_1008_bit1 -x_0x2e__0x2e__0x2e_1008_bit2 -x_0x2e__0x2e__0x2e_1008_bit3 -x_0x2e__0x2e__0x2e_0109_bit0 -x_0x2e__0x2e__0x2e_0109_bit1 -x_0x2e__0x2e__0x2e_0109_bit2 -x_0x2e__0x2e__0x2e_0209_bit0 -x_0x2e__0x2e__0x2e_0209_bit1 -x_0x2e__0x2e__0x2e_0209_bit2 -x_0x2e__0x2e__0x2e_0309_bit0 -x_0x2e__0x2e__0x2e_0309_bit1 -x_0x2e__0x2e__0x2e_0309_bit2 -x_0x2e__0x2e__0x2e_0409_bit0 -x_0x2e__0x2e__0x2e_0409_bit1 -x_0x2e__0x2e__0x2e_0409_bit2 -x_0x2e__0x2e__0x2e_0509_bit0 -x_0x2e__0x2e__0x2e_0509_bit1 -x_0x2e__0x2e__0x2e_0509_bit2 x_0x2e__0x2e__0x2e_0609_bit0 x_0x2e__0x2e__0x2e_0609_bit1 -x_0x2e__0x2e__0x2e_0609_bit2 -x_0x2e__0x2e__0x2e_0709_bit0 -x_0x2e__0x2e__0x2e_0709_bit1 -x_0x2e__0x2e__0x2e_0709_bit2 x_0x2e__0x2e__0x2e_0809_bit0 -x_0x2e__0x2e__0x2e_0809_bit1 -x_0x2e__0x2e__0x2e_0809_bit2 -x_0x2e__0x2e__0x2e_0909_bit0 -x_0x2e__0x2e__0x2e_0909_bit1 -x_0x2e__0x2e__0x2e_0909_bit2 x_0x2e__0x2e__0x2e_1009_bit0 -x_0x2e__0x2e__0x2e_1009_bit1 -x_0x2e__0x2e__0x2e_1009_bit2 -x_0x2e__0x2e__0x2e_1109_bit0 -x_0x2e__0x2e__0x2e_1109_bit1 -x_0x2e__0x2e__0x2e_1109_bit2 -x_0x2e__0x2e__0x2e_1209_bit0 -x_0x2e__0x2e__0x2e_1209_bit1 -x_0x2e__0x2e__0x2e_1209_bit2 -x_0x2e__0x2e__0x2e_0110_bit0 -x_0x2e__0x2e__0x2e_0110_bit1 x_0x2e__0x2e__0x2e_0110_bit2 -x_0x2e__0x2e__0x2e_0111_bit0 -x_0x2e__0x2e__0x2e_0111_bit1 -x_0x2e__0x2e__0x2e_0111_bit2 -x_0x2e__0x2e__0x2e_0112_bit0 -x_0x2e__0x2e__0x2e_0112_bit1 -x_0x2e__0x2e__0x2e_0112_bit2 -x_0x2e__0x2e__0x2e_0112_bit3 x_0x2e__0x2e__0x2e_0113_bit0 -x_0x2e__0x2e__0x2e_0113_bit1 -x_0x2e__0x2e__0x2e_0113_bit2 -x_0x2e__0x2e__0x2e_0114_bit0 -x_0x2e__0x2e__0x2e_0114_bit1 -x_0x2e__0x2e__0x2e_0114_bit2 -x_0x2e__0x2e__0x2e_0115_bit0 x_0x2e__0x2e__0x2e_0115_bit1 x_0x2e__0x2e__0x2e_0116_bit0 -x_0x2e__0x2e__0x2e_0116_bit1 -x_0x2e__0x2e__0x2e_0117_bit0 -x_0x2e__0x2e__0x2e_0210_bit0 -x_0x2e__0x2e__0x2e_0210_bit1 -x_0x2e__0x2e__0x2e_0210_bit2 -x_0x2e__0x2e__0x2e_0211_bit0 -x_0x2e__0x2e__0x2e_0211_bit1 -x_0x2e__0x2e__0x2e_0211_bit2 -x_0x2e__0x2e__0x2e_0212_bit0 -x_0x2e__0x2e__0x2e_0212_bit1 -x_0x2e__0x2e__0x2e_0212_bit2 -x_0x2e__0x2e__0x2e_0212_bit3 -x_0x2e__0x2e__0x2e_0213_bit0 -x_0x2e__0x2e__0x2e_0213_bit1 -x_0x2e__0x2e__0x2e_0213_bit2 -x_0x2e__0x2e__0x2e_0214_bit0 -x_0x2e__0x2e__0x2e_0214_bit1 -x_0x2e__0x2e__0x2e_0214_bit2 -x_0x2e__0x2e__0x2e_0215_bit0 -x_0x2e__0x2e__0x2e_0215_bit1 -x_0x2e__0x2e__0x2e_0216_bit0 -x_0x2e__0x2e__0x2e_0216_bit1 -x_0x2e__0x2e__0x2e_0217_bit0 -x_0x2e__0x2e__0x2e_0310_bit0 -x_0x2e__0x2e__0x2e_0310_bit1 -x_0x2e__0x2e__0x2e_0310_bit2 -x_0x2e__0x2e__0x2e_0311_bit0 -x_0x2e__0x2e__0x2e_0311_bit1 -x_0x2e__0x2e__0x2e_0311_bit2 -x_0x2e__0x2e__0x2e_0312_bit0 -x_0x2e__0x2e__0x2e_0312_bit1 -x_0x2e__0x2e__0x2e_0312_bit2 -x_0x2e__0x2e__0x2e_0312_bit3 -x_0x2e__0x2e__0x2e_0313_bit0 -x_0x2e__0x2e__0x2e_0313_bit1 -x_0x2e__0x2e__0x2e_0313_bit2 -x_0x2e__0x2e__0x2e_0314_bit0 -x_0x2e__0x2e__0x2e_0314_bit1 -x_0x2e__0x2e__0x2e_0314_bit2 -x_0x2e__0x2e__0x2e_0315_bit0 -x_0x2e__0x2e__0x2e_0315_bit1 -x_0x2e__0x2e__0x2e_0316_bit0 -x_0x2e__0x2e__0x2e_0316_bit1 -x_0x2e__0x2e__0x2e_0317_bit0 -x_0x2e__0x2e__0x2e_0410_bit0 -x_0x2e__0x2e__0x2e_0410_bit1 -x_0x2e__0x2e__0x2e_0410_bit2 -x_0x2e__0x2e__0x2e_0411_bit0 -x_0x2e__0x2e__0x2e_0411_bit1 -x_0x2e__0x2e__0x2e_0411_bit2 -x_0x2e__0x2e__0x2e_0412_bit0 -x_0x2e__0x2e__0x2e_0412_bit1 -x_0x2e__0x2e__0x2e_0412_bit2 x_0x2e__0x2e__0x2e_0412_bit3 -x_0x2e__0x2e__0x2e_0413_bit0 -x_0x2e__0x2e__0x2e_0413_bit1 -x_0x2e__0x2e__0x2e_0413_bit2 -x_0x2e__0x2e__0x2e_0414_bit0 -x_0x2e__0x2e__0x2e_0414_bit1 -x_0x2e__0x2e__0x2e_0414_bit2 -x_0x2e__0x2e__0x2e_0415_bit0 -x_0x2e__0x2e__0x2e_0415_bit1 -x_0x2e__0x2e__0x2e_0416_bit0 -x_0x2e__0x2e__0x2e_0416_bit1 -x_0x2e__0x2e__0x2e_0417_bit0 -x_0x2e__0x2e__0x2e_0510_bit0 -x_0x2e__0x2e__0x2e_0510_bit1 -x_0x2e__0x2e__0x2e_0510_bit2 -x_0x2e__0x2e__0x2e_0511_bit0 -x_0x2e__0x2e__0x2e_0511_bit1 -x_0x2e__0x2e__0x2e_0511_bit2 -x_0x2e__0x2e__0x2e_0512_bit0 -x_0x2e__0x2e__0x2e_0512_bit1 -x_0x2e__0x2e__0x2e_0512_bit2 -x_0x2e__0x2e__0x2e_0512_bit3 -x_0x2e__0x2e__0x2e_0513_bit0 -x_0x2e__0x2e__0x2e_0513_bit1 -x_0x2e__0x2e__0x2e_0513_bit2 -x_0x2e__0x2e__0x2e_0514_bit0 -x_0x2e__0x2e__0x2e_0514_bit1 -x_0x2e__0x2e__0x2e_0514_bit2 -x_0x2e__0x2e__0x2e_0515_bit0 -x_0x2e__0x2e__0x2e_0515_bit1 -x_0x2e__0x2e__0x2e_0516_bit0 -x_0x2e__0x2e__0x2e_0516_bit1 -x_0x2e__0x2e__0x2e_0517_bit0 -x_0x2e__0x2e__0x2e_0610_bit0 -x_0x2e__0x2e__0x2e_0610_bit1 -x_0x2e__0x2e__0x2e_0610_bit2 -x_0x2e__0x2e__0x2e_0611_bit0 -x_0x2e__0x2e__0x2e_0611_bit1 -x_0x2e__0x2e__0x2e_0611_bit2 -x_0x2e__0x2e__0x2e_0612_bit0 -x_0x2e__0x2e__0x2e_0612_bit1 -x_0x2e__0x2e__0x2e_0612_bit2 -x_0x2e__0x2e__0x2e_0612_bit3 -x_0x2e__0x2e__0x2e_0613_bit0 -x_0x2e__0x2e__0x2e_0613_bit1 -x_0x2e__0x2e__0x2e_0613_bit2 -x_0x2e__0x2e__0x2e_0614_bit0 -x_0x2e__0x2e__0x2e_0614_bit1 -x_0x2e__0x2e__0x2e_0614_bit2 -x_0x2e__0x2e__0x2e_0615_bit0 -x_0x2e__0x2e__0x2e_0615_bit1 -x_0x2e__0x2e__0x2e_0616_bit0 -x_0x2e__0x2e__0x2e_0616_bit1 -x_0x2e__0x2e__0x2e_0617_bit0 -x_0x2e__0x2e__0x2e_0710_bit0 -x_0x2e__0x2e__0x2e_0710_bit1 -x_0x2e__0x2e__0x2e_0710_bit2 -x_0x2e__0x2e__0x2e_0711_bit0 -x_0x2e__0x2e__0x2e_0711_bit1 -x_0x2e__0x2e__0x2e_0711_bit2 -x_0x2e__0x2e__0x2e_0712_bit0 -x_0x2e__0x2e__0x2e_0712_bit1 -x_0x2e__0x2e__0x2e_0712_bit2 -x_0x2e__0x2e__0x2e_0712_bit3 x_0x2e__0x2e__0x2e_0713_bit0 -x_0x2e__0x2e__0x2e_0713_bit1 -x_0x2e__0x2e__0x2e_0713_bit2 -x_0x2e__0x2e__0x2e_0714_bit0 x_0x2e__0x2e__0x2e_0714_bit1 -x_0x2e__0x2e__0x2e_0714_bit2 -x_0x2e__0x2e__0x2e_0715_bit0 -x_0x2e__0x2e__0x2e_0715_bit1 -x_0x2e__0x2e__0x2e_0716_bit0 -x_0x2e__0x2e__0x2e_0716_bit1 -x_0x2e__0x2e__0x2e_0717_bit0 -x_0x2e__0x2e__0x2e_0810_bit0 -x_0x2e__0x2e__0x2e_0810_bit1 -x_0x2e__0x2e__0x2e_0810_bit2 -x_0x2e__0x2e__0x2e_0811_bit0 -x_0x2e__0x2e__0x2e_0811_bit1 -x_0x2e__0x2e__0x2e_0811_bit2 -x_0x2e__0x2e__0x2e_0812_bit0 -x_0x2e__0x2e__0x2e_0812_bit1 -x_0x2e__0x2e__0x2e_0812_bit2 -x_0x2e__0x2e__0x2e_0812_bit3 -x_0x2e__0x2e__0x2e_0813_bit0 -x_0x2e__0x2e__0x2e_0813_bit1 -x_0x2e__0x2e__0x2e_0813_bit2 -x_0x2e__0x2e__0x2e_0814_bit0 -x_0x2e__0x2e__0x2e_0814_bit1 -x_0x2e__0x2e__0x2e_0814_bit2 -x_0x2e__0x2e__0x2e_0815_bit0 -x_0x2e__0x2e__0x2e_0815_bit1 -x_0x2e__0x2e__0x2e_0816_bit0 -x_0x2e__0x2e__0x2e_0816_bit1 -x_0x2e__0x2e__0x2e_0817_bit0 x_0x2e__0x2e__0x2e_0910_bit0 -x_0x2e__0x2e__0x2e_0910_bit1 -x_0x2e__0x2e__0x2e_0910_bit2 -x_0x2e__0x2e__0x2e_0911_bit0 -x_0x2e__0x2e__0x2e_0911_bit1 x_0x2e__0x2e__0x2e_0911_bit2 -x_0x2e__0x2e__0x2e_0912_bit0 -x_0x2e__0x2e__0x2e_0912_bit1 -x_0x2e__0x2e__0x2e_0912_bit2 -x_0x2e__0x2e__0x2e_0912_bit3 x_0x2e__0x2e__0x2e_0913_bit0 -x_0x2e__0x2e__0x2e_0913_bit1 -x_0x2e__0x2e__0x2e_0913_bit2 x_0x2e__0x2e__0x2e_0914_bit0 -x_0x2e__0x2e__0x2e_0914_bit1 -x_0x2e__0x2e__0x2e_0914_bit2 -x_0x2e__0x2e__0x2e_0915_bit0 -x_0x2e__0x2e__0x2e_0915_bit1 -x_0x2e__0x2e__0x2e_0916_bit0 -x_0x2e__0x2e__0x2e_0916_bit1 -x_0x2e__0x2e__0x2e_0917_bit0 -x_0x2e__0x2e__0x2e_1010_bit0 -x_0x2e__0x2e__0x2e_1010_bit1 -x_0x2e__0x2e__0x2e_1010_bit2 -x_0x2e__0x2e__0x2e_1011_bit0 -x_0x2e__0x2e__0x2e_1011_bit1 -x_0x2e__0x2e__0x2e_1011_bit2 -x_0x2e__0x2e__0x2e_1012_bit0 -x_0x2e__0x2e__0x2e_1012_bit1 -x_0x2e__0x2e__0x2e_1012_bit2 -x_0x2e__0x2e__0x2e_1012_bit3 -x_0x2e__0x2e__0x2e_1013_bit0 -x_0x2e__0x2e__0x2e_1013_bit1 -x_0x2e__0x2e__0x2e_1013_bit2 -x_0x2e__0x2e__0x2e_1014_bit0 -x_0x2e__0x2e__0x2e_1014_bit1 -x_0x2e__0x2e__0x2e_1014_bit2 -x_0x2e__0x2e__0x2e_1015_bit0 -x_0x2e__0x2e__0x2e_1015_bit1 -x_0x2e__0x2e__0x2e_1016_bit0 -x_0x2e__0x2e__0x2e_1016_bit1 -x_0x2e__0x2e__0x2e_1017_bit0 x_0x2e__0x2e__0x2e_1110_bit0 -x_0x2e__0x2e__0x2e_1110_bit1 -x_0x2e__0x2e__0x2e_1110_bit2 -x_0x2e__0x2e__0x2e_1111_bit0 -x_0x2e__0x2e__0x2e_1111_bit1 -x_0x2e__0x2e__0x2e_1111_bit2 x_0x2e__0x2e__0x2e_1112_bit0 -x_0x2e__0x2e__0x2e_1112_bit1 -x_0x2e__0x2e__0x2e_1112_bit2 -x_0x2e__0x2e__0x2e_1112_bit3 x_0x2e__0x2e__0x2e_1113_bit0 -x_0x2e__0x2e__0x2e_1113_bit1 -x_0x2e__0x2e__0x2e_1113_bit2 -x_0x2e__0x2e__0x2e_1114_bit0 -x_0x2e__0x2e__0x2e_1114_bit1 -x_0x2e__0x2e__0x2e_1114_bit2 -x_0x2e__0x2e__0x2e_1115_bit0 -x_0x2e__0x2e__0x2e_1115_bit1 -x_0x2e__0x2e__0x2e_1116_bit0 -x_0x2e__0x2e__0x2e_1116_bit1 x_0x2e__0x2e__0x2e_1117_bit0 -x_0x2e__0x2e__0x2e_1210_bit0 -x_0x2e__0x2e__0x2e_1210_bit1 -x_0x2e__0x2e__0x2e_1210_bit2 -x_0x2e__0x2e__0x2e_1211_bit0 -x_0x2e__0x2e__0x2e_1211_bit1 -x_0x2e__0x2e__0x2e_1211_bit2 -x_0x2e__0x2e__0x2e_1212_bit0 -x_0x2e__0x2e__0x2e_1212_bit1 -x_0x2e__0x2e__0x2e_1212_bit2 -x_0x2e__0x2e__0x2e_1212_bit3 -x_0x2e__0x2e__0x2e_1213_bit0 -x_0x2e__0x2#### 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.85 0.97 0.93 2/54 9755
Raw data (stat): 9755 (runsolver) R 9754 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487401787 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 8949 0 0 0 976 22 0 0 25 0 1 0 487401787 39116800 8315 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9550 8315 603 41 0 9509 0
vsize: 38200
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 9061 0 0 0 1975 23 0 0 25 0 1 0 487401787 39624704 8427 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9674 8427 603 41 0 9633 0
vsize: 38696
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 9122 0 0 0 2974 23 0 0 25 0 1 0 487401787 39895040 8488 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9740 8488 603 41 0 9699 0
vsize: 38960
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 9312 0 0 0 3974 24 0 0 25 0 1 0 487401787 40718336 8678 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9941 8678 603 41 0 9900 0
vsize: 39764
[startup+50.0022 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 9489 0 0 0 4974 24 0 0 25 0 1 0 487401787 41390080 8855 4294967295 134512640 134672761 3221224624 3221223808 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 8855 603 41 0 10064 0
vsize: 40420
[startup+60.0021 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 9619 0 0 0 5973 25 0 0 25 0 1 0 487401787 41930752 8985 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10237 8985 603 41 0 10196 0
vsize: 40948
[startup+70.0032 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 9926 0 0 0 6973 25 0 0 25 0 1 0 487401787 43134976 9292 4294967295 134512640 134672761 3221224624 3221223808 134559540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10531 9292 603 41 0 10490 0
vsize: 42124
[startup+80.0042 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 10130 0 0 0 7972 26 0 0 25 0 1 0 487401787 44036096 9496 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10751 9496 603 41 0 10710 0
vsize: 43004
[startup+90.0039 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 10282 0 0 0 8972 27 0 0 25 0 1 0 487401787 44695552 9648 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10912 9648 603 41 0 10871 0
vsize: 43648
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 10431 0 0 0 9971 27 0 0 25 0 1 0 487401787 45228032 9797 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11042 9797 603 41 0 11001 0
vsize: 44168
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 9755
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 10561 0 0 0 10970 28 0 0 25 0 1 0 487401787 45760512 9927 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11172 9927 603 41 0 11131 0
vsize: 44688
[startup+120.009 s]
Raw data (loadavg): 0.98 0.97 0.93 3/57 9790
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 10854 0 0 0 11970 29 0 0 25 0 1 0 487401787 46968832 10220 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11467 10220 603 41 0 11426 0
vsize: 45868
[startup+130.008 s]
Raw data (loadavg): 1.35 1.05 0.95 2/54 9808
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 10921 0 0 0 12967 32 0 0 25 0 1 0 487401787 47239168 10287 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11533 10287 603 41 0 11492 0
vsize: 46132
[startup+140.008 s]
Raw data (loadavg): 1.29 1.05 0.95 2/54 9808
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 11110 0 0 0 13966 33 0 0 25 0 1 0 487401787 48041984 10476 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11729 10476 603 41 0 11688 0
vsize: 46916
[startup+150.008 s]
Raw data (loadavg): 1.25 1.05 0.95 2/54 9808
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 11403 0 0 0 14965 34 0 0 25 0 1 0 487401787 49250304 10769 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12024 10769 603 41 0 11983 0
vsize: 48096
[startup+160.008 s]
Raw data (loadavg): 1.21 1.05 0.95 2/54 9808
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 11654 0 0 0 15964 36 0 0 25 0 1 0 487401787 50319360 11020 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12285 11020 603 41 0 12244 0
vsize: 49140
[startup+170.009 s]
Raw data (loadavg): 1.18 1.04 0.95 2/54 9808
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 11939 0 0 0 16962 38 0 0 25 0 1 0 487401787 51548160 11305 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11305 603 41 0 12544 0
vsize: 50340
[startup+180.009 s]
Raw data (loadavg): 1.15 1.04 0.95 2/54 9808
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 12164 0 0 0 17962 39 0 0 25 0 1 0 487401787 52322304 11530 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12774 11530 603 41 0 12733 0
vsize: 51096
[startup+190.01 s]
Raw data (loadavg): 1.13 1.04 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 12350 0 0 0 18961 40 0 0 25 0 1 0 487401787 53256192 11716 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13002 11716 603 41 0 12961 0
vsize: 52008
[startup+200.01 s]
Raw data (loadavg): 1.11 1.04 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 12445 0 0 0 19960 40 0 0 25 0 1 0 487401787 53653504 11811 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13099 11811 603 41 0 13058 0
vsize: 52396
[startup+210.009 s]
Raw data (loadavg): 1.09 1.04 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 12538 0 0 0 20960 41 0 0 25 0 1 0 487401787 53919744 11904 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13164 11904 603 41 0 13123 0
vsize: 52656
[startup+220.018 s]
Raw data (loadavg): 1.08 1.04 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 12668 0 0 0 21960 42 0 0 25 0 1 0 487401787 54452224 12034 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13294 12034 603 41 0 13253 0
vsize: 53176
[startup+230.033 s]
Raw data (loadavg): 1.06 1.03 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 12812 0 0 0 22961 42 0 0 25 0 1 0 487401787 55123968 12178 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13458 12178 603 41 0 13417 0
vsize: 53832
[startup+240.032 s]
Raw data (loadavg): 1.05 1.03 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 12949 0 0 0 23960 43 0 0 25 0 1 0 487401787 55660544 12315 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13589 12315 603 41 0 13548 0
vsize: 54356
[startup+250.032 s]
Raw data (loadavg): 1.04 1.03 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 13118 0 0 0 24960 44 0 0 25 0 1 0 487401787 56352768 12484 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13758 12484 603 41 0 13717 0
vsize: 55032
[startup+260.033 s]
Raw data (loadavg): 1.04 1.03 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 13307 0 0 0 25959 45 0 0 25 0 1 0 487401787 57143296 12673 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13951 12673 603 41 0 13910 0
vsize: 55804
[startup+270.033 s]
Raw data (loadavg): 1.03 1.03 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 19141 0 0 0 26944 60 0 0 25 0 1 0 487401787 83886080 17887 4294967295 134512640 134672761 3221224624 3221223624 1075349878 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20480 17887 603 41 0 20439 0
vsize: 81920
[startup+280.033 s]
Raw data (loadavg): 1.03 1.03 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 19232 0 0 0 27944 60 0 0 25 0 1 0 487401787 84021248 17978 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20513 17978 603 41 0 20472 0
vsize: 82052
[startup+290.033 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 19391 0 0 0 28943 61 0 0 25 0 1 0 487401787 84692992 18137 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20677 18137 603 41 0 20636 0
vsize: 82708
[startup+300.033 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 19524 0 0 0 29943 62 0 0 25 0 1 0 487401787 85241856 18270 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20811 18270 603 41 0 20770 0
vsize: 83244
[startup+310.033 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 19589 0 0 0 30942 62 0 0 25 0 1 0 487401787 85504000 18335 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20875 18335 603 41 0 20834 0
vsize: 83500
[startup+320.034 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 19653 0 0 0 31942 63 0 0 25 0 1 0 487401787 85639168 18399 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20908 18399 603 41 0 20867 0
vsize: 83632
[startup+330.034 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 19946 0 0 0 32940 65 0 0 25 0 1 0 487401787 87113728 18692 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21268 18692 603 41 0 21227 0
vsize: 85072
[startup+340.034 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 20156 0 0 0 33939 66 0 0 25 0 1 0 487401787 88047616 18902 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21496 18902 603 41 0 21455 0
vsize: 85984
[startup+350.035 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 20169 0 0 0 34939 67 0 0 25 0 1 0 487401787 88047616 18915 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21496 18915 603 41 0 21455 0
vsize: 85984
[startup+360.035 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 20245 0 0 0 35939 67 0 0 25 0 1 0 487401787 88317952 18991 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21562 18991 603 41 0 21521 0
vsize: 86248
[startup+370.035 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 20259 0 0 0 36939 67 0 0 25 0 1 0 487401787 88453120 19005 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21595 19005 603 41 0 21554 0
vsize: 86380
[startup+380.036 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 25275 0 0 0 37928 78 0 0 25 0 1 0 487401787 103784448 23731 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25338 23731 603 41 0 25297 0
vsize: 101352
[startup+390.035 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 25313 0 0 0 38928 78 0 0 25 0 1 0 487401787 103927808 23769 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25373 23769 603 41 0 25332 0
vsize: 101492
[startup+400.035 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 25383 0 0 0 39928 79 0 0 25 0 1 0 487401787 104198144 23839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25439 23839 603 41 0 25398 0
vsize: 101756
[startup+410.036 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 25426 0 0 0 40928 79 0 0 25 0 1 0 487401787 104333312 23882 4294967295 134512640 134672761 3221224624 3221223792 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25472 23882 603 41 0 25431 0
vsize: 101888
[startup+420.036 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26105 0 0 0 41926 81 0 0 25 0 1 0 487401787 106266624 24271 4294967295 134512640 134672761 3221224624 3221223924 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25944 24271 603 41 0 25903 0
vsize: 103776
[startup+430.036 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26106 0 0 0 42926 81 0 0 25 0 1 0 487401787 106266624 24272 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25944 24272 603 41 0 25903 0
vsize: 103776
[startup+440.037 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26109 0 0 0 43925 81 0 0 25 0 1 0 487401787 106266624 24275 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25944 24275 603 41 0 25903 0
vsize: 103776
[startup+450.038 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26155 0 0 0 44925 82 0 0 25 0 1 0 487401787 106409984 24321 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25979 24321 603 41 0 25938 0
vsize: 103916
[startup+460.037 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26242 0 0 0 45924 83 0 0 25 0 1 0 487401787 106807296 24408 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26076 24408 603 41 0 26035 0
vsize: 104304
[startup+470.037 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26305 0 0 0 46924 83 0 0 25 0 1 0 487401787 107065344 24471 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26139 24471 603 41 0 26098 0
vsize: 104556
[startup+480.038 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26358 0 0 0 47924 83 0 0 25 0 1 0 487401787 107200512 24524 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26172 24524 603 41 0 26131 0
vsize: 104688
[startup+490.038 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9810
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26412 0 0 0 48924 84 0 0 25 0 1 0 487401787 107474944 24578 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26239 24578 603 41 0 26198 0
vsize: 104956
[startup+500.038 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26452 0 0 0 49923 84 0 0 25 0 1 0 487401787 107610112 24618 4294967295 134512640 134672761 3221224624 3221223840 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26272 24618 603 41 0 26231 0
vsize: 105088
[startup+510.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26467 0 0 0 50923 85 0 0 25 0 1 0 487401787 107745280 24633 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26305 24633 603 41 0 26264 0
vsize: 105220
[startup+520.038 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 26613 0 0 0 51923 85 0 0 25 0 1 0 487401787 108273664 24779 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26434 24779 603 41 0 26393 0
vsize: 105736
[startup+530.038 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 27319 0 0 0 52921 87 0 0 25 0 1 0 487401787 110010368 25195 4294967295 134512640 134672761 3221224624 3221222896 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26858 25195 603 41 0 26817 0
vsize: 107432
[startup+540.038 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 31711 0 0 0 53910 98 0 0 25 0 1 0 487401787 142872576 29587 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34881 29587 603 41 0 34840 0
vsize: 139524
[startup+550.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 31831 0 0 0 54909 99 0 0 25 0 1 0 487401787 143413248 29707 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35013 29707 603 41 0 34972 0
vsize: 140052
[startup+560.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 31897 0 0 0 55909 100 0 0 25 0 1 0 487401787 143679488 29773 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35078 29773 603 41 0 35037 0
vsize: 140312
[startup+570.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 31950 0 0 0 56908 100 0 0 25 0 1 0 487401787 143814656 29826 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35111 29826 603 41 0 35070 0
vsize: 140444
[startup+580.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 32042 0 0 0 57908 101 0 0 25 0 1 0 487401787 144216064 29918 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35209 29918 603 41 0 35168 0
vsize: 140836
[startup+590.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 32061 0 0 0 58908 101 0 0 25 0 1 0 487401787 144351232 29937 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35242 29937 603 41 0 35201 0
vsize: 140968
[startup+600.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 32257 0 0 0 59907 102 0 0 25 0 1 0 487401787 145145856 30133 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35436 30133 603 41 0 35395 0
vsize: 141744
[startup+610.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 32322 0 0 0 60907 102 0 0 25 0 1 0 487401787 145408000 30198 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35500 30198 603 41 0 35459 0
vsize: 142000
[startup+620.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 32382 0 0 0 61907 102 0 0 25 0 1 0 487401787 145674240 30258 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35565 30258 603 41 0 35524 0
vsize: 142260
[startup+630.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 32462 0 0 0 62907 102 0 0 25 0 1 0 487401787 145944576 30338 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35631 30338 603 41 0 35590 0
vsize: 142524
[startup+640.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 32544 0 0 0 63907 103 0 0 25 0 1 0 487401787 146210816 30420 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35696 30420 603 41 0 35655 0
vsize: 142784
[startup+650.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 32622 0 0 0 64907 103 0 0 25 0 1 0 487401787 146616320 30498 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35795 30498 603 41 0 35754 0
vsize: 143180
[startup+660.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 32720 0 0 0 65907 103 0 0 25 0 1 0 487401787 147017728 30596 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35893 30596 603 41 0 35852 0
vsize: 143572
[startup+670.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33195 0 0 0 66906 105 0 0 25 0 1 0 487401787 148889600 31071 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36350 31071 603 41 0 36309 0
vsize: 145400
[startup+680.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33911 0 0 0 67904 106 0 0 25 0 1 0 487401787 150339584 31497 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36704 31497 603 41 0 36663 0
vsize: 146816
[startup+690.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33911 0 0 0 68904 106 0 0 25 0 1 0 487401787 150339584 31497 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36704 31497 603 41 0 36663 0
vsize: 146816
[startup+700.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33912 0 0 0 69905 106 0 0 25 0 1 0 487401787 150339584 31498 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36704 31498 603 41 0 36663 0
vsize: 146816
[startup+710.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33912 0 0 0 70905 106 0 0 25 0 1 0 487401787 150339584 31498 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36704 31498 603 41 0 36663 0
vsize: 146816
[startup+720.038 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33912 0 0 0 71905 106 0 0 25 0 1 0 487401787 150339584 31498 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36704 31498 603 41 0 36663 0
vsize: 146816
[startup+730.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33912 0 0 0 72905 106 0 0 25 0 1 0 487401787 150339584 31498 4294967295 134512640 134672761 3221224624 3221223796 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36704 31498 603 41 0 36663 0
vsize: 146816
[startup+740.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33913 0 0 0 73905 106 0 0 25 0 1 0 487401787 150339584 31499 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36704 31499 603 41 0 36663 0
vsize: 146816
[startup+750.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33914 0 0 0 74906 106 0 0 25 0 1 0 487401787 150339584 31500 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36704 31500 603 41 0 36663 0
vsize: 146816
[startup+760.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 33925 0 0 0 75906 106 0 0 25 0 1 0 487401787 150339584 31511 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36704 31511 603 41 0 36663 0
vsize: 146816
[startup+770.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34014 0 0 0 76895 106 0 0 25 0 1 0 487401787 150781952 31600 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36812 31600 603 41 0 36771 0
vsize: 147248
[startup+780.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34020 0 0 0 77895 106 0 0 25 0 1 0 487401787 150781952 31606 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36812 31606 603 41 0 36771 0
vsize: 147248
[startup+790.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34328 0 0 0 78895 107 0 0 25 0 1 0 487401787 151986176 31914 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37106 31914 603 41 0 37065 0
vsize: 148424
[startup+800.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34469 0 0 0 79894 108 0 0 25 0 1 0 487401787 152645632 32055 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37267 32055 603 41 0 37226 0
vsize: 149068
[startup+810.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34524 0 0 0 80894 108 0 0 25 0 1 0 487401787 152776704 32110 4294967295 134512640 134672761 3221224624 3221223728 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37299 32110 603 41 0 37258 0
vsize: 149196
[startup+820.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34606 0 0 0 81894 108 0 0 25 0 1 0 487401787 153194496 32192 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37401 32192 603 41 0 37360 0
vsize: 149604
[startup+830.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34687 0 0 0 82894 109 0 0 25 0 1 0 487401787 153448448 32273 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37463 32273 603 41 0 37422 0
vsize: 149852
[startup+840.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34765 0 0 0 83894 110 0 0 25 0 1 0 487401787 153849856 32351 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37561 32351 603 41 0 37520 0
vsize: 150244
[startup+850.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34846 0 0 0 84893 110 0 0 25 0 1 0 487401787 154120192 32432 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37627 32432 603 41 0 37586 0
vsize: 150508
[startup+860.042 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 34952 0 0 0 85894 110 0 0 25 0 1 0 487401787 154521600 32538 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37725 32538 603 41 0 37684 0
vsize: 150900
[startup+870.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 35048 0 0 0 86893 110 0 0 25 0 1 0 487401787 154923008 32634 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37823 32634 603 41 0 37782 0
vsize: 151292
[startup+880.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 35134 0 0 0 87893 111 0 0 25 0 1 0 487401787 155324416 32720 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37921 32720 603 41 0 37880 0
vsize: 151684
[startup+890.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 35205 0 0 0 88893 111 0 0 25 0 1 0 487401787 155590656 32791 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37986 32791 603 41 0 37945 0
vsize: 151944
[startup+900.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 35240 0 0 0 89893 111 0 0 25 0 1 0 487401787 155729920 32826 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38020 32826 603 41 0 37979 0
vsize: 152080
[startup+910.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 35285 0 0 0 90893 112 0 0 25 0 1 0 487401787 155865088 32871 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38053 32871 603 41 0 38012 0
vsize: 152212
[startup+920.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 35341 0 0 0 91893 112 0 0 25 0 1 0 487401787 156135424 32927 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38119 32927 603 41 0 38078 0
vsize: 152476
[startup+930.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 35361 0 0 0 92893 112 0 0 25 0 1 0 487401787 156270592 32947 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38152 32947 603 41 0 38111 0
vsize: 152608
[startup+940.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 35556 0 0 0 93893 112 0 0 25 0 1 0 487401787 156942336 33142 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38316 33142 603 41 0 38275 0
vsize: 153264
[startup+950.042 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 35769 0 0 0 94892 113 0 0 25 0 1 0 487401787 157876224 33355 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38544 33355 603 41 0 38503 0
vsize: 154176
[startup+960.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36011 0 0 0 95892 114 0 0 25 0 1 0 487401787 158818304 33597 4294967295 134512640 134672761 3221224624 3221223728 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38774 33597 603 41 0 38733 0
vsize: 155096
[startup+970.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36101 0 0 0 96891 114 0 0 25 0 1 0 487401787 159215616 33687 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38871 33687 603 41 0 38830 0
vsize: 155484
[startup+980.042 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36150 0 0 0 97891 114 0 0 25 0 1 0 487401787 159485952 33736 4294967295 134512640 134672761 3221224624 3221223728 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38937 33736 603 41 0 38896 0
vsize: 155748
[startup+990.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36259 0 0 0 98891 114 0 0 25 0 1 0 487401787 159887360 33845 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39035 33845 603 41 0 38994 0
vsize: 156140
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36387 0 0 0 99891 115 0 0 25 0 1 0 487401787 160428032 33973 4294967295 134512640 134672761 3221224624 3221223728 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39167 33973 603 41 0 39126 0
vsize: 156668
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36441 0 0 0 100891 115 0 0 25 0 1 0 487401787 160559104 34027 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39199 34027 603 41 0 39158 0
vsize: 156796
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36453 0 0 0 101892 115 0 0 25 0 1 0 487401787 160690176 34039 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39231 34039 603 41 0 39190 0
vsize: 156924
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36474 0 0 0 102892 115 0 0 25 0 1 0 487401787 160690176 34060 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39231 34060 603 41 0 39190 0
vsize: 156924
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36504 0 0 0 103892 115 0 0 25 0 1 0 487401787 160821248 34090 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39263 34090 603 41 0 39222 0
vsize: 157052
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36525 0 0 0 104892 115 0 0 25 0 1 0 487401787 160952320 34111 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39295 34111 603 41 0 39254 0
vsize: 157180
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 36576 0 0 0 105892 115 0 0 25 0 1 0 487401787 161087488 34162 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39328 34162 603 41 0 39287 0
vsize: 157312
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37105 0 0 0 106891 116 0 0 25 0 1 0 487401787 161308672 34219 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39382 34219 603 41 0 39341 0
vsize: 157528
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37108 0 0 0 107890 117 0 0 25 0 1 0 487401787 161443840 34222 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39415 34222 603 41 0 39374 0
vsize: 157660
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37120 0 0 0 108890 117 0 0 25 0 1 0 487401787 161443840 34234 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39415 34234 603 41 0 39374 0
vsize: 157660
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37150 0 0 0 109890 117 0 0 25 0 1 0 487401787 161579008 34264 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39448 34264 603 41 0 39407 0
vsize: 157792
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37182 0 0 0 110890 117 0 0 25 0 1 0 487401787 162238464 34296 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39609 34296 603 41 0 39568 0
vsize: 158436
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37744 0 0 0 111888 119 0 0 25 0 1 0 487401787 162480128 34380 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39668 34380 603 41 0 39627 0
vsize: 158672
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37746 0 0 0 112889 119 0 0 25 0 1 0 487401787 162480128 34382 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39668 34382 603 41 0 39627 0
vsize: 158672
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37796 0 0 0 113889 120 0 0 25 0 1 0 487401787 162750464 34432 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39734 34432 603 41 0 39693 0
vsize: 158936
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37830 0 0 0 114889 120 0 0 25 0 1 0 487401787 162881536 34466 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39766 34466 603 41 0 39725 0
vsize: 159064
[startup+1160.05 s]
Raw data (loadavg): 1.07 1.02 0.96 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37899 0 0 0 115888 120 0 0 25 0 1 0 487401787 163160064 34535 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39834 34535 603 41 0 39793 0
vsize: 159336
[startup+1170.04 s]
Raw data (loadavg): 1.06 1.02 0.96 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37918 0 0 0 116889 120 0 0 25 0 1 0 487401787 163295232 34554 4294967295 134512640 134672761 3221224624 3221223760 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39867 34554 603 41 0 39826 0
vsize: 159468
[startup+1180.05 s]
Raw data (loadavg): 1.05 1.01 0.96 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37933 0 0 0 117889 120 0 0 25 0 1 0 487401787 163295232 34569 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39867 34569 603 41 0 39826 0
vsize: 159468
[startup+1190.05 s]
Raw data (loadavg): 1.04 1.01 0.96 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37939 0 0 0 118889 120 0 0 25 0 1 0 487401787 163295232 34575 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39867 34575 603 41 0 39826 0
vsize: 159468
[startup+1200.05 s]
Raw data (loadavg): 1.04 1.01 0.96 2/54 9812
Raw data (stat): 9755 (minisat+) R 9754 30701 30700 0 -1 0 37949 0 0 0 119889 120 0 0 25 0 1 0 487401787 163295232 34585 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39867 34585 603 41 0 39826 0
vsize: 159468
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.04 1.01 0.96 1/54 9812
Raw data (stat): 9755 (minisat+) Z 9754 30701 30700 0 -1 12 37952 0 0 0 119889 127 0 0 25 0 1 0 487401787 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.12
CPU time (s): 1200.17
CPU user time (s): 1198.9
CPU system time (s): 1.27581
CPU usage (%): 100.004
Max. virtual memory (Kb): 159468
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####