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-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	1177.34
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 21370

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        731308 kB
Buffers:         22720 kB
Cached:         259208 kB
SwapCached:          0 kB
Active:          43528 kB
Inactive:       240948 kB
HighTotal:      131008 kB
HighFree:          728 kB
LowTotal:       903652 kB
LowFree:        730580 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13168 kB
Committed_AS:    63520 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:49:14 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 13447 7 1200.25 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.91 0.97 0.99 2/54 6466
Raw data (stat): 6466 (runsolver) R 6465 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490832856 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+9.99982 s]
Raw data (loadavg): 0.93 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 8949 0 0 0 978 20 0 0 25 0 1 0 490832856 39116800 8315 4294967295 134512640 134672761 3221224624 3221223808 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9550 8315 603 41 0 9509 0
vsize: 38200
[startup+19.9996 s]
Raw data (loadavg): 0.94 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9061 0 0 0 1977 21 0 0 25 0 1 0 490832856 39624704 8427 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9674 8427 603 41 0 9633 0
vsize: 38696
[startup+30.0001 s]
Raw data (loadavg): 0.95 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9121 0 0 0 2977 21 0 0 25 0 1 0 490832856 39895040 8487 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9740 8487 603 41 0 9699 0
vsize: 38960
[startup+39.9993 s]
Raw data (loadavg): 0.95 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9312 0 0 0 3977 21 0 0 25 0 1 0 490832856 40718336 8678 4294967295 134512640 134672761 3221224624 3221223796 134556634 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.0003 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9489 0 0 0 4976 22 0 0 25 0 1 0 490832856 41390080 8855 4294967295 134512640 134672761 3221224624 3221223792 134561382 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.0011 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9619 0 0 0 5976 22 0 0 25 0 1 0 490832856 41930752 8985 4294967295 134512640 134672761 3221224624 3221223792 134560852 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.0011 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 9926 0 0 0 6975 23 0 0 25 0 1 0 490832856 43134976 9292 4294967295 134512640 134672761 3221224624 3221223760 134560588 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.002 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10130 0 0 0 7975 23 0 0 25 0 1 0 490832856 44036096 9496 4294967295 134512640 134672761 3221224624 3221223760 134560608 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.0018 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10282 0 0 0 8975 24 0 0 25 0 1 0 490832856 44695552 9648 4294967295 134512640 134672761 3221224624 3221223792 134560842 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.002 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10432 0 0 0 9975 24 0 0 25 0 1 0 490832856 45228032 9798 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11042 9798 603 41 0 11001 0
vsize: 44168
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10563 0 0 0 10974 24 0 0 25 0 1 0 490832856 45760512 9929 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11172 9929 603 41 0 11131 0
vsize: 44688
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10855 0 0 0 11974 25 0 0 25 0 1 0 490832856 46968832 10221 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11467 10221 603 41 0 11426 0
vsize: 45868
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 10921 0 0 0 12974 25 0 0 25 0 1 0 490832856 47239168 10287 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11533 10287 603 41 0 11492 0
vsize: 46132
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 11115 0 0 0 13973 26 0 0 25 0 1 0 490832856 48041984 10481 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11729 10481 603 41 0 11688 0
vsize: 46916
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 11411 0 0 0 14973 27 0 0 25 0 1 0 490832856 49385472 10777 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12057 10777 603 41 0 12016 0
vsize: 48228
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 11659 0 0 0 15972 28 0 0 25 0 1 0 490832856 50319360 11025 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12285 11025 603 41 0 12244 0
vsize: 49140
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 11944 0 0 0 16972 28 0 0 25 0 1 0 490832856 51548160 11310 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12585 11310 603 41 0 12544 0
vsize: 50340
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12178 0 0 0 17972 29 0 0 25 0 1 0 490832856 52461568 11544 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12808 11544 603 41 0 12767 0
vsize: 51232
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12350 0 0 0 18972 29 0 0 25 0 1 0 490832856 53256192 11716 4294967295 134512640 134672761 3221224624 3221223760 134560588 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.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12449 0 0 0 19971 29 0 0 25 0 1 0 490832856 53653504 11815 4294967295 134512640 134672761 3221224624 3221223764 134560629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13099 11815 603 41 0 13058 0
vsize: 52396
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12540 0 0 0 20971 30 0 0 25 0 1 0 490832856 53919744 11906 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13164 11906 603 41 0 13123 0
vsize: 52656
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12677 0 0 0 21971 30 0 0 25 0 1 0 490832856 54587392 12043 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13327 12043 603 41 0 13286 0
vsize: 53308
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12819 0 0 0 22971 30 0 0 25 0 1 0 490832856 55123968 12185 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13458 12185 603 41 0 13417 0
vsize: 53832
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 12955 0 0 0 23970 31 0 0 25 0 1 0 490832856 55660544 12321 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13589 12321 603 41 0 13548 0
vsize: 54356
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 13126 0 0 0 24970 32 0 0 25 0 1 0 490832856 56352768 12492 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13758 12492 603 41 0 13717 0
vsize: 55032
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 13307 0 0 0 25970 32 0 0 25 0 1 0 490832856 57143296 12673 4294967295 134512640 134672761 3221224624 3221223760 134560688 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.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19142 0 0 0 26958 44 0 0 25 0 1 0 490832856 83886080 17888 4294967295 134512640 134672761 3221224624 3221223772 1074754720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20480 17888 603 41 0 20439 0
vsize: 81920
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19239 0 0 0 27956 45 0 0 25 0 1 0 490832856 84021248 17985 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20513 17985 603 41 0 20472 0
vsize: 82052
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19391 0 0 0 28956 45 0 0 25 0 1 0 490832856 84692992 18137 4294967295 134512640 134672761 3221224624 3221223760 134560688 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.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19526 0 0 0 29956 45 0 0 25 0 1 0 490832856 85241856 18272 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20811 18272 603 41 0 20770 0
vsize: 83244
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19590 0 0 0 30956 46 0 0 25 0 1 0 490832856 85504000 18336 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20875 18336 603 41 0 20834 0
vsize: 83500
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19653 0 0 0 31956 46 0 0 25 0 1 0 490832856 85639168 18399 4294967295 134512640 134672761 3221224624 3221223824 134557830 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.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 19965 0 0 0 32955 47 0 0 25 0 1 0 490832856 87248896 18711 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21301 18711 603 41 0 21260 0
vsize: 85204
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 20156 0 0 0 33955 47 0 0 25 0 1 0 490832856 88047616 18902 4294967295 134512640 134672761 3221224624 3221223792 134561382 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.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 20169 0 0 0 34955 47 0 0 25 0 1 0 490832856 88047616 18915 4294967295 134512640 134672761 3221224624 3221223796 134556598 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.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 20245 0 0 0 35955 47 0 0 25 0 1 0 490832856 88317952 18991 4294967295 134512640 134672761 3221224624 3221223792 134560830 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.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 20264 0 0 0 36955 47 0 0 25 0 1 0 490832856 88453120 19010 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21595 19010 603 41 0 21554 0
vsize: 86380
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 25275 0 0 0 37944 59 0 0 25 0 1 0 490832856 103784448 23731 4294967295 134512640 134672761 3221224624 3221223760 134565073 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.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 25313 0 0 0 38944 59 0 0 25 0 1 0 490832856 103927808 23769 4294967295 134512640 134672761 3221224624 3221223796 134556643 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.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 25389 0 0 0 39944 59 0 0 25 0 1 0 490832856 104198144 23845 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25439 23845 603 41 0 25398 0
vsize: 101756
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 25426 0 0 0 40944 59 0 0 25 0 1 0 490832856 104333312 23882 4294967295 134512640 134672761 3221224624 3221223824 134557911 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.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26105 0 0 0 41944 60 0 0 25 0 1 0 490832856 106266624 24271 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26106 0 0 0 42944 60 0 0 25 0 1 0 490832856 106266624 24272 4294967295 134512640 134672761 3221224624 3221223760 134560654 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.002 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26109 0 0 0 43944 60 0 0 25 0 1 0 490832856 106266624 24275 4294967295 134512640 134672761 3221224624 3221223792 134560869 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.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26155 0 0 0 44944 60 0 0 25 0 1 0 490832856 106409984 24321 4294967295 134512640 134672761 3221224624 3221223792 134561372 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.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26246 0 0 0 45944 60 0 0 25 0 1 0 490832856 106807296 24412 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26076 24412 603 41 0 26035 0
vsize: 104304
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26305 0 0 0 46944 60 0 0 25 0 1 0 490832856 107065344 24471 4294967295 134512640 134672761 3221224624 3221223824 134557911 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.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26358 0 0 0 47944 60 0 0 25 0 1 0 490832856 107200512 24524 4294967295 134512640 134672761 3221224624 3221223760 134560640 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.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26412 0 0 0 48944 60 0 0 25 0 1 0 490832856 107474944 24578 4294967295 134512640 134672761 3221224624 3221223792 134560869 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.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26452 0 0 0 49944 60 0 0 25 0 1 0 490832856 107610112 24618 4294967295 134512640 134672761 3221224624 3221223796 134556634 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.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26467 0 0 0 50945 60 0 0 25 0 1 0 490832856 107745280 24633 4294967295 134512640 134672761 3221224624 3221223792 134561261 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 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 26626 0 0 0 51944 61 0 0 25 0 1 0 490832856 108273664 24792 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26434 24792 603 41 0 26393 0
vsize: 105736
[startup+530.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 27706 0 0 0 52941 64 0 0 25 0 1 0 490832856 114745344 25582 4294967295 134512640 134672761 3221224624 3221221656 134524843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25582 603 41 0 27973 0
vsize: 112056
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 31714 0 0 0 53932 74 0 0 25 0 1 0 490832856 142872576 29590 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34881 29590 603 41 0 34840 0
vsize: 139524
[startup+550 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 31833 0 0 0 54932 74 0 0 25 0 1 0 490832856 143413248 29709 4294967295 134512640 134672761 3221224624 3221223792 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35013 29709 603 41 0 34972 0
vsize: 140052
[startup+560 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 31898 0 0 0 55932 74 0 0 25 0 1 0 490832856 143679488 29774 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35078 29774 603 41 0 35037 0
vsize: 140312
[startup+570 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 31952 0 0 0 56932 75 0 0 25 0 1 0 490832856 143814656 29828 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35111 29828 603 41 0 35070 0
vsize: 140444
[startup+580 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32042 0 0 0 57932 75 0 0 25 0 1 0 490832856 144216064 29918 4294967295 134512640 134672761 3221224624 3221223792 134560830 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 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32061 0 0 0 58932 75 0 0 25 0 1 0 490832856 144351232 29937 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35242 29937 603 41 0 35201 0
vsize: 140968
[startup+599.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32261 0 0 0 59931 75 0 0 25 0 1 0 490832856 145145856 30137 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35436 30137 603 41 0 35395 0
vsize: 141744
[startup+609.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32327 0 0 0 60931 75 0 0 25 0 1 0 490832856 145408000 30203 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35500 30203 603 41 0 35459 0
vsize: 142000
[startup+619.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32387 0 0 0 61931 76 0 0 25 0 1 0 490832856 145674240 30263 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35565 30263 603 41 0 35524 0
vsize: 142260
[startup+629.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32475 0 0 0 62931 76 0 0 25 0 1 0 490832856 145944576 30351 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35631 30351 603 41 0 35590 0
vsize: 142524
[startup+639.998 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32554 0 0 0 63931 76 0 0 25 0 1 0 490832856 146345984 30430 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35729 30430 603 41 0 35688 0
vsize: 142916
[startup+649.998 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32639 0 0 0 64931 76 0 0 25 0 1 0 490832856 146616320 30515 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35795 30515 603 41 0 35754 0
vsize: 143180
[startup+659.998 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 32796 0 0 0 65931 77 0 0 25 0 1 0 490832856 147283968 30672 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35958 30672 603 41 0 35917 0
vsize: 143832
[startup+669.998 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33288 0 0 0 66930 77 0 0 25 0 1 0 490832856 149291008 31164 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36448 31164 603 41 0 36407 0
vsize: 145792
[startup+679.998 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33911 0 0 0 67929 79 0 0 25 0 1 0 490832856 150339584 31497 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36704 31497 603 41 0 36663 0
vsize: 146816
[startup+689.998 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33911 0 0 0 68929 79 0 0 25 0 1 0 490832856 150339584 31497 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36704 31497 603 41 0 36663 0
vsize: 146816
[startup+699.998 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33912 0 0 0 69930 79 0 0 25 0 1 0 490832856 150339584 31498 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36704 31498 603 41 0 36663 0
vsize: 146816
[startup+710 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33912 0 0 0 70930 79 0 0 25 0 1 0 490832856 150339584 31498 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36704 31498 603 41 0 36663 0
vsize: 146816
[startup+719.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33912 0 0 0 71930 79 0 0 25 0 1 0 490832856 150339584 31498 4294967295 134512640 134672761 3221224624 3221223840 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36704 31498 603 41 0 36663 0
vsize: 146816
[startup+729.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33912 0 0 0 72930 79 0 0 25 0 1 0 490832856 150339584 31498 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36704 31498 603 41 0 36663 0
vsize: 146816
[startup+740.001 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33913 0 0 0 73930 79 0 0 25 0 1 0 490832856 150339584 31499 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36704 31499 603 41 0 36663 0
vsize: 146816
[startup+750 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33914 0 0 0 74931 79 0 0 25 0 1 0 490832856 150339584 31500 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36704 31500 603 41 0 36663 0
vsize: 146816
[startup+760 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 33967 0 0 0 75931 79 0 0 25 0 1 0 490832856 150482944 31553 4294967295 134512640 134672761 3221224624 3221223808 134559583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36739 31553 603 41 0 36698 0
vsize: 146956
[startup+770 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34015 0 0 0 76931 79 0 0 25 0 1 0 490832856 150781952 31601 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36812 31601 603 41 0 36771 0
vsize: 147248
[startup+780 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34059 0 0 0 77931 79 0 0 25 0 1 0 490832856 150917120 31645 4294967295 134512640 134672761 3221224624 3221223728 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36845 31645 603 41 0 36804 0
vsize: 147380
[startup+790 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34446 0 0 0 78930 80 0 0 25 0 1 0 490832856 152510464 32032 4294967295 134512640 134672761 3221224624 3221223772 1074732988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37234 32032 603 41 0 37193 0
vsize: 148936
[startup+800 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34494 0 0 0 79930 81 0 0 25 0 1 0 490832856 152645632 32080 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37267 32080 603 41 0 37226 0
vsize: 149068
[startup+810 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34550 0 0 0 80930 81 0 0 25 0 1 0 490832856 152915968 32136 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37333 32136 603 41 0 37292 0
vsize: 149332
[startup+819.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34646 0 0 0 81929 81 0 0 25 0 1 0 490832856 153313280 32232 4294967295 134512640 134672761 3221224624 3221223760 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37430 32232 603 41 0 37389 0
vsize: 149720
[startup+829.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34716 0 0 0 82929 81 0 0 25 0 1 0 490832856 153583616 32302 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37496 32302 603 41 0 37455 0
vsize: 149984
[startup+839.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34796 0 0 0 83929 82 0 0 25 0 1 0 490832856 153985024 32382 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37594 32382 603 41 0 37553 0
vsize: 150376
[startup+849.998 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34895 0 0 0 84929 82 0 0 25 0 1 0 490832856 154390528 32481 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37693 32481 603 41 0 37652 0
vsize: 150772
[startup+859.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 34997 0 0 0 85929 82 0 0 25 0 1 0 490832856 154791936 32583 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37791 32583 603 41 0 37750 0
vsize: 151164
[startup+869.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35087 0 0 0 86929 82 0 0 25 0 1 0 490832856 155054080 32673 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37855 32673 603 41 0 37814 0
vsize: 151420
[startup+879.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35177 0 0 0 87929 83 0 0 25 0 1 0 490832856 155455488 32763 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37953 32763 603 41 0 37912 0
vsize: 151812
[startup+889.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35229 0 0 0 88929 83 0 0 25 0 1 0 490832856 155729920 32815 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38020 32815 603 41 0 37979 0
vsize: 152080
[startup+899.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35258 0 0 0 89929 83 0 0 25 0 1 0 490832856 155865088 32844 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38053 32844 603 41 0 38012 0
vsize: 152212
[startup+909.999 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35294 0 0 0 90929 83 0 0 25 0 1 0 490832856 156000256 32880 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38086 32880 603 41 0 38045 0
vsize: 152344
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35356 0 0 0 91929 84 0 0 25 0 1 0 490832856 156135424 32942 4294967295 134512640 134672761 3221224624 3221223796 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38119 32942 603 41 0 38078 0
vsize: 152476
[startup+930.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35440 0 0 0 92929 84 0 0 25 0 1 0 490832856 156540928 33026 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38218 33026 603 41 0 38177 0
vsize: 152872
[startup+940.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35686 0 0 0 93929 85 0 0 25 0 1 0 490832856 157478912 33272 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38447 33272 603 41 0 38406 0
vsize: 153788
[startup+950.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 35887 0 0 0 94928 85 0 0 25 0 1 0 490832856 158285824 33473 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38644 33473 603 41 0 38603 0
vsize: 154576
[startup+960.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36096 0 0 0 95928 86 0 0 25 0 1 0 490832856 159215616 33682 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38871 33682 603 41 0 38830 0
vsize: 155484
[startup+970.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36124 0 0 0 96928 86 0 0 25 0 1 0 490832856 159354880 33710 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38905 33710 603 41 0 38864 0
vsize: 155620
[startup+980.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36214 0 0 0 97928 86 0 0 25 0 1 0 490832856 159752192 33800 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39002 33800 603 41 0 38961 0
vsize: 156008
[startup+990.003 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36330 0 0 0 98928 86 0 0 25 0 1 0 490832856 160157696 33916 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39101 33916 603 41 0 39060 0
vsize: 156404
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36440 0 0 0 99928 86 0 0 25 0 1 0 490832856 160559104 34026 4294967295 134512640 134672761 3221224624 3221223796 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39199 34026 603 41 0 39158 0
vsize: 156796
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36441 0 0 0 100928 86 0 0 25 0 1 0 490832856 160559104 34027 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39199 34027 603 41 0 39158 0
vsize: 156796
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36462 0 0 0 101928 86 0 0 25 0 1 0 490832856 160690176 34048 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39231 34048 603 41 0 39190 0
vsize: 156924
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36493 0 0 0 102928 87 0 0 25 0 1 0 490832856 160821248 34079 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39263 34079 603 41 0 39222 0
vsize: 157052
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36520 0 0 0 103928 87 0 0 25 0 1 0 490832856 160952320 34106 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39295 34106 603 41 0 39254 0
vsize: 157180
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 36570 0 0 0 104929 87 0 0 25 0 1 0 490832856 161087488 34156 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39328 34156 603 41 0 39287 0
vsize: 157312
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37104 0 0 0 105927 88 0 0 25 0 1 0 490832856 161308672 34218 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39382 34218 603 41 0 39341 0
vsize: 157528
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37107 0 0 0 106927 88 0 0 25 0 1 0 490832856 161443840 34221 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39415 34221 603 41 0 39374 0
vsize: 157660
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37111 0 0 0 107927 88 0 0 25 0 1 0 490832856 161443840 34225 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39415 34225 603 41 0 39374 0
vsize: 157660
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37139 0 0 0 108927 88 0 0 25 0 1 0 490832856 161443840 34253 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39415 34253 603 41 0 39374 0
vsize: 157660
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37176 0 0 0 109927 88 0 0 25 0 1 0 490832856 162238464 34290 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39609 34290 603 41 0 39568 0
vsize: 158436
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37234 0 0 0 110928 88 0 0 25 0 1 0 490832856 162373632 34348 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39642 34348 603 41 0 39601 0
vsize: 158568
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37746 0 0 0 111926 90 0 0 25 0 1 0 490832856 162480128 34382 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39668 34382 603 41 0 39627 0
vsize: 158672
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37746 0 0 0 112927 90 0 0 25 0 1 0 490832856 162480128 34382 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39668 34382 603 41 0 39627 0
vsize: 158672
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37812 0 0 0 113927 90 0 0 25 0 1 0 490832856 162750464 34448 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39734 34448 603 41 0 39693 0
vsize: 158936
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37898 0 0 0 114927 90 0 0 25 0 1 0 490832856 163160064 34534 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39834 34534 603 41 0 39793 0
vsize: 159336
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37917 0 0 0 115927 90 0 0 25 0 1 0 490832856 163295232 34553 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39867 34553 603 41 0 39826 0
vsize: 159468
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37928 0 0 0 116927 90 0 0 25 0 1 0 490832856 163295232 34564 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39867 34564 603 41 0 39826 0
vsize: 159468
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37938 0 0 0 117927 90 0 0 25 0 1 0 490832856 163295232 34574 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39867 34574 603 41 0 39826 0
vsize: 159468
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37948 0 0 0 118927 90 0 0 25 0 1 0 490832856 163295232 34584 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39867 34584 603 41 0 39826 0
vsize: 159468
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 6466
Raw data (stat): 6466 (minisat+) R 6465 25347 25346 0 -1 0 37977 0 0 0 119928 90 0 0 25 0 1 0 490832856 163430400 34613 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39900 34613 603 41 0 39859 0
vsize: 159600
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.99 1/54 6466
Raw data (stat): 6466 (minisat+) Z 6465 25347 25346 0 -1 12 37980 0 0 0 119928 97 0 0 25 0 1 0 490832856 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.25
CPU user time (s): 1199.28
CPU system time (s): 0.971852
CPU usage (%): 100.015
Max. virtual memory (Kb): 159600
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####