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 21331

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        868832 kB
Buffers:         14732 kB
Cached:         127028 kB
SwapCached:        360 kB
Active:          10132 kB
Inactive:       134128 kB
HighTotal:      131008 kB
HighFree:        96684 kB
LowTotal:       903652 kB
LowFree:        772148 kB
SwapTotal:     2097892 kB
SwapFree:      2097056 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5860 kB
Slab:            15856 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:45:53 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 13454 7 1200.21 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]---> BDD-cost:  231
c ---[  35]---> BDD-cost:  231
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:  183
c ---[  31]---> BDD-cost:   25
c ---[  30]---> BDD-cost:  126
c ---[  29]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  128
c ---[  27]---> BDD-cost:  105
c ---[  26]---> BDD-cost:  185
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]---> BDD-cost: 7378
c ---[   9]---> BDD-cost:  669
c ---[   8]---> BDD-cost:   76
c ---[   7]---> BDD-cost: 1557
c ---[   6]---> BDD-cost: 1215
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:  114
c ---[   3]---> BDD-cost:   55
c ---[   2]---> BDD-cost: 2937
c ---[   1]---> BDD-cost: 1052
c ---[   0]---> BDD-cost:   92
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   45289   134500 |   15096       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 228152[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:92447     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 |         2 |  298890   726329 |   99630       2       12     6.0 |  0.000 % |
c |       105 |  298124   724597 |  109593     101      535     5.3 |  0.281 % |
c |       255 |  297317   722773 |  120552     250     5224    20.9 |  0.486 % |
c |       480 |  295636   718946 |  132607     471    10583    22.5 |  0.945 % |
c |       817 |  293957   715105 |  145868     806    24487    30.4 |  1.417 % |
c |      1325 |  287505   700303 |  160455    1282    27144    21.2 |  3.285 % |
c |      2086 |  274412   670155 |  176500    1959    41217    21.0 |  7.185 % |
c ==============================================================================
c [1mFound solution: 228107[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:72978     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 |      2182 |  455370  1091535 |  151790    2051    43708    21.3 |  7.185 % |
c |      2282 |  455370  1091535 |  166969    2151    45808    21.3 |  7.218 % |
c |      2432 |  450153  1079714 |  183665    2295    49252    21.5 |  8.191 % |
c |      2657 |  450153  1079714 |  202032    2520    53000    21.0 |  8.191 % |
c |      2994 |  441724  1060467 |  222235    2817    56525    20.1 |  9.728 % |
c |      3500 |  441049  1058922 |  244459    3317    64078    19.3 |  9.849 % |
c |      4259 |  441049  1058922 |  268905    4076    70538    17.3 |  9.849 % |
c |      5398 |  441049  1058922 |  295795    5215    81194    15.6 |  9.849 % |
c |      7108 |  440946  1058682 |  325375    6924   102009    14.7 |  9.869 % |
c ==============================================================================
c [1mFound solution: 228003[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:68318     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 |      7782 |  598189  1424680 |  199396    7400   107739    14.6 |  9.869 % |
c |      7883 |  598038  1424335 |  219335    7499   109071    14.5 | 11.279 % |
c |      8033 |  593293  1413534 |  241269    7260   106197    14.6 | 11.923 % |
c |      8260 |  593279  1413501 |  265396    7440   120478    16.2 | 11.925 % |
c ==============================================================================
c [1mFound solution: 226571[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 |      8298 |  593064  1413790 |  197688    7476   124044    16.6 | 11.925 % |
c |      8398 |  592851  1413314 |  217456    7572   125841    16.6 | 11.979 % |
c |      8548 |  592248  1411977 |  239202    7719   126514    16.4 | 12.064 % |
c ==============================================================================
c [1mFound solution: 225156[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     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 |      8610 |  589147  1404947 |  196382    7720   126643    16.4 | 12.064 % |
c |      8710 |  589147  1404947 |  216020    7820   127668    16.3 | 12.483 % |
c |      8861 |  589147  1404947 |  237622    7971   128755    16.2 | 12.483 % |
c |      9086 |  587881  1402070 |  261384    8192   130321    15.9 | 12.657 % |
c |      9424 |  581084  1386553 |  287522    8444   131552    15.6 | 13.585 % |
c |      9930 |  577887  1379236 |  316275    8856   141272    16.0 | 14.021 % |
c |     10689 |  575421  1373584 |  347902    9496   146897    15.5 | 14.357 % |
c |     11828 |  574402  1371278 |  382692   10609   187884    17.7 | 14.493 % |
c |     13538 |  570586  1362558 |  420962   12281   264267    21.5 | 15.004 % |
c |     16101 |  569103  1359156 |  463058   14831   402467    27.1 | 15.208 % |
c |     19945 |  567496  1355462 |  509364   18667   828516    44.4 | 15.426 % |
c ==============================================================================
c [1mFound solution: 224882[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     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 |     20299 |  567509  1355605 |  189169   19021   836114    44.0 | 15.426 % |
c |     20399 |  567509  1355605 |  208085   19121   840088    43.9 | 15.426 % |
c |     20549 |  567329  1355202 |  228894   19269   844134    43.8 | 15.446 % |
c |     20774 |  564229  1348123 |  251783   19421   844924    43.5 | 15.867 % |
c |     21111 |  564229  1348123 |  276962   19758   850448    43.0 | 15.867 % |
c |     21617 |  564126  1347891 |  304658   20263   857199    42.3 | 15.882 % |
c |     22378 |  563650  1346812 |  335124   21011   862862    41.1 | 15.947 % |
c |     23517 |  561569  1342052 |  368636   22103   881716    39.9 | 16.231 % |
c ==============================================================================
c [1mFound solution: 222653[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 |     24619 |  558563  1335130 |  186187   22960   956712    41.7 | 16.231 % |
c |     24719 |  558563  1335130 |  204805   23060   958791    41.6 | 16.639 % |
c |     24871 |  558539  1335075 |  225286   23211   963417    41.5 | 16.642 % |
c |     25098 |  556797  1331061 |  247814   23357   966618    41.4 | 16.880 % |
c |     25435 |  551457  1318704 |  272596   23537   966536    41.1 | 17.622 % |
c |     25941 |  551302  1318351 |  299856   24037   977475    40.7 | 17.643 % |
c |     26703 |  551302  1318351 |  329841   24799  1021116    41.2 | 17.643 % |
c ==============================================================================
c [1mFound solution: 120481[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 |     26816 |  551347  1318463 |  183782   24912  1024011    41.1 | 17.643 % |
c |     26918 |  551301  1318356 |  202160   25013  1025225    41.0 | 17.649 % |
c |     27068 |  551301  1318356 |  222376   25163  1031087    41.0 | 17.649 % |
c |     27296 |  551301  1318356 |  244613   25391  1065796    42.0 | 17.649 % |
c |     27633 |  549875  1315069 |  269075   25550  1084183    42.4 | 17.844 % |
c |     28139 |  549517  1314253 |  295982   26053  1088933    41.8 | 17.889 % |
c |     28899 |  548230  1311311 |  325581   26791  1097334    41.0 | 18.056 % |
c |     30038 |  543493  1300399 |  358139   27750  1115651    40.2 | 18.701 % |
c ==============================================================================
c [1mFound solution: 119791[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 |     30534 |  543495  1300408 |  181165   28245  1134636    40.2 | 18.701 % |
c |     30634 |  542867  1298964 |  199281   28327  1137163    40.1 | 18.787 % |
c |     30787 |  542867  1298964 |  219209   28480  1140643    40.1 | 18.787 % |
c |     31012 |  542867  1298964 |  241130   28705  1152607    40.2 | 18.787 % |
c |     31349 |  538587  1289074 |  265243   28715  1156875    40.3 | 19.378 % |
c |     31855 |  538397  1288634 |  291768   29217  1161472    39.8 | 19.404 % |
c |     32614 |  537715  1287065 |  320944   29869  1170464    39.2 | 19.497 % |
c |     33753 |  537468  1286494 |  353039   30995  1187597    38.3 | 19.532 % |
c |     35462 |  533253  1276753 |  388343   32596  1263680    38.8 | 20.112 % |
c ==============================================================================
c [1mFound solution: 118096[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 |     35657 |  533267  1276787 |  177755   32791  1284635    39.2 | 20.112 % |
c |     35757 |  533267  1276787 |  195530   32891  1287773    39.2 | 20.112 % |
c |     35907 |  532417  1274825 |  215083   32963  1288290    39.1 | 20.229 % |
c |     36132 |  532417  1274825 |  236591   33188  1299883    39.2 | 20.229 % |
c |     36469 |  532417  1274825 |  260251   33525  1302922    38.9 | 20.229 % |
c |     36975 |  531944  1273732 |  286276   33906  1320618    38.9 | 20.296 % |
c |     37734 |  531944  1273732 |  314903   34665  1341440    38.7 | 20.296 % |
c |     38874 |  531861  1273544 |  346394   35803  1419556    39.6 | 20.307 % |
c |     40582 |  530900  1271335 |  381033   37504  1515069    40.4 | 20.437 % |
c ==============================================================================
c [1mFound solution: 116340[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     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 |     41153 |  530748  1270984 |  176916   38066  1536021    40.4 | 20.437 % |
c |     41253 |  529765  1268705 |  194607   38156  1537843    40.3 | 20.596 % |
c |     41404 |  527957  1264539 |  214068   38170  1538217    40.3 | 20.841 % |
c |     41629 |  526967  1262274 |  235475   38379  1546527    40.3 | 20.973 % |
c |     41967 |  526967  1262274 |  259022   38717  1552391    40.1 | 20.973 % |
c |     42473 |  526311  1260774 |  284924   39078  1554205    39.8 | 21.060 % |
c |     43233 |  526311  1260774 |  313417   39838  1564762    39.3 | 21.060 % |
c |     44374 |  525407  1258697 |  344759   40934  1610696    39.3 | 21.184 % |
c |     46082 |  524738  1257157 |  379235   42622  1729510    40.6 | 21.277 % |
c ==============================================================================
c [1mFound solution: 112950[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 |     46141 |  524322  1256197 |  174774   42680  1736911    40.7 | 21.277 % |
c |     46241 |  524322  1256197 |  192251   42780  1740112    40.7 | 21.336 % |
c |     46394 |  524322  1256197 |  211476   42933  1741348    40.6 | 21.336 % |
c |     46620 |  524322  1256197 |  232624   43159  1743123    40.4 | 21.336 % |
c |     46957 |  524322  1256197 |  255886   43496  1745234    40.1 | 21.336 % |
c |     47463 |  524322  1256197 |  281475   44002  1749672    39.8 | 21.336 % |
c |     48222 |  523760  1254895 |  309622   44748  1761216    39.4 | 21.416 % |
c |     49365 |  523760  1254895 |  340585   45891  1789036    39.0 | 21.416 % |
c |     51074 |  523451  1254182 |  374643   47542  1918282    40.3 | 21.460 % |
c |     53637 |  523230  1253676 |  412107   50100  2089988    41.7 | 21.489 % |
c |     57482 |  519536  1245170 |  453318   53663  2331890    43.5 | 21.985 % |
c ==============================================================================
c [1mFound solution: 110854[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 |     57516 |  519310  1244651 |  173103   53695  2336515    43.5 | 21.985 % |
c |     57616 |  519310  1244651 |  190413   53795  2338342    43.5 | 22.016 % |
c |     57766 |  519310  1244651 |  209454   53945  2342960    43.4 | 22.016 % |
c |     57993 |  519310  1244651 |  230400   54172  2346033    43.3 | 22.016 % |
c |     58330 |  518541  1242880 |  253440   54482  2350570    43.1 | 22.121 % |
c |     58836 |  517156  1239688 |  278784   54936  2353957    42.8 | 22.311 % |
c |     59595 |  516045  1237127 |  306662   55665  2377705    42.7 | 22.463 % |
c |     60735 |  515589  1236076 |  337328   56771  2459751    43.3 | 22.526 % |
c ==============================================================================
c [1mFound solution: 76236[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     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 |     61651 |  515612  1236131 |  171870   57687  2565392    44.5 | 22.526 % |
c |     61751 |  515374  1235581 |  189057   57781  2570479    44.5 | 22.557 % |
c |     61902 |  515374  1235581 |  207962   57932  2584955    44.6 | 22.557 % |
c |     62127 |  515374  1235581 |  228758   58157  2599969    44.7 | 22.557 % |
c |     62464 |  514964  1234631 |  251634   58440  2615640    44.8 | 22.615 % |
c |     62971 |  513351  1230928 |  276798   58582  2619291    44.7 | 22.835 % |
c |     63731 |  513351  1230928 |  304478   59342  2647464    44.6 | 22.835 % |
c |     64870 |  513351  1230928 |  334926   60481  2666471    44.1 | 22.835 % |
c ==============================================================================
c [1mFound solution: 75858[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 |     66316 |  511544  1226747 |  170514   61832  2879140    46.6 | 22.835 % |
c |     66417 |  511305  1226189 |  187565   61914  2889868    46.7 | 23.122 % |
c |     66567 |  510740  1224874 |  206321   62053  2891563    46.6 | 23.203 % |
c |     66792 |  510726  1224842 |  226954   62276  2898742    46.5 | 23.205 % |
c ==============================================================================
c [1mFound solution: 75739[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 |     66892 |  510498  1224314 |  170166   62374  2904417    46.6 | 23.205 % |
c |     66992 |  510498  1224314 |  187182   62474  2909023    46.6 | 23.240 % |
c |     67142 |  510498  1224314 |  205900   62624  2912865    46.5 | 23.240 % |
c |     67369 |  508841  1220497 |  226490   62692  2913240    46.5 | 23.466 % |
c |     67706 |  508821  1220450 |  249140   63016  2927307    46.5 | 23.469 % |
c |     68213 |  507776  1218035 |  274054   63512  2993275    47.1 | 23.610 % |
c ==============================================================================
c [1mFound solution: 74881[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     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 |     68289 |  507789  1218067 |  169263   63588  3002926    47.2 | 23.610 % |
c |     68392 |  507789  1218067 |  186189   63691  3017355    47.4 | 23.610 % |
c |     68542 |  507323  1216992 |  204808   63828  3022418    47.4 | 23.677 % |
c |     68767 |  506850  1215908 |  225289   63984  3030816    47.4 | 23.739 % |
c ==============================================================================
c [1mFound solution: 71337[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 |     69043 |  506863  1215947 |  168954   64260  3055644    47.6 | 23.739 % |
c |     69145 |  505567  1212960 |  185849   64309  3057894    47.6 | 23.915 % |
c ==============================================================================
c [1mFound solution: 71054[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 |     69209 |  505562  1212956 |  168520   64372  3059874    47.5 | 23.915 % |
c ==============================================================================
c [1mFound solution: 69614[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     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 |     69239 |  505572  1212982 |  168524   64402  3061029    47.5 | 23.915 % |
c |     69339 |  505572  1212982 |  185376   64502  3066241    47.5 | 23.916 % |
c |     69490 |  505572  1212982 |  203914   64653  3070609    47.5 | 23.916 % |
c |     69715 |  505572  1212982 |  224305   64878  3077896    47.4 | 23.916 % |
c |     70053 |  505202  1212131 |  246735   65195  3100673    47.6 | 23.963 % |
c ==============================================================================
c [1mFound solution: 68795[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     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 |     70179 |  505216  1212166 |  168405   65321  3114607    47.7 | 23.963 % |
c |     70279 |  505216  1212166 |  185245   65421  3115979    47.6 | 23.962 % |
c |     70429 |  505123  1211953 |  203770   65570  3118930    47.6 | 23.974 % |
c |     70654 |  504188  1209790 |  224147   65759  3121473    47.5 | 24.104 % |
c |     70991 |  504188  1209790 |  246561   66096  3138484    47.5 | 24.104 % |
c ==============================================================================
c [1mFound solution: 68554[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 |     71011 |  504200  1209821 |  168066   66116  3141878    47.5 | 24.104 % |
c |     71111 |  503917  1209163 |  184872   66212  3164635    47.8 | 24.146 % |
c |     71263 |  503917  1209163 |  203359   66364  3167458    47.7 | 24.146 % |
c |     71488 |  503842  1208992 |  223695   66584  3171024    47.6 | 24.156 % |
c |     71827 |  503415  1208009 |  246065   66702  3173054    47.6 | 24.215 % |
c |     72333 |  503138  1207370 |  270671   67017  3179237    47.4 | 24.254 % |
c |     73093 |  502444  1205777 |  297739   67381  3200953    47.5 | 24.347 % |
c ==============================================================================
c [1mFound solution: 64777[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     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 |     73150 |  501869  1204457 |  167289   67422  3205237    47.5 | 24.347 % |
c |     73251 |  501809  1204320 |  184017   67522  3216871    47.6 | 24.433 % |
c |     73402 |  499991  1200109 |  202419   66414  3131920    47.2 | 24.681 % |
c |     73627 |  498522  1196710 |  222661   66154  3130036    47.3 | 24.886 % |
c |     73965 |  498515  1196695 |  244927   66489  3135457    47.2 | 24.887 % |
c |     74471 |  497408  1194129 |  269420   66921  3147606    47.0 | 25.043 % |
c |     75232 |  497216  1193682 |  296362   67677  3167750    46.8 | 25.070 % |
c |     76371 |  497216  1193682 |  325998   68816  3212914    46.7 | 25.070 % |
c |     78079 |  497210  1193668 |  358598   70520  3372262    47.8 | 25.071 % |
c ==============================================================================
c [1mFound solution: 64343[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:52219     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 |     78296 |  595370  1421212 |  198456   70737  3420063    48.3 | 25.071 % |
c ==============================================================================
c [1mFound solution: 64308[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     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 |     78341 |  595405  1421588 |  198468   70782  3424089    48.4 | 25.071 % |
c |     78441 |  594640  1419832 |  218314   70873  3426664    48.3 | 25.761 % |
c |     78591 |  593992  1418326 |  240146   70954  3430454    48.3 | 25.836 % |
c |     78817 |  593992  1418326 |  264160   71180  3442997    48.4 | 25.836 % |
c |     79155 |  593920  1418160 |  290576   71517  3478608    48.6 | 25.844 % |
c |     79661 |  593836  1417966 |  319634   72015  3515965    48.8 | 25.853 % |
c |     80421 |  591282  1412194 |  351598   72537  3570749    49.2 | 26.139 % |
c |     81561 |  590980  1411521 |  386757   73670  3649538    49.5 | 26.173 % |
c |     83270 |  590798  1411120 |  425433   75378  4503969    59.8 | 26.194 % |
c |     85834 |  586920  1402191 |  467977   77813  4694498    60.3 | 26.638 % |
c |     89678 |  586213  1400603 |  514774   81607  5103308    62.5 | 26.720 % |
c ==============================================================================
c [1mFound solution: 52018[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:65838     Base: 2 2 2 2 3 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90997 |  719458  1709984 |  239819   82576  5331159    64.6 | 26.720 % |
c |     91097 |  718738  1708328 |  263800   82666  5337543    64.6 | 26.453 % |
c |     91249 |  718738  1708328 |  290180   82818  5381999    65.0 | 26.453 % |
c |     91475 |  718738  1708328 |  319199   83044  5413728    65.2 | 26.453 % |
c |     91812 |  718383  1707517 |  351118   83376  5435360    65.2 | 26.486 % |
c |     92318 |  718383  1707517 |  386230   83882  5443883    64.9 | 26.486 % |
c |     93077 |  718383  1707517 |  424853   84641  5494325    64.9 | 26.486 % |
c |     94219 |  716739  1703848 |  467339   85767  5575556    65.0 | 26.637 % |
c |     95929 |  716739  1703848 |  514073   87477  5774198    66.0 | 26.637 % |
c |     98491 |  715748  1701587 |  565480   90000  5988895    66.5 | 26.732 % |
c ==============================================================================
c [1mFound solution: 51169[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 3 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99097 |  715770  1702086 |  238590   90606  6150562    67.9 | 26.732 % |
c |     99197 |  715770  1702086 |  262449   90706  6154126    67.8 | 26.731 % |
c |     99348 |  715770  1702086 |  288693   90857  6193168    68.2 | 26.731 % |
c |     99574 |  715770  1702086 |  317563   91083  6195320    68.0 | 26.731 % |
c |     99911 |  715770  1702086 |  349319   91420  6198919    67.8 | 26.731 % |
c |    100419 |  715539  1701548 |  384251   91921  6203500    67.5 | 26.754 % |
c |    101178 |  715539  1701548 |  422676   92680  6210496    67.0 | 26.754 % |
c |    102317 |  715525  1701516 |  464944   93818  6273714    66.9 | 26.755 % |
c |    104025 |  715452  1701358 |  511438   95525  6414020    67.1 | 26.762 % |
c ==============================================================================
c [1mFound solution: 50473[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 3 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    104106 |  715467  1701508 |  238489   95606  6444430    67.4 | 26.762 % |
c |    104206 |  715467  1701508 |  262337   95706  6456108    67.5 | 26.762 % |
c |    104358 |  715122  1700718 |  288571   95843  6464966    67.5 | 26.795 % |
c |    104584 |  715122  1700718 |  317428   96069  6476632    67.4 | 26.795 % |
c |    104921 |  714551  1699432 |  349171   96318  6481465    67.3 | 26.847 % |
c |    105428 |  714551  1699432 |  384088   96825  6497453    67.1 | 26.847 % |
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_0#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/55 7238
Raw data (stat): 7238 (runsolver) R 7237 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549034218 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0004 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 9073 0 0 0 969 24 0 0 25 0 1 0 549034218 40308736 8722 4294967295 134512640 134672761 3221224544 3221223680 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9841 8722 603 41 0 9800 0
vsize: 39364
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 14818 0 0 0 1954 39 0 0 25 0 1 0 549034218 67272704 14137 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16424 14137 603 41 0 16383 0
vsize: 65696
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 14848 0 0 0 2954 40 0 0 25 0 1 0 549034218 67272704 14167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16424 14167 603 41 0 16383 0
vsize: 65696
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 14901 0 0 0 3953 40 0 0 25 0 1 0 549034218 67538944 14220 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16489 14220 603 41 0 16448 0
vsize: 65956
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19653 0 0 0 4941 52 0 0 25 0 1 0 549034218 83431424 18972 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20369 18972 603 41 0 20328 0
vsize: 81476
[startup+60.0008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19785 0 0 0 5941 53 0 0 25 0 1 0 549034218 83558400 19104 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20400 19104 603 41 0 20359 0
vsize: 81600
[startup+70.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19796 0 0 0 6941 53 0 0 25 0 1 0 549034218 83607552 19115 4294967295 134512640 134672761 3221224544 3221223728 134558500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20412 19115 603 41 0 20371 0
vsize: 81648
[startup+80.0021 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19812 0 0 0 7940 54 0 0 25 0 1 0 549034218 83742720 19131 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20445 19131 603 41 0 20404 0
vsize: 81780
[startup+90.0018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19830 0 0 0 8940 54 0 0 25 0 1 0 549034218 83742720 19149 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20445 19149 603 41 0 20404 0
vsize: 81780
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19845 0 0 0 9940 55 0 0 25 0 1 0 549034218 83873792 19164 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20477 19164 603 41 0 20436 0
vsize: 81908
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19879 0 0 0 10940 55 0 0 25 0 1 0 549034218 84045824 19198 4294967295 134512640 134672761 3221224544 3221223600 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20519 19198 603 41 0 20478 0
vsize: 82076
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 19920 0 0 0 11940 55 0 0 25 0 1 0 549034218 84180992 19239 4294967295 134512640 134672761 3221224544 3221223680 134560637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20552 19239 603 41 0 20511 0
vsize: 82208
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20058 0 0 0 12940 55 0 0 25 0 1 0 549034218 84721664 19377 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20684 19377 603 41 0 20643 0
vsize: 82736
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20317 0 0 0 13939 56 0 0 25 0 1 0 549034218 85852160 19636 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20960 19636 603 41 0 20919 0
vsize: 83840
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20482 0 0 0 14939 56 0 0 25 0 1 0 549034218 86540288 19801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21128 19801 603 41 0 21087 0
vsize: 84512
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20548 0 0 0 15939 56 0 0 25 0 1 0 549034218 86794240 19867 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21190 19867 603 41 0 21149 0
vsize: 84760
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20548 0 0 0 16939 56 0 0 25 0 1 0 549034218 86794240 19867 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21190 19867 603 41 0 21149 0
vsize: 84760
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20558 0 0 0 17939 56 0 0 25 0 1 0 549034218 86929408 19877 4294967295 134512640 134672761 3221224544 3221223808 134562492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21223 19877 603 41 0 21182 0
vsize: 84892
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7238
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20625 0 0 0 18939 57 0 0 25 0 1 0 549034218 87199744 19944 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21289 19944 603 41 0 21248 0
vsize: 85156
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20674 0 0 0 19939 57 0 0 25 0 1 0 549034218 87293952 19993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21312 19993 603 41 0 21271 0
vsize: 85248
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20675 0 0 0 20939 57 0 0 25 0 1 0 549034218 87293952 19994 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21312 19994 603 41 0 21271 0
vsize: 85248
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20713 0 0 0 21939 57 0 0 25 0 1 0 549034218 87564288 20032 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21378 20032 603 41 0 21337 0
vsize: 85512
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20749 0 0 0 22939 57 0 0 25 0 1 0 549034218 87699456 20068 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21411 20068 603 41 0 21370 0
vsize: 85644
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20783 0 0 0 23939 57 0 0 25 0 1 0 549034218 87834624 20102 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21444 20102 603 41 0 21403 0
vsize: 85776
[startup+250 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20795 0 0 0 24939 58 0 0 25 0 1 0 549034218 87834624 20114 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21444 20114 603 41 0 21403 0
vsize: 85776
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20815 0 0 0 25939 58 0 0 25 0 1 0 549034218 87969792 20134 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21477 20134 603 41 0 21436 0
vsize: 85908
[startup+269.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20856 0 0 0 26939 58 0 0 25 0 1 0 549034218 88018944 20175 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21489 20175 603 41 0 21448 0
vsize: 85956
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20856 0 0 0 27939 58 0 0 25 0 1 0 549034218 88018944 20175 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21489 20175 603 41 0 21448 0
vsize: 85956
[startup+290 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20878 0 0 0 28939 58 0 0 25 0 1 0 549034218 88150016 20197 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21521 20197 603 41 0 21480 0
vsize: 86084
[startup+299.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 20963 0 0 0 29939 59 0 0 25 0 1 0 549034218 88551424 20282 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21619 20282 603 41 0 21578 0
vsize: 86476
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21009 0 0 0 30939 59 0 0 25 0 1 0 549034218 88813568 20328 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21683 20328 603 41 0 21642 0
vsize: 86732
[startup+319.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21030 0 0 0 31939 59 0 0 25 0 1 0 549034218 88948736 20349 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21716 20349 603 41 0 21675 0
vsize: 86864
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21092 0 0 0 32939 60 0 0 25 0 1 0 549034218 89083904 20411 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21749 20411 603 41 0 21708 0
vsize: 86996
[startup+340 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21186 0 0 0 33938 60 0 0 25 0 1 0 549034218 89485312 20505 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21847 20505 603 41 0 21806 0
vsize: 87388
[startup+350 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21248 0 0 0 34938 60 0 0 25 0 1 0 549034218 89751552 20567 4294967295 134512640 134672761 3221224544 3221223104 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21912 20567 603 41 0 21871 0
vsize: 87648
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21270 0 0 0 35938 61 0 0 25 0 1 0 549034218 89808896 20589 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21926 20589 603 41 0 21885 0
vsize: 87704
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21273 0 0 0 36938 61 0 0 25 0 1 0 549034218 89808896 20592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21926 20592 603 41 0 21885 0
vsize: 87704
[startup+380 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21422 0 0 0 37938 61 0 0 25 0 1 0 549034218 90476544 20741 4294967295 134512640 134672761 3221224544 3221223648 134559818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22089 20741 603 41 0 22048 0
vsize: 88356
[startup+390 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21493 0 0 0 38938 62 0 0 25 0 1 0 549034218 90701824 20812 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22144 20812 603 41 0 22103 0
vsize: 88576
[startup+400 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21550 0 0 0 39938 62 0 0 25 0 1 0 549034218 90968064 20869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22209 20869 603 41 0 22168 0
vsize: 88836
[startup+410 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21684 0 0 0 40938 62 0 0 25 0 1 0 549034218 91504640 21003 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22340 21003 603 41 0 22299 0
vsize: 89360
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21818 0 0 0 41937 63 0 0 25 0 1 0 549034218 92041216 21137 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22471 21137 603 41 0 22430 0
vsize: 89884
[startup+430 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 21858 0 0 0 42937 63 0 0 25 0 1 0 549034218 92176384 21177 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22504 21177 603 41 0 22463 0
vsize: 90016
[startup+440 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22009 0 0 0 43937 63 0 0 25 0 1 0 549034218 92844032 21328 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22667 21328 603 41 0 22626 0
vsize: 90668
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22140 0 0 0 44936 64 0 0 25 0 1 0 549034218 93384704 21459 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22799 21459 603 41 0 22758 0
vsize: 91196
[startup+460 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22163 0 0 0 45937 64 0 0 25 0 1 0 549034218 93409280 21482 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22805 21482 603 41 0 22764 0
vsize: 91220
[startup+470 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22164 0 0 0 46937 64 0 0 25 0 1 0 549034218 93409280 21483 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22805 21483 603 41 0 22764 0
vsize: 91220
[startup+479.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22199 0 0 0 47937 64 0 0 25 0 1 0 549034218 93540352 21518 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22837 21518 603 41 0 22796 0
vsize: 91348
[startup+489.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7240
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22272 0 0 0 48937 64 0 0 25 0 1 0 549034218 93954048 21591 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22938 21591 603 41 0 22897 0
vsize: 91752
[startup+499.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22353 0 0 0 49937 64 0 0 25 0 1 0 549034218 94224384 21672 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23004 21672 603 41 0 22963 0
vsize: 92016
[startup+509.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22403 0 0 0 50937 65 0 0 25 0 1 0 549034218 94371840 21722 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23040 21722 603 41 0 22999 0
vsize: 92160
[startup+519.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22418 0 0 0 51937 65 0 0 25 0 1 0 549034218 94507008 21737 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23073 21737 603 41 0 23032 0
vsize: 92292
[startup+529.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22446 0 0 0 52937 65 0 0 25 0 1 0 549034218 94638080 21765 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23105 21765 603 41 0 23064 0
vsize: 92420
[startup+539.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22458 0 0 0 53937 65 0 0 25 0 1 0 549034218 94638080 21777 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23105 21777 603 41 0 23064 0
vsize: 92420
[startup+549.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22487 0 0 0 54937 65 0 0 25 0 1 0 549034218 94769152 21806 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23137 21806 603 41 0 23096 0
vsize: 92548
[startup+559.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22520 0 0 0 55937 65 0 0 25 0 1 0 549034218 94904320 21839 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23170 21839 603 41 0 23129 0
vsize: 92680
[startup+569.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22743 0 0 0 56937 65 0 0 25 0 1 0 549034218 95752192 22062 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23377 22062 603 41 0 23336 0
vsize: 93508
[startup+579.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22779 0 0 0 57937 65 0 0 25 0 1 0 549034218 95887360 22098 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23410 22098 603 41 0 23369 0
vsize: 93640
[startup+589.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22780 0 0 0 58937 66 0 0 25 0 1 0 549034218 95887360 22099 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23410 22099 603 41 0 23369 0
vsize: 93640
[startup+599.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22807 0 0 0 59937 66 0 0 25 0 1 0 549034218 96022528 22126 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23443 22126 603 41 0 23402 0
vsize: 93772
[startup+609.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22851 0 0 0 60937 66 0 0 25 0 1 0 549034218 96292864 22170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23509 22170 603 41 0 23468 0
vsize: 94036
[startup+619.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22886 0 0 0 61937 66 0 0 25 0 1 0 549034218 96321536 22205 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23516 22205 603 41 0 23475 0
vsize: 94064
[startup+629.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22921 0 0 0 62937 66 0 0 25 0 1 0 549034218 96456704 22240 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23549 22240 603 41 0 23508 0
vsize: 94196
[startup+639.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22948 0 0 0 63937 67 0 0 25 0 1 0 549034218 96575488 22267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23578 22267 603 41 0 23537 0
vsize: 94312
[startup+649.997 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 22950 0 0 0 64937 67 0 0 25 0 1 0 549034218 96575488 22269 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23578 22269 603 41 0 23537 0
vsize: 94312
[startup+659.997 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23011 0 0 0 65936 67 0 0 25 0 1 0 549034218 97091584 22330 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23704 22330 603 41 0 23663 0
vsize: 94816
[startup+669.998 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23016 0 0 0 66936 67 0 0 25 0 1 0 549034218 97091584 22335 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23704 22335 603 41 0 23663 0
vsize: 94816
[startup+679.997 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23048 0 0 0 67936 67 0 0 25 0 1 0 549034218 97345536 22367 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23766 22367 603 41 0 23725 0
vsize: 95064
[startup+689.997 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23055 0 0 0 68937 68 0 0 25 0 1 0 549034218 97345536 22374 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23766 22374 603 41 0 23725 0
vsize: 95064
[startup+699.997 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23057 0 0 0 69937 68 0 0 25 0 1 0 549034218 97345536 22376 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23766 22376 603 41 0 23725 0
vsize: 95064
[startup+709.997 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23090 0 0 0 70936 68 0 0 25 0 1 0 549034218 97476608 22409 4294967295 134512640 134672761 3221224544 3221223728 134557999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23798 22409 603 41 0 23757 0
vsize: 95192
[startup+719.998 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23119 0 0 0 71937 68 0 0 25 0 1 0 549034218 97521664 22438 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22438 603 41 0 23768 0
vsize: 95236
[startup+729.997 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23119 0 0 0 72937 68 0 0 25 0 1 0 549034218 97521664 22438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22438 603 41 0 23768 0
vsize: 95236
[startup+739.997 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23119 0 0 0 73937 68 0 0 25 0 1 0 549034218 97521664 22438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22438 603 41 0 23768 0
vsize: 95236
[startup+749.997 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23120 0 0 0 74937 68 0 0 25 0 1 0 549034218 97521664 22439 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22439 603 41 0 23768 0
vsize: 95236
[startup+759.997 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23121 0 0 0 75937 68 0 0 25 0 1 0 549034218 97521664 22440 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22440 603 41 0 23768 0
vsize: 95236
[startup+769.997 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 23330 0 0 0 76937 69 0 0 25 0 1 0 549034218 98467840 22649 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24040 22649 603 41 0 23999 0
vsize: 96160
[startup+779.997 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26600 0 0 0 77928 77 0 0 25 0 1 0 549034218 129404928 25919 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31593 25919 603 41 0 31552 0
vsize: 126372
[startup+789.996 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 7242
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26612 0 0 0 78928 77 0 0 25 0 1 0 549034218 129540096 25931 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31626 25931 603 41 0 31585 0
vsize: 126504
[startup+799.995 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26673 0 0 0 79928 78 0 0 25 0 1 0 549034218 129675264 25992 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31659 25992 603 41 0 31618 0
vsize: 126636
[startup+809.996 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26694 0 0 0 80928 78 0 0 25 0 1 0 549034218 129814528 26013 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31693 26013 603 41 0 31652 0
vsize: 126772
[startup+819.996 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26769 0 0 0 81928 78 0 0 25 0 1 0 549034218 130084864 26088 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31759 26088 603 41 0 31718 0
vsize: 127036
[startup+829.995 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26835 0 0 0 82928 78 0 0 25 0 1 0 549034218 130355200 26154 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31825 26154 603 41 0 31784 0
vsize: 127300
[startup+839.995 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 26902 0 0 0 83928 78 0 0 25 0 1 0 549034218 130625536 26221 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31891 26221 603 41 0 31850 0
vsize: 127564
[startup+849.995 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27024 0 0 0 84928 79 0 0 25 0 1 0 549034218 131133440 26343 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32015 26343 603 41 0 31974 0
vsize: 128060
[startup+859.995 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27124 0 0 0 85928 79 0 0 25 0 1 0 549034218 131522560 26443 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32110 26443 603 41 0 32069 0
vsize: 128440
[startup+869.995 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27324 0 0 0 86928 80 0 0 25 0 1 0 549034218 132501504 26643 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32349 26643 603 41 0 32308 0
vsize: 129396
[startup+879.995 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27505 0 0 0 87927 80 0 0 25 0 1 0 549034218 133263360 26824 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32535 26824 603 41 0 32494 0
vsize: 130140
[startup+889.995 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27650 0 0 0 88927 81 0 0 25 0 1 0 549034218 133885952 26969 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32687 26969 603 41 0 32646 0
vsize: 130748
[startup+899.996 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27690 0 0 0 89927 81 0 0 25 0 1 0 549034218 134021120 27009 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32720 27009 603 41 0 32679 0
vsize: 130880
[startup+909.995 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27771 0 0 0 90927 81 0 0 25 0 1 0 549034218 134291456 27090 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32786 27090 603 41 0 32745 0
vsize: 131144
[startup+919.995 s]
Raw data (loadavg): 1.08 1.02 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 27912 0 0 0 91926 82 0 0 25 0 1 0 549034218 134963200 27231 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32950 27231 603 41 0 32909 0
vsize: 131800
[startup+929.995 s]
Raw data (loadavg): 1.06 1.02 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 28054 0 0 0 92926 82 0 0 25 0 1 0 549034218 135499776 27373 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33081 27373 603 41 0 33040 0
vsize: 132324
[startup+939.994 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 28354 0 0 0 93925 83 0 0 25 0 1 0 549034218 136695808 27673 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33373 27673 603 41 0 33332 0
vsize: 133492
[startup+949.995 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 28380 0 0 0 94925 83 0 0 25 0 1 0 549034218 136822784 27699 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33404 27699 603 41 0 33363 0
vsize: 133616
[startup+959.994 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 28466 0 0 0 95925 84 0 0 25 0 1 0 549034218 137093120 27785 4294967295 134512640 134672761 3221224544 3221223680 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33470 27785 603 41 0 33429 0
vsize: 133880
[startup+969.995 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34225 0 0 0 96913 96 0 0 25 0 1 0 549034218 153686016 32885 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37521 32885 603 41 0 37480 0
vsize: 150084
[startup+979.994 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34312 0 0 0 97913 96 0 0 25 0 1 0 549034218 153821184 32972 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37554 32972 603 41 0 37513 0
vsize: 150216
[startup+989.994 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34359 0 0 0 98913 97 0 0 25 0 1 0 549034218 154087424 33019 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37619 33019 603 41 0 37578 0
vsize: 150476
[startup+999.995 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34378 0 0 0 99913 97 0 0 25 0 1 0 549034218 154087424 33038 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37619 33038 603 41 0 37578 0
vsize: 150476
[startup+1009.99 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34444 0 0 0 100913 97 0 0 25 0 1 0 549034218 154353664 33104 4294967295 134512640 134672761 3221224544 3221223680 134560613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37684 33104 603 41 0 37643 0
vsize: 150736
[startup+1019.99 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34545 0 0 0 101912 98 0 0 25 0 1 0 549034218 154750976 33205 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37781 33205 603 41 0 37740 0
vsize: 151124
[startup+1029.99 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34582 0 0 0 102912 98 0 0 25 0 1 0 549034218 154882048 33242 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37813 33242 603 41 0 37772 0
vsize: 151252
[startup+1039.99 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34629 0 0 0 103912 98 0 0 25 0 1 0 549034218 155152384 33289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37879 33289 603 41 0 37838 0
vsize: 151516
[startup+1049.99 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34666 0 0 0 104912 98 0 0 25 0 1 0 549034218 155291648 33326 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37913 33326 603 41 0 37872 0
vsize: 151652
[startup+1059.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34694 0 0 0 105912 98 0 0 25 0 1 0 549034218 155426816 33354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37946 33355 603 41 0 37905 0
vsize: 151784
[startup+1069.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34749 0 0 0 106912 99 0 0 25 0 1 0 549034218 155561984 33409 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37979 33409 603 41 0 37938 0
vsize: 151916
[startup+1079.99 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 34973 0 0 0 107911 100 0 0 25 0 1 0 549034218 156491776 33633 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38206 33633 603 41 0 38165 0
vsize: 152824
[startup+1090 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7244
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35136 0 0 0 108911 100 0 0 25 0 1 0 549034218 157155328 33796 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38368 33796 603 41 0 38327 0
vsize: 153472
[startup+1100 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35247 0 0 0 109911 101 0 0 25 0 1 0 549034218 157278208 33907 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38398 33907 603 41 0 38357 0
vsize: 153592
[startup+1110 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35280 0 0 0 110911 101 0 0 25 0 1 0 549034218 157417472 33940 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38432 33940 603 41 0 38391 0
vsize: 153728
[startup+1120 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35297 0 0 0 111911 101 0 0 25 0 1 0 549034218 157552640 33957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38465 33957 603 41 0 38424 0
vsize: 153860
[startup+1130 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35312 0 0 0 112911 101 0 0 25 0 1 0 549034218 157552640 33972 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38465 33972 603 41 0 38424 0
vsize: 153860
[startup+1140 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35345 0 0 0 113911 101 0 0 25 0 1 0 549034218 157687808 34005 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38498 34005 603 41 0 38457 0
vsize: 153992
[startup+1150 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35419 0 0 0 114911 101 0 0 25 0 1 0 549034218 158085120 34079 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38595 34079 603 41 0 38554 0
vsize: 154380
[startup+1160 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35569 0 0 0 115911 102 0 0 25 0 1 0 549034218 158597120 34229 4294967295 134512640 134672761 3221224544 3221223844 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38720 34229 603 41 0 38679 0
vsize: 154880
[startup+1170 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35569 0 0 0 116911 102 0 0 25 0 1 0 549034218 158597120 34229 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38720 34229 603 41 0 38679 0
vsize: 154880
[startup+1180 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35581 0 0 0 117911 102 0 0 25 0 1 0 549034218 158728192 34241 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38752 34241 603 41 0 38711 0
vsize: 155008
[startup+1190 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35588 0 0 0 118911 102 0 0 25 0 1 0 549034218 158728192 34248 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38752 34248 603 41 0 38711 0
vsize: 155008
[startup+1200 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 7246
Raw data (stat): 7238 (minisat+) R 7237 20838 20837 0 -1 0 35600 0 0 0 119911 102 0 0 25 0 1 0 549034218 158728192 34260 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38752 34260 603 41 0 38711 0
vsize: 155008
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 7246
Raw data (stat): 7238 (minisat+) Z 7237 20838 20837 0 -1 12 35603 0 0 0 119911 109 0 0 25 0 1 0 549034218 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.21
CPU user time (s): 1199.12
CPU system time (s): 1.09383
CPU usage (%): 100.012
Max. virtual memory (Kb): 155008
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####