PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        741400 kB
Buffers:         22624 kB
Cached:         248220 kB
SwapCached:          0 kB
Active:          25084 kB
Inactive:       248568 kB
HighTotal:      131008 kB
HighFree:        88060 kB
LowTotal:       903652 kB
LowFree:        653340 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            13896 kB
Committed_AS:    71776 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:14:24 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 18446 7 1200.26 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.90 0.94 0.90 2/54 13032
Raw data (stat): 13032 (runsolver) R 13031 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487370817 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 9073 0 0 0 978 20 0 0 25 0 1 0 487370817 40308736 8722 4294967295 134512640 134672761 3221224544 3221223744 134557809 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.0019 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 14818 0 0 0 1965 33 0 0 25 0 1 0 487370817 67272704 14137 4294967295 134512640 134672761 3221224544 3221223680 134560650 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.0024 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 14848 0 0 0 2965 33 0 0 25 0 1 0 487370817 67272704 14167 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16424 14167 603 41 0 16383 0
vsize: 65696
[startup+40.0028 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 14898 0 0 0 3964 34 0 0 25 0 1 0 487370817 67538944 14217 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16489 14217 603 41 0 16448 0
vsize: 65956
[startup+50.0035 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 19627 0 0 0 4953 44 0 0 25 0 1 0 487370817 83431424 18946 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20369 18946 603 41 0 20328 0
vsize: 81476
[startup+60.004 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 19785 0 0 0 5952 45 0 0 25 0 1 0 487370817 83558400 19104 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20400 19104 603 41 0 20359 0
vsize: 81600
[startup+70.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 19796 0 0 0 6952 45 0 0 25 0 1 0 487370817 83607552 19115 4294967295 134512640 134672761 3221224544 3221223712 134561375 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.0049 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 19809 0 0 0 7952 46 0 0 25 0 1 0 487370817 83742720 19128 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20445 19128 603 41 0 20404 0
vsize: 81780
[startup+90.0044 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 19830 0 0 0 8952 46 0 0 25 0 1 0 487370817 83742720 19149 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 19843 0 0 0 9952 46 0 0 25 0 1 0 487370817 83873792 19162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20477 19162 603 41 0 20436 0
vsize: 81908
[startup+110.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 19879 0 0 0 10952 46 0 0 25 0 1 0 487370817 84045824 19198 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 19904 0 0 0 11952 46 0 0 25 0 1 0 487370817 84180992 19223 4294967295 134512640 134672761 3221224544 3221223692 1074754736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20552 19223 603 41 0 20511 0
vsize: 82208
[startup+130.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20053 0 0 0 12952 47 0 0 25 0 1 0 487370817 84721664 19372 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20684 19372 603 41 0 20643 0
vsize: 82736
[startup+140.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20317 0 0 0 13952 47 0 0 25 0 1 0 487370817 85852160 19636 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20960 19636 603 41 0 20919 0
vsize: 83840
[startup+150.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20462 0 0 0 14951 48 0 0 25 0 1 0 487370817 86540288 19781 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21128 19781 603 41 0 21087 0
vsize: 84512
[startup+160.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20548 0 0 0 15951 48 0 0 25 0 1 0 487370817 86794240 19867 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21190 19867 603 41 0 21149 0
vsize: 84760
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20548 0 0 0 16951 48 0 0 25 0 1 0 487370817 86794240 19867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21190 19867 603 41 0 21149 0
vsize: 84760
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20553 0 0 0 17951 48 0 0 25 0 1 0 487370817 86794240 19872 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21190 19872 603 41 0 21149 0
vsize: 84760
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20625 0 0 0 18951 48 0 0 25 0 1 0 487370817 87199744 19944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21289 19944 603 41 0 21248 0
vsize: 85156
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20674 0 0 0 19951 48 0 0 25 0 1 0 487370817 87293952 19993 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21312 19993 603 41 0 21271 0
vsize: 85248
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20675 0 0 0 20952 48 0 0 25 0 1 0 487370817 87293952 19994 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21312 19994 603 41 0 21271 0
vsize: 85248
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20697 0 0 0 21952 48 0 0 25 0 1 0 487370817 87429120 20016 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21345 20016 603 41 0 21304 0
vsize: 85380
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20745 0 0 0 22952 48 0 0 25 0 1 0 487370817 87564288 20064 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21378 20064 603 41 0 21337 0
vsize: 85512
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20783 0 0 0 23952 48 0 0 25 0 1 0 487370817 87834624 20102 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21444 20102 603 41 0 21403 0
vsize: 85776
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20793 0 0 0 24952 48 0 0 25 0 1 0 487370817 87834624 20112 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21444 20112 603 41 0 21403 0
vsize: 85776
[startup+260.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20812 0 0 0 25952 48 0 0 25 0 1 0 487370817 87834624 20131 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21444 20131 603 41 0 21403 0
vsize: 85776
[startup+270.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20856 0 0 0 26952 48 0 0 25 0 1 0 487370817 88018944 20175 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21489 20175 603 41 0 21448 0
vsize: 85956
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20856 0 0 0 27953 48 0 0 25 0 1 0 487370817 88018944 20175 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21489 20175 603 41 0 21448 0
vsize: 85956
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20878 0 0 0 28953 49 0 0 25 0 1 0 487370817 88150016 20197 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21521 20197 603 41 0 21480 0
vsize: 86084
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 20959 0 0 0 29952 49 0 0 25 0 1 0 487370817 88416256 20278 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21586 20278 603 41 0 21545 0
vsize: 86344
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21009 0 0 0 30952 49 0 0 25 0 1 0 487370817 88813568 20328 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21683 20328 603 41 0 21642 0
vsize: 86732
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21029 0 0 0 31953 49 0 0 25 0 1 0 487370817 88948736 20348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21716 20348 603 41 0 21675 0
vsize: 86864
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21072 0 0 0 32953 49 0 0 25 0 1 0 487370817 89083904 20391 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21749 20391 603 41 0 21708 0
vsize: 86996
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13032
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21174 0 0 0 33953 50 0 0 25 0 1 0 487370817 89485312 20493 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21847 20493 603 41 0 21806 0
vsize: 87388
[startup+350.012 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 13085
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21241 0 0 0 34952 50 0 0 25 0 1 0 487370817 89751552 20560 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21912 20560 603 41 0 21871 0
vsize: 87648
[startup+360.013 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 13085
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21270 0 0 0 35952 50 0 0 25 0 1 0 487370817 89808896 20589 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21926 20589 603 41 0 21885 0
vsize: 87704
[startup+370.013 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 13085
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21273 0 0 0 36952 50 0 0 25 0 1 0 487370817 89808896 20592 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21926 20592 603 41 0 21885 0
vsize: 87704
[startup+380.014 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 13085
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21365 0 0 0 37951 51 0 0 25 0 1 0 487370817 90210304 20684 4294967295 134512640 134672761 3221224544 3221223712 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22024 20684 603 41 0 21983 0
vsize: 88096
[startup+390.015 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 13085
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21492 0 0 0 38950 52 0 0 25 0 1 0 487370817 90701824 20811 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22144 20811 603 41 0 22103 0
vsize: 88576
[startup+400.015 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 13085
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21548 0 0 0 39950 53 0 0 25 0 1 0 487370817 90968064 20867 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22209 20867 603 41 0 22168 0
vsize: 88836
[startup+410.016 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 13085
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21684 0 0 0 40949 54 0 0 25 0 1 0 487370817 91504640 21003 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22340 21003 603 41 0 22299 0
vsize: 89360
[startup+420.015 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21804 0 0 0 41948 55 0 0 25 0 1 0 487370817 92041216 21123 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22471 21123 603 41 0 22430 0
vsize: 89884
[startup+430.016 s]
Raw data (loadavg): 1.09 1.01 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21857 0 0 0 42948 55 0 0 25 0 1 0 487370817 92176384 21176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22504 21176 603 41 0 22463 0
vsize: 90016
[startup+440.017 s]
Raw data (loadavg): 1.15 1.03 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 21995 0 0 0 43947 56 0 0 25 0 1 0 487370817 92712960 21314 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22635 21314 603 41 0 22594 0
vsize: 90540
[startup+450.017 s]
Raw data (loadavg): 1.13 1.03 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22135 0 0 0 44947 57 0 0 25 0 1 0 487370817 93384704 21454 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22799 21454 603 41 0 22758 0
vsize: 91196
[startup+460.019 s]
Raw data (loadavg): 1.11 1.03 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22163 0 0 0 45946 58 0 0 25 0 1 0 487370817 93409280 21482 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22805 21482 603 41 0 22764 0
vsize: 91220
[startup+470.023 s]
Raw data (loadavg): 1.09 1.03 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22164 0 0 0 46946 58 0 0 25 0 1 0 487370817 93409280 21483 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22805 21483 603 41 0 22764 0
vsize: 91220
[startup+480.023 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22187 0 0 0 47946 59 0 0 25 0 1 0 487370817 93540352 21506 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22837 21506 603 41 0 22796 0
vsize: 91348
[startup+490.023 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22265 0 0 0 48946 59 0 0 25 0 1 0 487370817 93814784 21584 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22904 21584 603 41 0 22863 0
vsize: 91616
[startup+500.024 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22353 0 0 0 49945 59 0 0 25 0 1 0 487370817 94224384 21672 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23004 21672 603 41 0 22963 0
vsize: 92016
[startup+510.025 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22403 0 0 0 50945 60 0 0 25 0 1 0 487370817 94371840 21722 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23040 21722 603 41 0 22999 0
vsize: 92160
[startup+520.025 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22409 0 0 0 51945 60 0 0 25 0 1 0 487370817 94507008 21728 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23073 21728 603 41 0 23032 0
vsize: 92292
[startup+530.026 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22446 0 0 0 52945 60 0 0 25 0 1 0 487370817 94638080 21765 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23105 21765 603 41 0 23064 0
vsize: 92420
[startup+540.026 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22456 0 0 0 53944 61 0 0 25 0 1 0 487370817 94638080 21775 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23105 21775 603 41 0 23064 0
vsize: 92420
[startup+550.026 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22478 0 0 0 54944 61 0 0 25 0 1 0 487370817 94769152 21797 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23137 21797 603 41 0 23096 0
vsize: 92548
[startup+560.027 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22507 0 0 0 55944 62 0 0 25 0 1 0 487370817 94904320 21826 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23170 21826 603 41 0 23129 0
vsize: 92680
[startup+570.028 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22743 0 0 0 56943 63 0 0 25 0 1 0 487370817 95752192 22062 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23377 22062 603 41 0 23336 0
vsize: 93508
[startup+580.029 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22755 0 0 0 57943 63 0 0 25 0 1 0 487370817 95887360 22074 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23410 22074 603 41 0 23369 0
vsize: 93640
[startup+590.029 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22780 0 0 0 58942 64 0 0 25 0 1 0 487370817 95887360 22099 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23410 22099 603 41 0 23369 0
vsize: 93640
[startup+600.028 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22806 0 0 0 59942 65 0 0 25 0 1 0 487370817 96022528 22125 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23443 22125 603 41 0 23402 0
vsize: 93772
[startup+610.029 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22846 0 0 0 60942 65 0 0 25 0 1 0 487370817 96157696 22165 4294967295 134512640 134672761 3221224544 3221223680 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23476 22165 603 41 0 23435 0
vsize: 93904
[startup+620.029 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22886 0 0 0 61941 65 0 0 25 0 1 0 487370817 96321536 22205 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23516 22205 603 41 0 23475 0
vsize: 94064
[startup+630.03 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22913 0 0 0 62941 66 0 0 25 0 1 0 487370817 96456704 22232 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23549 22232 603 41 0 23508 0
vsize: 94196
[startup+640.031 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22948 0 0 0 63941 66 0 0 25 0 1 0 487370817 96575488 22267 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23578 22267 603 41 0 23537 0
vsize: 94312
[startup+650.031 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 13087
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 22950 0 0 0 64941 66 0 0 25 0 1 0 487370817 96575488 22269 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23578 22269 603 41 0 23537 0
vsize: 94312
[startup+660.032 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23011 0 0 0 65941 67 0 0 25 0 1 0 487370817 96829440 22330 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23640 22330 603 41 0 23599 0
vsize: 94560
[startup+670.031 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23012 0 0 0 66941 67 0 0 25 0 1 0 487370817 97091584 22331 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23704 22331 603 41 0 23663 0
vsize: 94816
[startup+680.032 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23047 0 0 0 67941 67 0 0 25 0 1 0 487370817 97214464 22366 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23734 22366 603 41 0 23693 0
vsize: 94936
[startup+690.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23055 0 0 0 68941 67 0 0 25 0 1 0 487370817 97345536 22374 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23766 22374 603 41 0 23725 0
vsize: 95064
[startup+700.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23057 0 0 0 69941 67 0 0 25 0 1 0 487370817 97345536 22376 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23766 22376 603 41 0 23725 0
vsize: 95064
[startup+710.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23090 0 0 0 70941 67 0 0 25 0 1 0 487370817 97476608 22409 4294967295 134512640 134672761 3221224544 3221223668 134566128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23798 22409 603 41 0 23757 0
vsize: 95192
[startup+720.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23119 0 0 0 71941 67 0 0 25 0 1 0 487370817 97521664 22438 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22438 603 41 0 23768 0
vsize: 95236
[startup+730.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23119 0 0 0 72942 67 0 0 25 0 1 0 487370817 97521664 22438 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22438 603 41 0 23768 0
vsize: 95236
[startup+740.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23119 0 0 0 73942 67 0 0 25 0 1 0 487370817 97521664 22438 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22438 603 41 0 23768 0
vsize: 95236
[startup+750.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23120 0 0 0 74942 67 0 0 25 0 1 0 487370817 97521664 22439 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22439 603 41 0 23768 0
vsize: 95236
[startup+760.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23121 0 0 0 75942 67 0 0 25 0 1 0 487370817 97521664 22440 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23809 22440 603 41 0 23768 0
vsize: 95236
[startup+770.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 23507 0 0 0 76941 68 0 0 25 0 1 0 487370817 102019072 22826 4294967295 134512640 134672761 3221224544 3221221016 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24907 22827 603 41 0 24866 0
vsize: 99628
[startup+780.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 26600 0 0 0 77935 75 0 0 25 0 1 0 487370817 129404928 25919 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31593 25919 603 41 0 31552 0
vsize: 126372
[startup+790.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 26615 0 0 0 78935 75 0 0 25 0 1 0 487370817 129540096 25934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31626 25934 603 41 0 31585 0
vsize: 126504
[startup+800.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 26673 0 0 0 79935 75 0 0 25 0 1 0 487370817 129675264 25992 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31659 25992 603 41 0 31618 0
vsize: 126636
[startup+810.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 26703 0 0 0 80936 75 0 0 25 0 1 0 487370817 129814528 26022 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31693 26022 603 41 0 31652 0
vsize: 126772
[startup+820.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 26769 0 0 0 81936 75 0 0 25 0 1 0 487370817 130084864 26088 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31759 26088 603 41 0 31718 0
vsize: 127036
[startup+830.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 26841 0 0 0 82935 76 0 0 25 0 1 0 487370817 130355200 26160 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31825 26160 603 41 0 31784 0
vsize: 127300
[startup+840.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 26927 0 0 0 83935 76 0 0 25 0 1 0 487370817 130748416 26246 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31921 26246 603 41 0 31880 0
vsize: 127684
[startup+850.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 27039 0 0 0 84935 76 0 0 25 0 1 0 487370817 131268608 26358 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32048 26358 603 41 0 32007 0
vsize: 128192
[startup+860.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 27148 0 0 0 85935 77 0 0 25 0 1 0 487370817 131657728 26467 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32143 26467 603 41 0 32102 0
vsize: 128572
[startup+870.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 27358 0 0 0 86935 77 0 0 25 0 1 0 487370817 132624384 26677 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32379 26677 603 41 0 32338 0
vsize: 129516
[startup+880.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 27531 0 0 0 87935 77 0 0 25 0 1 0 487370817 133365760 26850 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32560 26850 603 41 0 32519 0
vsize: 130240
[startup+890.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 27673 0 0 0 88935 77 0 0 25 0 1 0 487370817 133885952 26992 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32687 26992 603 41 0 32646 0
vsize: 130748
[startup+900.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 27690 0 0 0 89935 77 0 0 25 0 1 0 487370817 134021120 27009 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32720 27009 603 41 0 32679 0
vsize: 130880
[startup+910.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 27813 0 0 0 90935 78 0 0 25 0 1 0 487370817 134561792 27132 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32852 27132 603 41 0 32811 0
vsize: 131408
[startup+920.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 27916 0 0 0 91935 78 0 0 25 0 1 0 487370817 134963200 27235 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32950 27235 603 41 0 32909 0
vsize: 131800
[startup+930.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 28137 0 0 0 92934 79 0 0 25 0 1 0 487370817 135766016 27456 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33146 27456 603 41 0 33105 0
vsize: 132584
[startup+940.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 28356 0 0 0 93934 79 0 0 25 0 1 0 487370817 136695808 27675 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33373 27675 603 41 0 33332 0
vsize: 133492
[startup+950.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 28388 0 0 0 94934 79 0 0 25 0 1 0 487370817 136822784 27707 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33404 27707 603 41 0 33363 0
vsize: 133616
[startup+960.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 28514 0 0 0 95933 80 0 0 25 0 1 0 487370817 137371648 27833 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33538 27833 603 41 0 33497 0
vsize: 134152
[startup+970.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34225 0 0 0 96921 93 0 0 25 0 1 0 487370817 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+980.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34323 0 0 0 97920 93 0 0 25 0 1 0 487370817 153956352 32983 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37587 32983 603 41 0 37546 0
vsize: 150348
[startup+990.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34365 0 0 0 98920 94 0 0 25 0 1 0 487370817 154087424 33025 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37619 33025 603 41 0 37578 0
vsize: 150476
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34429 0 0 0 99920 94 0 0 25 0 1 0 487370817 154353664 33089 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37684 33089 603 41 0 37643 0
vsize: 150736
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34498 0 0 0 100920 94 0 0 25 0 1 0 487370817 154619904 33158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37749 33158 603 41 0 37708 0
vsize: 150996
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34555 0 0 0 101920 94 0 0 25 0 1 0 487370817 154882048 33215 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37813 33215 603 41 0 37772 0
vsize: 151252
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34592 0 0 0 102920 94 0 0 25 0 1 0 487370817 155017216 33252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37846 33252 603 41 0 37805 0
vsize: 151384
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34640 0 0 0 103921 94 0 0 25 0 1 0 487370817 155152384 33300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37879 33300 603 41 0 37838 0
vsize: 151516
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34679 0 0 0 104921 94 0 0 25 0 1 0 487370817 155291648 33339 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37913 33339 603 41 0 37872 0
vsize: 151652
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34741 0 0 0 105921 95 0 0 25 0 1 0 487370817 155561984 33401 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37979 33401 603 41 0 37938 0
vsize: 151916
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 34829 0 0 0 106921 95 0 0 25 0 1 0 487370817 155963392 33489 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38077 33489 603 41 0 38036 0
vsize: 152308
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35040 0 0 0 107920 96 0 0 25 0 1 0 487370817 156762112 33700 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38272 33700 603 41 0 38231 0
vsize: 153088
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35242 0 0 0 108920 96 0 0 25 0 1 0 487370817 157278208 33902 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38398 33902 603 41 0 38357 0
vsize: 153592
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35269 0 0 0 109920 96 0 0 25 0 1 0 487370817 157417472 33929 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38432 33929 603 41 0 38391 0
vsize: 153728
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35290 0 0 0 110920 96 0 0 25 0 1 0 487370817 157552640 33950 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38465 33950 603 41 0 38424 0
vsize: 153860
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35303 0 0 0 111920 96 0 0 25 0 1 0 487370817 157552640 33963 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38465 33963 603 41 0 38424 0
vsize: 153860
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35327 0 0 0 112921 96 0 0 25 0 1 0 487370817 157687808 33987 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38498 33987 603 41 0 38457 0
vsize: 153992
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35352 0 0 0 113921 96 0 0 25 0 1 0 487370817 157818880 34012 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38530 34012 603 41 0 38489 0
vsize: 154120
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35518 0 0 0 114921 97 0 0 25 0 1 0 487370817 158494720 34178 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38695 34178 603 41 0 38654 0
vsize: 154780
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35569 0 0 0 115921 97 0 0 25 0 1 0 487370817 158597120 34229 4294967295 134512640 134672761 3221224544 3221223680 134560709 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.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35578 0 0 0 116921 97 0 0 25 0 1 0 487370817 158728192 34238 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38752 34238 603 41 0 38711 0
vsize: 155008
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35583 0 0 0 117921 97 0 0 25 0 1 0 487370817 158728192 34243 4294967295 134512640 134672761 3221224544 3221223728 134558690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38752 34243 603 41 0 38711 0
vsize: 155008
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35593 0 0 0 118921 97 0 0 25 0 1 0 487370817 158728192 34253 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38752 34253 603 41 0 38711 0
vsize: 155008
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 13089
Raw data (stat): 13032 (minisat+) R 13031 10720 10719 0 -1 0 35609 0 0 0 119921 97 0 0 25 0 1 0 487370817 158863360 34269 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38785 34269 603 41 0 38744 0
vsize: 155140
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 13089
Raw data (stat): 13032 (minisat+) Z 13031 10720 10719 0 -1 12 35612 0 0 0 119921 103 0 0 25 0 1 0 487370817 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.12
CPU time (s): 1200.26
CPU user time (s): 1199.22
CPU system time (s): 1.03984
CPU usage (%): 100.011
Max. virtual memory (Kb): 155140
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####