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/miplib/normalized-mps-v2-13-7-egout.opb
MD5SUM	46c4db5f8baf54496e00a723c85beb20
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	58880896
Optimality of the best value was proved	NO
Number of terms in the objective function	1095
Biggest coefficient in the objective function	533200896
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	14929722305
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	533200896
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	14929722305
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	1155
Total number of constraints	153
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	98
Minimum length of a constraint	1
Maximum length of a constraint	280
Trace number 19266

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        534256 kB
Buffers:         34856 kB
Cached:         444476 kB
SwapCached:          0 kB
Active:         165100 kB
Inactive:       317080 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        534004 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            12592 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:52:33 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 16793 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 115 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 113]---> Adder-cost: 273   maxlim: 13440   bits: 15/14
c ---[ 111]---> Adder-cost: 18   maxlim: 766   bits: 10/10
c ---[ 109]---> Adder-cost: 18   maxlim: 511   bits: 10/9
c ---[ 107]---> Adder-cost: 20   maxlim: 1150   bits: 11/11
c ---[ 105]---> Adder-cost: 40   maxlim: 2047   bits: 12/11
c ---[ 101]---> Adder-cost: 24   maxlim: 3455   bits: 13/12
c ---[  99]---> Adder-cost: 48   maxlim: 8190   bits: 14/13
c ---[  97]---> Adder-cost: 24   maxlim: 4095   bits: 13/12
c ---[  91]---> Adder-cost: 24   maxlim: 5374   bits: 13/13
c ---[  89]---> Adder-cost: 26   maxlim: 7679   bits: 14/13
c ---[  85]---> Adder-cost: 56   maxlim: 32638   bits: 16/15
c ---[  83]---> Adder-cost: 28   maxlim: 16383   bits: 15/14
c ---[  81]---> Adder-cost: 55   maxlim: 16383   bits: 15/14
c ---[  79]---> Adder-cost: 28   maxlim: 16127   bits: 15/14
c ---[  75]---> Adder-cost: 20   maxlim: 1150   bits: 11/11
c ---[  73]---> Adder-cost: 20   maxlim: 1023   bits: 11/10
c ---[  71]---> Adder-cost: 84   maxlim: 32766   bits: 16/15
c ---[  69]---> Adder-cost: 24   maxlim: 5758   bits: 13/13
c ---[  67]---> Adder-cost: 55   maxlim: 15103   bits: 15/14
c ---[  65]---> Adder-cost: 56   maxlim: 32766   bits: 16/15
c ---[  59]---> Adder-cost: 28   maxlim: 15743   bits: 15/14
c ---[  57]---> Adder-cost: 28   maxlim: 16383   bits: 15/14
c ---[  55]---> Adder-cost: 28   maxlim: 16383   bits: 15/14
c ---[  53]---> Adder-cost: 28   maxlim: 15743   bits: 15/14
c ---[  49]---> Adder-cost: 56   maxlim: 32126   bits: 16/15
c ---[  47]---> Adder-cost: 56   maxlim: 32126   bits: 16/15
c ---[  45]---> Adder-cost: 28   maxlim: 15615   bits: 15/14
c ---[  44]---> Adder-cost: 54   maxlim: 12774   bits: 15/14
c ---[  43]---> Adder-cost: 54   maxlim: 12774   bits: 15/14
c ---[  42]---> Adder-cost: 54   maxlim: 12774   bits: 15/14
c ---[  41]---> Adder-cost: 60   maxlim: 25574   bits: 16/15
c ---[  40]---> Adder-cost: 60   maxlim: 25574   bits: 16/15
c ---[  39]---> Adder-cost: 66   maxlim: 51174   bits: 17/16
c ---[  37]---> Adder-cost: 72   maxlim: 102374   bits: 18/17
c ---[  36]---> Adder-cost: 72   maxlim: 102374   bits: 18/17
c ---[  35]---> Adder-cost: 72   maxlim: 102374   bits: 18/17
c ---[  34]---> Adder-cost: 72   maxlim: 102374   bits: 18/17
c ---[  31]---> Adder-cost: 73   maxlim: 102374   bits: 18/17
c ---[  30]---> Adder-cost: 73   maxlim: 102374   bits: 18/17
c ---[  29]---> Adder-cost: 69   maxlim: 204774   bits: 19/18
c ---[  27]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[  26]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[  25]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[  24]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[  23]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[  21]---> Adder-cost: 60   maxlim: 25574   bits: 16/15
c ---[  20]---> Adder-cost: 60   maxlim: 25574   bits: 16/15
c ---[  19]---> Adder-cost: 60   maxlim: 25574   bits: 16/15
c ---[  18]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[  17]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[  16]---> Adder-cost: 72   maxlim: 102374   bits: 18/17
c ---[  15]---> Adder-cost: 72   maxlim: 102374   bits: 18/17
c ---[  14]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[  13]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[  12]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[   9]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[   8]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[   7]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[   6]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[   4]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[   3]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[   2]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[   1]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ---[   0]---> Adder-cost: 70   maxlim: 409574   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   22467    82185 |    7489       0        0     nan |  0.000 % |
c |       100 |   22467    82185 |    8237     100      612     6.1 | 32.527 % |
c |       250 |   22424    82046 |    9061     238     1509     6.3 | 32.650 % |
c |       475 |   22379    81884 |    9967     456     2736     6.0 | 32.668 % |
c |       812 |   22280    81548 |   10964     766     4633     6.0 | 32.827 % |
c |      1320 |   22187    81230 |   12061    1215     8382     6.9 | 32.968 % |
c |      2079 |   21836    80056 |   13267    1895    12590     6.6 | 33.675 % |
c |      3218 |   21427    78693 |   14593    2913    20246     7.0 | 34.488 % |
c ==============================================================================
c [1mFound solution: 97467556[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3348   maxlim: 115335013   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4114 |   44531   161415 |   14843    3705    26372     7.1 | 34.488 % |
c |      4214 |   44524   161392 |   16327    3802    27091     7.1 | 22.189 % |
c |      4364 |   44524   161392 |   17960    3952    28587     7.2 | 22.189 % |
c |      4589 |   44517   161369 |   19756    4174    31062     7.4 | 22.200 % |
c |      4928 |   44482   161254 |   21731    4494    35828     8.0 | 22.255 % |
c |      5434 |   44467   161205 |   23904    4998    42636     8.5 | 22.278 % |
c |      6194 |   44362   160860 |   26295    5729    51313     9.0 | 22.444 % |
c |      7333 |   44186   160255 |   28924    6807    71990    10.6 | 22.621 % |
c ==============================================================================
c [1mFound solution: 96510902[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1344   maxlim: 116291667   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7761 |   53522   193712 |   17840    7227    79776    11.0 | 22.621 % |
c |      7861 |   53515   193689 |   19624    7323    80665    11.0 | 19.863 % |
c ==============================================================================
c [1mFound solution: 96426928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 116375641   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7981 |   53527   193852 |   17842    7441    85115    11.4 | 19.863 % |
c |      8081 |   53471   193668 |   19626    7521    85891    11.4 | 19.990 % |
c ==============================================================================
c [1mFound solution: 92014075[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 120788494   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8204 |   53487   193905 |   17829    7639    87308    11.4 | 19.990 % |
c |      8306 |   53473   193859 |   19611    7730    88649    11.5 | 20.119 % |
c |      8457 |   53473   193859 |   21573    7881    96579    12.3 | 20.119 % |
c |      8683 |   53459   193813 |   23730    8101   100609    12.4 | 20.138 % |
c |      9020 |   53354   193440 |   26103    8417   103696    12.3 | 20.196 % |
c |      9526 |   53354   193440 |   28713    8923   258227    28.9 | 20.196 % |
c |     10285 |   52931   191934 |   31585    9606   325263    33.9 | 20.446 % |
c ==============================================================================
c [1mFound solution: 87131861[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1460   maxlim: 111455540   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10654 |   63084   228321 |   21028    9975   366046    36.7 | 20.446 % |
c |     10755 |   63075   228290 |   23130   10074   366792    36.4 | 18.034 % |
c |     10906 |   63075   228290 |   25443   10225   375520    36.7 | 18.034 % |
c ==============================================================================
c [1mFound solution: 86976496[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 111610905   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11063 |   63091   228459 |   21030   10382   378900    36.5 | 18.034 % |
c |     11164 |   63091   228459 |   23133   10483   381264    36.4 | 18.078 % |
c ==============================================================================
c [1mFound solution: 84349068[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 114238333   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11229 |   63113   228742 |   21037   10548   382808    36.3 | 18.078 % |
c |     11329 |   63113   228742 |   23140   10648   383629    36.0 | 18.168 % |
c |     11479 |   63113   228742 |   25454   10798   394926    36.6 | 18.168 % |
c |     11704 |   63113   228742 |   28000   11023   398051    36.1 | 18.168 % |
c ==============================================================================
c [1mFound solution: 79618346[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 118969055   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11763 |   63139   228958 |   21046   11082   398639    36.0 | 18.168 % |
c |     11865 |   63123   228808 |   23150   11183   402612    36.0 | 18.264 % |
c |     12016 |   63123   228808 |   25465   11334   403680    35.6 | 18.264 % |
c |     12241 |   63123   228808 |   28012   11559   408200    35.3 | 18.264 % |
c |     12578 |   63123   228808 |   30813   11896   414800    34.9 | 18.264 % |
c |     13084 |   63123   228808 |   33894   12402   472690    38.1 | 18.264 % |
c |     13843 |   63123   228808 |   37284   13161   504612    38.3 | 18.264 % |
c |     14982 |   63114   228781 |   41012   14299   557615    39.0 | 18.281 % |
c ==============================================================================
c [1mFound solution: 76149600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 872   maxlim: 114466985   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16312 |   68950   249569 |   22983   15614   838894    53.7 | 18.281 % |
c |     16414 |   68950   249569 |   25281   15716   840096    53.5 | 17.213 % |
c |     16564 |   68941   249538 |   27809   15862   862296    54.4 | 17.221 % |
c |     16790 |   68941   249538 |   30590   16088   868691    54.0 | 17.221 % |
c |     17127 |   68941   249538 |   33649   16425   910569    55.4 | 17.221 % |
c |     17634 |   68941   249538 |   37014   16932   941129    55.6 | 17.221 % |
c |     18393 |   68941   249538 |   40715   17691   963735    54.5 | 17.221 % |
c |     19532 |   68941   249538 |   44787   18830  1034066    54.9 | 17.221 % |
c |     21240 |   68941   249538 |   49266   20538  1146458    55.8 | 17.221 % |
c |     23805 |   68941   249538 |   54192   23103  1297072    56.1 | 17.221 % |
c ==============================================================================
c [1mFound solution: 75865461[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 966   maxlim: 114251412   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26082 |   75466   272970 |   25155   25352  1433956    56.6 | 17.221 % |
c ==============================================================================
c [1mFound solution: 74635816[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 115481057   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26152 |   75480   273161 |   25160   25422  1435034    56.4 | 17.221 % |
c |     26252 |   75480   273161 |   27676   25522  1437361    56.3 | 16.239 % |
c |     26404 |   75480   273161 |   30443   25674  1444076    56.2 | 16.239 % |
c |     26629 |   75480   273161 |   33487   25899  1485454    57.4 | 16.239 % |
c |     26967 |   75480   273161 |   36836   26237  1504506    57.3 | 16.239 % |
c |     27473 |   75480   273161 |   40520   26743  1545286    57.8 | 16.239 % |
c |     28232 |   75480   273161 |   44572   27502  1610441    58.6 | 16.239 % |
c |     29371 |   75480   273161 |   49029   28641  1855390    64.8 | 16.239 % |
c |     31079 |   75480   273161 |   53932   30349  1905757    62.8 | 16.239 % |
c |     33642 |   75480   273161 |   59325   32912  2126873    64.6 | 16.239 % |
c ==============================================================================
c [1mFound solution: 71500170[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 118616703   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36314 |   75501   273328 |   25167   35584  2351578    66.1 | 16.239 % |
c |     36415 |   75501   273328 |   27683   15544  1015262    65.3 | 16.292 % |
c |     36565 |   75501   273328 |   30452   15694  1042968    66.5 | 16.292 % |
c |     36791 |   75501   273328 |   33497   15920  1054060    66.2 | 16.292 % |
c |     37128 |   75501   273328 |   36847   16257  1063829    65.4 | 16.292 % |
c ==============================================================================
c [1mFound solution: 65100160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 125016713   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37197 |   75519   273532 |   25173   16326  1065440    65.3 | 16.292 % |
c |     37297 |   75519   273532 |   27690   16426  1068889    65.1 | 16.357 % |
c |     37447 |   75519   273532 |   30459   16576  1071624    64.6 | 16.357 % |
c |     37673 |   75519   273532 |   33505   16802  1085016    64.6 | 16.357 % |
c |     38010 |   75519   273532 |   36855   17139  1092493    63.7 | 16.357 % |
c |     38516 |   75519   273532 |   40541   17645  1107339    62.8 | 16.357 % |
c |     39275 |   75519   273532 |   44595   18404  1165640    63.3 | 16.357 % |
c |     40415 |   75519   273532 |   49055   19544  1368322    70.0 | 16.357 % |
c |     42124 |   75519   273532 |   53960   21253  1675072    78.8 | 16.357 % |
c |     44686 |   75519   273532 |   59356   23815  1981095    83.2 | 16.357 % |
c |     48530 |   75512   273509 |   65292   27654  2235610    80.8 | 16.364 % |
c |     54296 |   75512   273509 |   71821   33420  2505550    75.0 | 16.364 % |
c |     62946 |   75512   273509 |   79003   42070  3994922    95.0 | 16.364 % |
c |     75920 |   75512   273509 |   86904   55044  6638325   120.6 | 16.364 % |
c |     95382 |   75512   273509 |   95594   74506  9448885   126.8 | 16.364 % |
c ==============================================================================
c [1mFound solution: 64828960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 125287913   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108677 |   75534   273786 |   25178   87801 11140385   126.9 | 16.364 % |
c |    108777 |   75534   273786 |   27695   16195  1652220   102.0 | 16.439 % |
c |    108927 |   75534   273786 |   30465   16345  1688075   103.3 | 16.439 % |
c |    109153 |   75534   273786 |   33511   16571  1724222   104.1 | 16.439 % |
c |    109491 |   75534   273786 |   36863   16909  1735848   102.7 | 16.439 % |
c |    109998 |   75534   273786 |   40549   17416  1821230   104.6 | 16.439 % |
c |    110757 |   75527   273763 |   44604   18174  1862245   102.5 | 16.447 % |
c |    111896 |   75527   273763 |   49064   19313  2161674   111.9 | 16.447 % |
c |    113604 |   75521   273746 |   53971   21018  2223864   105.8 | 16.454 % |
c |    116167 |   75521   273746 |   59368   23581  2319493    98.4 | 16.454 % |
c |    120011 |   75521   273746 |   65305   27425  2447643    89.2 | 16.454 % |
c |    125777 |   75521   273746 |   71835   33191  2672940    80.5 | 16.454 % |
c |    134426 |   75512   273715 |   79019   41837  3093563    73.9 | 16.461 % |
c ==============================================================================
c [1mFound solution: 64582912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 125533961   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    142126 |   75531   273940 |   25177   49537  4004613    80.8 | 16.461 % |
c |    142227 |   75531   273940 |   27694   17117  1143357    66.8 | 16.525 % |
c |    142378 |   75531   273940 |   30464   17268  1157363    67.0 | 16.525 % |
c |    142604 |   75531   273940 |   33510   17494  1173318    67.1 | 16.525 % |
c |    142942 |   75531   273940 |   36861   17832  1178587    66.1 | 16.525 % |
c |    143448 |   75531   273940 |   40547   18338  1219944    66.5 | 16.525 % |
c |    144208 |   75531   273940 |   44602   19098  1241647    65.0 | 16.525 % |
c |    145349 |   75531   273940 |   49062   20239  1279863    63.2 | 16.525 % |
c |    147058 |   75531   273940 |   53969   21948  1344625    61.3 | 16.525 % |
c |    149620 |   75531   273940 |   59366   24510  1411212    57.6 | 16.525 % |
c |    153464 |   75531   273940 |   65302   28354  1547465    54.6 | 16.525 % |
c |    159230 |   75531   273940 |   71832   34120  1876076    55.0 | 16.525 % |
c |    167879 |   75531   273940 |   79016   42769  2197935    51.4 | 16.525 % |
c |    180854 |   75531   273940 |   86917   55744  2579250    46.3 | 16.525 % |
c |    200315 |   75531   273940 |   95609   75205  3508579    46.7 | 16.525 % |
c ==============================================================================
c [1mFound solution: 64520832[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 125596041   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    202605 |   75545   274100 |   25181   77495  3809240    49.2 | 16.525 % |
c |    202705 |   75545   274100 |   27699   18896   851906    45.1 | 16.566 % |
c |    202856 |   75545   274100 |   30469   19047   853269    44.8 | 16.566 % |
c |    203083 |   75545   274100 |   33515   19274   870645    45.2 | 16.566 % |
c |    203421 |   75545   274100 |   36867   19612   915198    46.7 | 16.566 % |
c |    203929 |   75545   274100 |   40554   20120   934482    46.4 | 16.566 % |
c |    204688 |   75545   274100 |   44609   20879   967556    46.3 | 16.566 % |
c |    205828 |   75545   274100 |   49070   22019  1007433    45.8 | 16.566 % |
c |    207536 |   75545   274100 |   53977   23727  1085461    45.7 | 16.566 % |
c |    210098 |   75545   274100 |   59375   26289  1209249    46.0 | 16.566 % |
c |    213945 |   75545   274100 |   65313   30136  1316655    43.7 | 16.566 % |
c |    219711 |   75545   274100 |   71844   35902  1523420    42.4 | 16.566 % |
c |    228361 |   75545   274100 |   79028   44552  1827438    41.0 | 16.566 % |
c |    241338 |   75545   274100 |   86931   57529  2542220    44.2 | 16.566 % |
c |    260801 |   75545   274100 |   95624   76992  3480828    45.2 | 16.566 % |
c |    289998 |   75545   274100 |  105187   27192   793784    29.2 | 16.566 % |
c |    333787 |   75538   274077 |  115706   70978  5835852    82.2 | 16.573 % |
c |    399471 |   75538   274077 |  127276   36899  1363048    36.9 | 16.573 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v I_0x2e_001_0x2e__0x2e__0x2e__bit0 -I_0x2e_001003_bit0 -I_0x2e_002003_bit0 -I_0x2e_002_0x2e__0x2e__0x2e__bit0 -I_0x2e_003005_bit0 I_0x2e_004005_bit0 -I_0x2e_004_0x2e__0x2e__0x2e__bit0 I_0x2e_005007_bit0 I_0x2e_006007_bit0 I_0x2e_007008_bit0 -I_0x2e_008_0x2e__0x2e__0x2e__bit0 I_0x2e_008009_bit0 I_0x2e_010012_bit0 I_0x2e_011012_bit0 -I_0x2e_012_0x2e__0x2e__0x2e__bit0 I_0x2e_012013_bit0 I_0x2e_013016_bit0 -I_0x2e_014015_bit0 I_0x2e_015016_bit0 I_0x2e_016_0x2e__0x2e__0x2e__bit0 -I_0x2e_016017_bit0 I_0x2e_017018_bit0 I_0x2e_009018_bit0 I_0x2e_018019_bit0 I_0x2e_019024_bit0 -I_0x2e_024_0x2e__0x2e__0x2e__bit0 -I_0x2e_023024_bit0 -I_0x2e_022023_bit0 -I_0x2e_020022_bit0 I_0x2e_021022_bit0 I_0x2e_022_0x2e__0x2e__0x2e__bit0 I_0x2e_024026_bit0 I_0x2e_025026_bit0 -I_0x2e_025_0x2e__0x2e__0x2e__bit0 I_0x2e_026027_bit0 I_0x2e_027_0x2e__0x2e__0x2e__bit0 I_0x2e_027032_bit0 -I_0x2e_030031_bit0 I_0x2e_031032_bit0 I_0x2e_029031_bit0 -I_0x2e_028029_bit0 -I_0x2e_028_0x2e__0x2e__0x2e__bit0 I_0x2e_032033_bit0 I_0x2e_033037_bit0 I_0x2e_036037_bit0 I_0x2e_034036_bit0 -I_0x2e_035036_bit0 I_0x2e_037038_bit0 I_0x2e_038040_bit0 I_0x2e_039040_bit0 -I_0x2e_040_0x2e__0x2e__0x2e__bit0 -I_0x2e_041_0x2e__0x2e__0x2e__bit0 I_0x2e_040041_bit0 I_0x2e_041042_bit0 I_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_001_0x2e__0x2e__0x2e__bit_7 -F_0x2e_001_0x2e__0x2e__0x2e__bit_6 -F_0x2e_001_0x2e__0x2e__0x2e__bit_5 -F_0x2e_001_0x2e__0x2e__0x2e__bit_4 -F_0x2e_001_0x2e__0x2e__0x2e__bit_3 -F_0x2e_001_0x2e__0x2e__0x2e__bit_2 -F_0x2e_001_0x2e__0x2e__0x2e__bit_1 -F_0x2e_001_0x2e__0x2e__0x2e__bit0 F_0x2e_001_0x2e__0x2e__0x2e__bit1 -F_0x2e_001_0x2e__0x2e__0x2e__bit2 -F_0x2e_001_0x2e__0x2e__0x2e__bit3 -F_0x2e_001_0x2e__0x2e__0x2e__bit4 -F_0x2e_001_0x2e__0x2e__0x2e__bit5 -F_0x2e_001_0x2e__0x2e__0x2e__bit6 -F_0x2e_001_0x2e__0x2e__0x2e__bit7 -F_0x2e_001_0x2e__0x2e__0x2e__bit8 -F_0x2e_001_0x2e__0x2e__0x2e__bit9 -F_0x2e_001_0x2e__0x2e__0x2e__bit10 -F_0x2e_001_0x2e__0x2e__0x2e__bit11 -F_0x2e_001_0x2e__0x2e__0x2e__bit12 -F_0x2e_001003_bit_7 -F_0x2e_001003_bit_6 -F_0x2e_001003_bit_5 -F_0x2e_001003_bit_4 -F_0x2e_001003_bit_3 -F_0x2e_001003_bit_2 -F_0x2e_001003_bit_1 -F_0x2e_001003_bit0 -F_0x2e_001003_bit1 -F_0x2e_001003_bit2 -F_0x2e_001003_bit3 -F_0x2e_001003_bit4 -F_0x2e_001003_bit5 -F_0x2e_001003_bit6 -F_0x2e_001003_bit7 -F_0x2e_001003_bit8 -F_0x2e_001003_bit9 -F_0x2e_001003_bit10 -F_0x2e_001003_bit11 -F_0x2e_001003_bit12 -F_0x2e_002003_bit_7 -F_0x2e_002003_bit_6 -F_0x2e_002003_bit_5 -F_0x2e_002003_bit_4 -F_0x2e_002003_bit_3 -F_0x2e_002003_bit_2 -F_0x2e_002003_bit_1 -F_0x2e_002003_bit0 -F_0x2e_002003_bit1 -F_0x2e_002003_bit2 -F_0x2e_002003_bit3 -F_0x2e_002003_bit4 -F_0x2e_002003_bit5 -F_0x2e_002003_bit6 -F_0x2e_002003_bit7 -F_0x2e_002003_bit8 -F_0x2e_002003_bit9 -F_0x2e_002003_bit10 -F_0x2e_002003_bit11 -F_0x2e_002003_bit12 -F_0x2e_002_0x2e__0x2e__0x2e__bit_7 -F_0x2e_002_0x2e__0x2e__0x2e__bit_6 -F_0x2e_002_0x2e__0x2e__0x2e__bit_5 -F_0x2e_002_0x2e__0x2e__0x2e__bit_4 -F_0x2e_002_0x2e__0x2e__0x2e__bit_3 -F_0x2e_002_0x2e__0x2e__0x2e__bit_2 -F_0x2e_002_0x2e__0x2e__0x2e__bit_1 -F_0x2e_002_0x2e__0x2e__0x2e__bit0 -F_0x2e_002_0x2e__0x2e__0x2e__bit1 -F_0x2e_002_0x2e__0x2e__0x2e__bit2 -F_0x2e_002_0x2e__0x2e__0x2e__bit3 -F_0x2e_002_0x2e__0x2e__0x2e__bit4 -F_0x2e_002_0x2e__0x2e__0x2e__bit5 -F_0x2e_002_0x2e__0x2e__0x2e__bit6 -F_0x2e_002_0x2e__0x2e__0x2e__bit7 -F_0x2e_002_0x2e__0x2e__0x2e__bit8 -F_0x2e_002_0x2e__0x2e__0x2e__bit9 -F_0x2e_002_0x2e__0x2e__0x2e__bit10 -F_0x2e_002_0x2e__0x2e__0x2e__bit11 -F_0x2e_002_0x2e__0x2e__0x2e__bit12 -F_0x2e_003005_bit_7 -F_0x2e_003005_bit_6 -F_0x2e_003005_bit_5 -F_0x2e_003005_bit_4 -F_0x2e_003005_bit_3 -F_0x2e_003005_bit_2 -F_0x2e_003005_bit_1 -F_0x2e_003005_bit0 -F_0x2e_003005_bit1 -F_0x2e_003005_bit2 -F_0x2e_003005_bit3 -F_0x2e_003005_bit4 -F_0x2e_003005_bit5 -F_0x2e_003005_bit6 -F_0x2e_003005_bit7 -F_0x2e_003005_bit8 -F_0x2e_003005_bit9 -F_0x2e_003005_bit10 -F_0x2e_003005_bit11 -F_0x2e_003005_bit12 -F_0x2e_004005_bit_7 -F_0x2e_004005_bit_6 -F_0x2e_004005_bit_5 -F_0x2e_004005_bit_4 -F_0x2e_004005_bit_3 -F_0x2e_004005_bit_2 -F_0x2e_004005_bit_1 F_0x2e_004005_bit0 F_0x2e_004005_bit1 F_0x2e_004005_bit2 -F_0x2e_004005_bit3 -F_0x2e_004005_bit4 -F_0x2e_004005_bit5 -F_0x2e_004005_bit6 -F_0x2e_004005_bit7 -F_0x2e_004005_bit8 -F_0x2e_004005_bit9 -F_0x2e_004005_bit10 -F_0x2e_004005_bit11 -F_0x2e_004005_bit12 -F_0x2e_004_0x2e__0x2e__0x2e__bit_7 -F_0x2e_004_0x2e__0x2e__0x2e__bit_6 -F_0x2e_004_0x2e__0x2e__0x2e__bit_5 -F_0x2e_004_0x2e__0x2e__0x2e__bit_4 -F_0x2e_004_0x2e__0x2e__0x2e__bit_3 -F_0x2e_004_0x2e__0x2e__0x2e__bit_2 -F_0x2e_004_0x2e__0x2e__0x2e__bit_1 -F_0x2e_004_0x2e__0x2e__0x2e__bit0 -F_0x2e_004_0x2e__0x2e__0x2e__bit1 -F_0x2e_004_0x2e__0x2e__0x2e__bit2 -F_0x2e_004_0x2e__0x2e__0x2e__bit3 -F_0x2e_004_0x2e__0x2e__0x2e__bit4 -F_0x2e_004_0x2e__0x2e__0x2e__bit5 -F_0x2e_004_0x2e__0x2e__0x2e__bit6 -F_0x2e_004_0x2e__0x2e__0x2e__bit7 -F_0x2e_004_0x2e__0x2e__0x2e__bit8 -F_0x2e_004_0x2e__0x2e__0x2e__bit9 -F_0x2e_004_0x2e__0x2e__0x2e__bit10 -F_0x2e_004_0x2e__0x2e__0x2e__bit11 -F_0x2e_004_0x2e__0x2e__0x2e__bit12 -F_0x2e_005007_bit_7 -F_0x2e_005007_bit_6 -F_0x2e_005007_bit_5 -F_0x2e_005007_bit_4 -F_0x2e_005007_bit_3 -F_0x2e_005007_bit_2 -F_0x2e_005007_bit_1 F_0x2e_005007_bit0 F_0x2e_005007_bit1 F_0x2e_005007_bit2 -F_0x2e_005007_bit3 -F_0x2e_005007_bit4 -F_0x2e_005007_bit5 -F_0x2e_005007_bit6 -F_0x2e_005007_bit7 -F_0x2e_005007_bit8 -F_0x2e_005007_bit9 -F_0x2e_005007_bit10 -F_0x2e_005007_bit11 -F_0x2e_005007_bit12 -F_0x2e_006007_bit_7 -F_0x2e_006007_bit_6 -F_0x2e_006007_bit_5 -F_0x2e_006007_bit_4 -F_0x2e_006007_bit_3 -F_0x2e_006007_bit_2 -F_0x2e_006007_bit_1 -F_0x2e_006007_bit0 -F_0x2e_006007_bit1 F_0x2e_006007_bit2 -F_0x2e_006007_bit3 -F_0x2e_006007_bit4 -F_0x2e_006007_bit5 -F_0x2e_006007_bit6 -F_0x2e_006007_bit7 -F_0x2e_006007_bit8 -F_0x2e_006007_bit9 -F_0x2e_006007_bit10 -F_0x2e_006007_bit11 -F_0x2e_006007_bit12 -F_0x2e_007008_bit_7 -F_0x2e_007008_bit_6 -F_0x2e_007008_bit_5 -F_0x2e_007008_bit_4 -F_0x2e_007008_bit_3 -F_0x2e_007008_bit_2 -F_0x2e_007008_bit_1 -F_0x2e_007008_bit0 -F_0x2e_007008_bit1 F_0x2e_007008_bit2 F_0x2e_007008_bit3 -F_0x2e_007008_bit4 -F_0x2e_007008_bit5 -F_0x2e_007008_bit6 -F_0x2e_007008_bit7 -F_0x2e_007008_bit8 -F_0x2e_007008_bit9 -F_0x2e_007008_bit10 -F_0x2e_007008_bit11 -F_0x2e_007008_bit12 -F_0x2e_008_0x2e__0x2e__0x2e__bit_7 -F_0x2e_008_0x2e__0x2e__0x2e__bit_6 -F_0x2e_008_0x2e__0x2e__0x2e__bit_5 -F_0x2e_008_0x2e__0x2e__0x2e__bit_4 -F_0x2e_008_0x2e__0x2e__0x2e__bit_3 -F_0x2e_008_0x2e__0x2e__0x2e__bit_2 -F_0x2e_008_0x2e__0x2e__0x2e__bit_1 -F_0x2e_008_0x2e__0x2e__0x2e__bit0 -F_0x2e_008_0x2e__0x2e__0x2e__bit1 -F_0x2e_008_0x2e__0x2e__0x2e__bit2 -F_0x2e_008_0x2e__0x2e__0x2e__bit3 -F_0x2e_008_0x2e__0x2e__0x2e__bit4 -F_0x2e_008_0x2e__0x2e__0x2e__bit5 -F_0x2e_008_0x2e__0x2e__0x2e__bit6 -F_0x2e_008_0x2e__0x2e__0x2e__bit7 -F_0x2e_008_0x2e__0x2e__0x2e__bit8 -F_0x2e_008_0x2e__0x2e__0x2e__bit9 -F_0x2e_008_0x2e__0x2e__0x2e__bit10 -F_0x2e_008_0x2e__0x2e__0x2e__bit11 -F_0x2e_008_0x2e__0x2e__0x2e__bit12 -F_0x2e_008009_bit_7 -F_0x2e_008009_bit_6 -F_0x2e_008009_bit_5 -F_0x2e_008009_bit_4 -F_0x2e_008009_bit_3 -F_0x2e_008009_bit_2 -F_0x2e_008009_bit_1 -F_0x2e_008009_bit0 -F_0x2e_008009_bit1 F_0x2e_008009_bit2 F_0x2e_008009_bit3 -F_0x2e_008009_bit4 -F_0x2e_008009_bit5 -F_0x2e_008009_bit6 -F_0x2e_008009_bit7 -F_0x2e_008009_bit8 -F_0x2e_008009_bit9 -F_0x2e_008009_bit10 -F_0x2e_008009_bit11 -F_0x2e_008009_bit12 -F_0x2e_010012_bit_7 -F_0x2e_010012_bit_6 -F_0x2e_010012_bit_5 -F_0x2e_010012_bit_4 -F_0x2e_010012_bit_3 -F_0x2e_010012_bit_2 -F_0x2e_010012_bit_1 F_0x2e_010012_bit0 -F_0x2e_010012_bit1 -F_0x2e_010012_bit2 -F_0x2e_010012_bit3 -F_0x2e_010012_bit4 -F_0x2e_010012_bit5 -F_0x2e_010012_bit6 -F_0x2e_010012_bit7 -F_0x2e_010012_bit8 -F_0x2e_010012_bit9 -F_0x2e_010012_bit10 -F_0x2e_010012_bit11 -F_0x2e_010012_bit12 -F_0x2e_012_0x2e__0x2e__0x2e__bit_7 -F_0x2e_012_0x2e__0x2e__0x2e__bit_6 -F_0x2e_012_0x2e__0x2e__0x2e__bit_5 -F_0x2e_012_0x2e__0x2e__0x2e__bit_4 -F_0x2e_012_0x2e__0x2e__0x2e__bit_3 -F_0x2e_012_0x2e__0x2e__0x2e__bit_2 -F_0x2e_012_0x2e__0x2e__0x2e__bit_1 -F_0x2e_012_0x2e__0x2e__0x2e__bit0 -F_0x2e_012_0x2e__0x2e__0x2e__bit1 -F_0x2e_012_0x2e__0x2e__0x2e__bit2 -F_0x2e_012_0x2e__0x2e__0x2e__bit3 -F_0x2e_012_0x2e__0x2e__0x2e__bit4 -F_0x2e_012_0x2e__0x2e__0x2e__bit5 -F_0x2e_012_0x2e__0x2e__0x2e__bit6 -F_0x2e_012_0x2e__0x2e__0x2e__bit7 -F_0x2e_012_0x2e__0x2e__0x2e__bit8 -F_0x2e_012_0x2e__0x2e__0x2e__bit9 -F_0x2e_012_0x2e__0x2e__0x2e__bit10 -F_0x2e_012_0x2e__0x2e__0x2e__bit11 -F_0x2e_012_0x2e__0x2e__0x2e__bit12 -F_0x2e_012013_bit_7 -F_0x2e_012013_bit_6 -F_0x2e_012013_bit_5 -F_0x2e_012013_bit_4 -F_0x2e_012013_bit_3 -F_0x2e_012013_bit_2 -F_0x2e_012013_bit_1 -F_0x2e_012013_bit0 F_0x2e_012013_bit1 F_0x2e_012013_bit2 -F_0x2e_012013_bit3 F_0x2e_012013_bit4 -F_0x2e_012013_bit5 -F_0x2e_012013_bit6 -F_0x2e_012013_bit7 -F_0x2e_012013_bit8 -F_0x2e_012013_bit9 -F_0x2e_012013_bit10 -F_0x2e_012013_bit11 -F_0x2e_012013_bit12 -F_0x2e_013016_bit_7 -F_0x2e_013016_bit_6 -F_0x2e_013016_bit_5 -F_0x2e_013016_bit_4 -F_0x2e_013016_bit_3 -F_0x2e_013016_bit_2 -F_0x2e_013016_bit_1 -F_0x2e_013016_bit0 F_0x2e_013016_bit1 -F_0x2e_013016_bit2 F_0x2e_013016_bit3 F_0x2e_013016_bit4 -F_0x2e_013016_bit5 -F_0x2e_013016_bit6 -F_0x2e_013016_bit7 -F_0x2e_013016_bit8 -F_0x2e_013016_bit9 -F_0x2e_013016_bit10 -F_0x2e_013016_bit11 -F_0x2e_013016_bit12 -F_0x2e_014015_bit_7 -F_0x2e_014015_bit_6 -F_0x2e_014015_bit_5 -F_0x2e_014015_bit_4 -F_0x2e_014015_bit_3 -F_0x2e_014015_bit_2 -F_0x2e_014015_bit_1 -F_0x2e_014015_bit0 -F_0x2e_014015_bit1 -F_0x2e_014015_bit2 -F_0x2e_014015_bit3 -F_0x2e_014015_bit4 -F_0x2e_014015_bit5 -F_0x2e_014015_bit6 -F_0x2e_014015_bit7 -F_0x2e_014015_bit8 -F_0x2e_014015_bit9 -F_0x2e_014015_bit10 -F_0x2e_014015_bit11 -F_0x2e_014015_bit12 -F_0x2e_015016_bit_7 -F_0x2e_015016_bit_6 -F_0x2e_015016_bit_5 -F_0x2e_015016_bit_4 -F_0x2e_015016_bit_3 -F_0x2e_015016_bit_2 -F_0x2e_015016_bit_1 F_0x2e_015016_bit0 -F_0x2e_015016_bit1 -F_0x2e_015016_bit2 -F_0x2e_015016_bit3 -F_0x2e_015016_bit4 -F_0x2e_015016_bit5 -F_0x2e_015016_bit6 -F_0x2e_015016_bit7 -F_0x2e_015016_bit8 -F_0x2e_015016_bit9 -F_0x2e_015016_bit10 -F_0x2e_015016_bit11 -F_0x2e_015016_bit12 -F_0x2e_016_0x2e__0x2e__0x2e__bit_7 -F_0x2e_016_0x2e__0x2e__0x2e__bit_6 -F_0x2e_016_0x2e__0x2e__0x2e__bit_5 -F_0x2e_016_0x2e__0x2e__0x2e__bit_4 -F_0x2e_016_0x2e__0x2e__0x2e__bit_3 -F_0x2e_016_0x2e__0x2e__0x2e__bit_2 -F_0x2e_016_0x2e__0x2e__0x2e__bit_1 F_0x2e_016_0x2e__0x2e__0x2e__bit0 F_0x2e_016_0x2e__0x2e__0x2e__bit1 -F_0x2e_016_0x2e__0x2e__0x2e__bit2 F_0x2e_016_0x2e__0x2e__0x2e__bit3 F_0x2e_016_0x2e__0x2e__0x2e__bit4 -F_0x2e_016_0x2e__0x2e__0x2e__bit5 -F_0x2e_016_0x2e__0x2e__0x2e__bit6 -F_0x2e_016_0x2e__0x2e__0x2e__bit7 -F_0x2e_016_0x2e__0x2e__0x2e__bit8 -F_0x2e_016_0x2e__0x2e__0x2e__bit9 -F_0x2e_016_0x2e__0x2e__0x2e__bit10 -F_0x2e_016_0x2e__0x2e__0x2e__bit11 -F_0x2e_016_0x2e__0x2e__0x2e__bit12 -F_0x2e_016017_bit_7 -F_0x2e_016017_bit_6 -F_0x2e_016017_bit_5 -F_0x2e_016017_bit_4 -F_0x2e_016017_bit_3 -F_0x2e_016017_bit_2 -F_0x2e_016017_bit_1 -F_0x2e_016017_bit0 -F_0x2e_016017_bit1 -F_0x2e_016017_bit2 -F_0x2e_016017_bit3 -F_0x2e_016017_bit4 -F_0x2e_016017_bit5 -F_0x2e_016017_bit6 -F_0x2e_016017_bit7 -F_0x2e_016017_bit8 -F_0x2e_016017_bit9 -F_0x2e_016017_bit10 -F_0x2e_016017_bit11 -F_0x2e_016017_bit12 -F_0x2e_017018_bit_7 -F_0x2e_017018_bit_6 -F_0x2e_017018_bit_5 -F_0x2e_017018_bit_4 -F_0x2e_017018_bit_3 -F_0x2e_017018_bit_2 -F_0x2e_017018_bit_1 -F_0x2e_017018_bit0 -F_0x2e_017018_bit1 -F_0x2e_017018_bit2 -F_0x2e_017018_bit3 -F_0x2e_017018_bit4 -F_0x2e_017018_bit5 -F_0x2e_017018_bit6 -F_0x2e_017018_bit7 -F_0x2e_017018_bit8 -F_0x2e_017018_bit9 -F_0x2e_017018_bit10 -F_0x2e_017018_bit11 -F_0x2e_017018_bit12 -F_0x2e_009018_bit_7 -F_0x2e_009018_bit_6 -F_0x2e_009018_bit_5 -F_0x2e_009018_bit_4 -F_0x2e_009018_bit_3 -F_0x2e_009018_bit_2 -F_0x2e_009018_bit_1 -F_0x2e_009018_bit0 -F_0x2e_009018_bit1 F_0x2e_009018_bit2 F_0x2e_009018_bit3 -F_0x2e_009018_bit4 -F_0x2e_009018_bit5 -F_0x2e_009018_bit6 -F_0x2e_009018_bit7 -F_0x2e_009018_bit8 -F_0x2e_009018_bit9 -F_0x2e_009018_bit10 -F_0x2e_009018_bit11 -F_0x2e_009018_bit12 -F_0x2e_018019_bit_7 -F_0x2e_018019_bit_6 -F_0x2e_018019_bit_5 -F_0x2e_018019_bit_4 -F_0x2e_018019_bit_3 -F_0x2e_018019_bit_2 -F_0x2e_018019_bit_1 -F_0x2e_018019_bit0 -F_0x2e_018019_bit1 F_0x2e_018019_bit2 F_0x2e_018019_bit3 -F_0x2e_018019_bit4 -F_0x2e_018019_bit5 -F_0x2e_018019_bit6 -F_0x2e_018019_bit7 -F_0x2e_018019_bit8 -F_0x2e_018019_bit9 -F_0x2e_018019_bit10 -F_0x2e_018019_bit11 -F_0x2e_018019_bit12 -F_0x2e_019024_bit_7 -F_0x2e_019024_bit_6 -F_0x2e_019024_bit_5 -F_0x2e_019024_bit_4 -F_0x2e_019024_bit_3 -F_0x2e_019024_bit_2 -F_0x2e_019024_bit_1 -F_0x2e_019024_bit0 F_0x2e_019024_bit1 F_0x2e_019024_bit2 F_0x2e_019024_bit3 -F_0x2e_019024_bit4 -F_0x2e_019024_bit5 -F_0x2e_019024_bit6 -F_0x2e_019024_bit7 -F_0x2e_019024_bit8 -F_0x2e_019024_bit9 -F_0x2e_019024_bit10 -F_0x2e_019024_bit11 -F_0x2e_019024_bit12 -F_0x2e_024_0x2e__0x2e__0x2e__bit_7 -F_0x2e_024_0x2e__0x2e__0x2e__bit_6 -F_0x2e_024_0x2e__0x2e__0x2e__bit_5 -F_0x2e_024_0x2e__0x2e__0x2e__bit_4 -F_0x2e_024_0x2e__0x2e__0x2e__bit_3 -F_0x2e_024_0x2e__0x2e__0x2e__bit_2 -F_0x2e_024_0x2e__0x2e__0x2e__bit_1 -F_0x2e_024_0x2e__0x2e__0x2e__bit0 -F_0x2e_024_0x2e__0x2e__0x2e__bit1 -F_0x2e_024_0x2e__0x2e__0x2e__bit2 -F_0x2e_024_0x2e__0x2e__0x2e__bit3 -F_0x2e_024_0x2e__0x2e__0x2e__bit4 -F_0x2e_024_0x2e__0x2e__0x2e__bit5 -F_0x2e_024_0x2e__0x2e__0x2e__bit6 -F_0x2e_024_0x2e__0x2e__0x2e__bit7 -F_0x2e_024_0x2e__0x2e__0x2e__bit8 -F_0x2e_024_0x2e__0x2e__0x2e__bit9 -F_0x2e_024_0x2e__0x2e__0x2e__bit10 -F_0x2e_024_0x2e__0x2e__0x2e__bit11 -F_0x2e_024_0x2e__0x2e__0x2e__bit12 -F_0x2e_023024_bit_7 -F_0x2e_023024_bit_6 -F_0x2e_023024_bit_5 -F_0x2e_023024_bit_4 -F_0x2e_023024_bit_3 -F_0x2e_023024_bit_2 -F_0x2e_023024_bit_1 -F_0x2e_023024_bit0 -F_0x2e_023024_bit1 -F_0x2e_023024_bit2 -F_0x2e_023024_bit3 -F_0x2e_023024_bit4 -F_0x2e_023024_bit5 -F_0x2e_023024_bit6 -F_0x2e_023024_bit7 -F_0x2e_023024_bit8 -F_0x2e_023024_bit9 -F_0x2e_023024_bit10 -F_0x2e_023024_bit11 -F_0x2e_023024_bit12 -F_0x2e_022023_bit_7 -F_0x2e_022023_bit_6 -F_0x2e_022023_bit_5 -F_0x2e_022023_bit_4 -F_0x2e_022023_bit_3 -F_0x2e_022023_bit_2 -F_0x2e_022023_bit_1 -F_0x2e_022023_bit0 -F_0x2e_022023_bit1 -F_0x2e_022023_bit2 -F_0x2e_022023_bit3 -F_0x2e_022023_bit4 -F_0x2e_022023_bit5 -F_0x2e_022023_bit6 -F_0x2e_022023_bit7 -F_0x2e_022023_bit8 -F_0x2e_022023_bit9 -F_0x2e_022023_bit10 -F_0x2e_022023_bit11 -F_0x2e_022023_bit12 -F_0x2e_020022_bit_7 -F_0x2e_020022_bit_6 -F_0x2e_020022_bit_5 -F_0x2e_020022_bit_4 -F_0x2e_020022_bit_3 -F_0x2e_020022_bit_2 -F_0x2e_020022_bit_1 -F_0x2e_020022_bit0 -F_0x2e_020022_bit1 -F_0x2e_020022_bit2 -F_0x2e_020022_bit3 -F_0x2e_020022_bit4 -F_0x2e_020022_bit5 -F_0x2e_020022_bit6 -F_0x2e_020022_bit7 -F_0x2e_020022_bit8 -F_0x2e_020022_bit9 -F_0x2e_020022_bit10 -F_0x2e_020022_bit11 -F_0x2e_020022_bit12 -F_0x2e_021022_bit_7 -F_0x2e_021022_bit_6 -F_0x2e_021022_bit_5 -F_0x2e_021022_bit_4 -F_0x2e_021022_bit_3 -F_0x2e_021022_bit_2 -F_0x2e_021022_bit_1 F_0x2e_021022_bit0 F_0x2e_021022_bit1 F_0x2e_021022_bit2 -F_0x2e_021022_bit3 -F_0x2e_021022_bit4 -F_0x2e_021022_bit5 -F_0x2e_021022_bit6 -F_0x2e_021022_bit7 -F_0x2e_021022_bit8 -F_0x2e_021022_bit9 -F_0x2e_021022_bit10 -F_0x2e_021022_bit11 -F_0x2e_021022_bit12 -F_0x2e_022_0x2e__0x2e__0x2e__bit_7 -F_0x2e_022_0x2e__0x2e__0x2e__bit_6 -F_0x2e_022_0x2e__0x2e__0x2e__bit_5 -F_0x2e_022_0x2e__0x2e__0x2e__bit_4 -F_0x2e_022_0x2e__0x2e__0x2e__bit_3 -F_0x2e_022_0x2e__0x2e__0x2e__bit_2 -F_0x2e_022_0x2e__0x2e__0x2e__bit_1 F_0x2e_022_0x2e__0x2e__0x2e__bit0 F_0x2e_022_0x2e__0x2e__0x2e__bit1 F_0x2e_022_0x2e__0x2e__0x2e__bit2 -F_0x2e_022_0x2e__0x2e__0x2e__bit3 -F_0x2e_022_0x2e__0x2e__0x2e__bit4 -F_0x2e_022_0x2e__0x2e__0x2e__bit5 -F_0x2e_022_0x2e__0x2e__0x2e__bit6 -F_0x2e_022_0x2e__0x2e__0x2e__bit7 -F_0x2e_022_0x2e__0x2e__0x2e__bit8 -F_0x2e_022_0x2e__0x2e__0x2e__bit9 -F_0x2e_022_0x2e__0x2e__0x2e__bit10 -F_0x2e_022_0x2e__0x2e__0x2e__bit11 -F_0x2e_022_0x2e__0x2e__0x2e__bit12 -F_0x2e_024026_bit_7 -F_0x2e_024026_bit_6 -F_0x2e_024026_bit_5 -F_0x2e_024026_bit_4 -F_0x2e_024026_bit_3 -F_0x2e_024026_bit_2 -F_0x2e_024026_bit_1 -F_0x2e_024026_bit0 F_0x2e_024026_bit1 F_0x2e_024026_bit2 F_0x2e_024026_bit3 -F_0x2e_024026_bit4 -F_0x2e_024026_bit5 -F_0x2e_024026_bit6 -F_0x2e_024026_bit7 -F_0x2e_024026_bit8 -F_0x2e_024026_bit9 -F_0x2e_024026_bit10 -F_0x2e_024026_bit11 -F_0x2e_024026_bit12 -F_0x2e_025026_bit_7 -F_0x2e_025026_bit_6 -F_0x2e_025026_bit_5 -F_0x2e_025026_bit_4 -F_0x2e_025026_bit_3 -F_0x2e_025026_bit_2 -F_0x2e_025026_bit_1 F_0x2e_025026_bit0 F_0x2e_025026_bit1 -F_0x2e_025026_bit2 -F_0x2e_025026_bit3 F_0x2e_025026_bit4 -F_0x2e_025026_bit5 -F_0x2e_025026_bit6 -F_0x2e_025026_bit7 -F_0x2e_025026_bit8 -F_0x2e_025026_bit9 -F_0x2e_025026_bit10 -F_0x2e_025026_bit11 -F_0x2e_025026_bit12 -F_0x2e_025_0x2e__0x2e__0x2e__bit_7 -F_0x2e_025_0x2e__0x2e__0x2e__bit_6 -F_0x2e_025_0x2e__0x2e__0x2e__bit_5 -F_0x2e_025_0x2e__0x2e__0x2e__bit_4 -F_0x2e_025_0x2e__0x2e__0x2e__bit_3 -F_0x2e_025_0x2e__0x2e__0x2e__bit_2 -F_0x2e_025_0x2e__0x2e__0x2e__bit_1 -F_0x2e_025_0x2e__0x2e__0x2e__bit0 -F_0x2e_025_0x2e__0x2e__0x2e__bit1 -F_0x2e_025_0x2e__0x2e__0x2e__bit2 -F_0x2e_025_0x2e__0x2e__0x2e__bit3 -F_0x2e_025_0x2e__0x2e__0x2e__bit4 -F_0x2e_025_0x2e__0x2e__0x2e__bit5 -F_0x2e_025_0x2e__0x2e__0x2e__bit6 -F_0x2e_025_0x2e__0x2e__0x2e__bit7 -F_0x2e_025_0x2e__0x2e__0x2e__bit8 -F_0x2e_025_0x2e__0x2e__0x2e__bit9 -F_0x2e_025_0x2e__0x2e__0x2e__bit10 -F_0x2e_025_0x2e__0x2e__0x2e__bit11 -F_0x2e_025_0x2e__0x2e__0x2e__bit12 -F_0x2e_026027_bit_7 -F_0x2e_026027_bit_6 -F_0x2e_026027_bit_5 -F_0x2e_026027_bit_4 -F_0x2e_026027_bit_3 -F_0x2e_026027_bit_2 -F_0x2e_026027_bit_1 F_0x2e_026027_bit0 F_0x2e_026027_bit1 -F_0x2e_026027_bit2 F_0x2e_026027_bit3 -F_0x2e_026027_bit4 F_0x2e_026027_bit5 -F_0x2e_026027_bit6 -F_0x2e_026027_bit7 -F_0x2e_026027_bit8 -F_0x2e_026027_bit9 -F_0x2e_026027_bit10 -F_0x2e_026027_bit11 -F_0x2e_026027_bit12 -F_0x2e_027_0x2e__0x2e__0x2e__bit_7 -F_0x2e_027_0x2e__0x2e__0x2e__bit_6 F_0x2e_027_0x2e__0x2e__0x2e__bit_5 -F_0x2e_027_0x2e__0x2e__0x2e__bit_4 -F_0x2e_027_0x2e__0x2e__0x2e__bit_3 -F_0x2e_027_0x2e__0x2e__0x2e__bit_2 F_0x2e_027_0x2e__0x2e__0x2e__bit_1 F_0x2e_027_0x2e__0x2e__0x2e__bit0 -F_0x2e_027_0x2e__0x2e__0x2e__bit1 -F_0x2e_027_0x2e__0x2e__0x2e__bit2 F_0x2e_027_0x2e__0x2e__0x2e__bit3 -F_0x2e_027_0x2e__0x2e__0x2e__bit4 F_0x2e_027_0x2e__0x2e__0x2e__bit5 -F_0x2e_027_0x2e__0x2e__0x2e__bit6 -F_0x2e_027_0x2e__0x2e__0x2e__bit7 -F_0x2e_027_0x2e__0x2e__0x2e__bit8 -F_0x2e_027_0x2e__0x2e__0x2e__bit9 -F_0x2e_027_0x2e__0x2e__0x2e__bit10 -F_0x2e_027_0x2e__0x2e__0x2e__bit11 -F_0x2e_027_0x2e__0x2e__0x2e__bit12 -F_0x2e_027032_bit_7 -F_0x2e_027032_bit_6 F_0x2e_027032_bit_5 F_0x2e_027032_bit_4 F_0x2e_027032_bit_3 F_0x2e_027032_bit_2 -F_0x2e_027032_bit_1 F_0x2e_027032_bit0 -F_0x2e_027032_bit1 -F_0x2e_027032_bit2 -F_0x2e_027032_bit3 -F_0x2e_027032_bit4 -F_0x2e_027032_bit5 -F_0x2e_027032_bit6 -F_0x2e_027032_bit7 -F_0x2e_027032_bit8 -F_0x2e_027032_bit9 -F_0x2e_027032_bit10 -F_0x2e_027032_bit11 -F_0x2e_027032_bit12 -F_0x2e_030031_bit_7 -F_0x2e_030031_bit_6 -F_0x2e_030031_bit_5 -F_0x2e_030031_bit_4 -F_0x2e_030031_bit_3 -F_0x2e_030031_bit_2 -F_0x2e_030031_bit_1 -F_0x2e_030031_bit0 -F_0x2e_030031_bit1 -F_0x2e_030031_bit2 -F_0x2e_030031_bit3 -F_0x2e_030031_bit4 -F_0x2e_030031_bit5 -F_0x2e_030031_bit6 -F_0x2e_030031_bit7 -F_0x2e_030031_bit8 -F_0x2e_030031_bit9 -F_0x2e_030031_bit10 -F_0x2e_030031_bit11 -F_0x2e_030031_bit12 -F_0x2e_031032_bit_7 -F_0x2e_031032_bit_6 -F_0x2e_031032_bit_5 -F_0x2e_031032_bit_4 -F_0x2e_031032_bit_3 -F_0x2e_031032_bit_2 -F_0x2e_031032_bit_1 F_0x2e_031032_bit0 -F_0x2e_031032_bit1 F_0x2e_031032_bit2 -F_0x2e_031032_bit3 -F_0x2e_031032_bit4 -F_0x2e_031032_bit5 -F_0x2e_031032_bit6 -F_0x2e_031032_bit7 -F_0x2e_031032_bit8 -F_0x2e_031032_bit9 -F_0x2e_031032_bit10 -F_0x2e_031032_bit11 -F_0x2e_031032_bit12 -F_0x2e_029031_bit_7 -F_0x2e_029031_bit_6 -F_0x2e_029031_bit_5 -F_0x2e_029031_bit_4 -F_0x2e_029031_bit_3 -F_0x2e_029031_bit_2 -F_0x2e_029031_bit_1 F_0x2e_029031_bit0 -F_0x2e_029031_bit1 F_0x2e_029031_bit2 -F_0x2e_029031_bit3 -F_0x2e_029031_bit4 -F_0x2e_029031_bit5 -F_0x2e_029031_bit6 -F_0x2e_029031_bit7 -F_0x2e_029031_bit8 -F_0x2e_029031_bit9 -F_0x2e_029031_bit10 -F_0x2e_029031_bit11 -F_0x2e_029031_bit12 -F_0x2e_028029_bit_7 -F_0x2e_028029_bit_6 -F_0x2e_028029_bit_5 -F_0x2e_028029_bit_4 -F_0x2e_028029_bit_3 -F_0x2e_028029_bit_2 -F_0x2e_028029_bit_1 -F_0x2e_028029_bit0 -F_0x2e_028029_bit1 -F_0x2e_028029_bit2 -F_0x2e_028029_bit3 -F_0x2e_028029_bit4 -F_0x2e_028029_bit5 -F_0x2e_028029_bit6 -F_0x2e_028029_bit7 -F_0x2e_028029_bit8 -F_0x2e_028029_bit9 -F_0x2e_028029_bit10 -F_0x2e_028029_bit11 -F_0x2e_028029_bit12 -F_0x2e_028_0x2e__0x2e__0x2e__bit_7 -F_0x2e_028_0x2e__0x2e__0x2e__bit_6 -F_0x2e_028_0x2e__0x2e__0x2e__bit_5 -F_0x2e_028_0x2e__0x2e__0x2e__bit_4 -F_0x2e_028_0x2e__0x2e__0x2e__bit_3 -F_0x2e_028_0x2e__0x2e__0x2e__bit_2 -F_0x2e_028_0x2e__0x2e__0x2e__bit_1 -F_0x2e_028_0x2e__0x2e__0x2e__bit0 -F_0x2e_028_0x2e__0x2e__0x2e__bit1 -F_0x2e_028_0x2e__0x2e__0x2e__bit2 -F_0x2e_028_0x2e__0x2e__0x2e__bit3 -F_0x2e_028_0x2e__0x2e__0x2e__bit4 -F_0x2e_028_0x2e__0x2e__0x2e__bit5 -F_0x2e_028_0x2e__0x2e__0x2e__bit6 -F_0x2e_028_0x2e__0x2e__0x2e__bit7 -F_0x2e_028_0x2e__0x2e__0x2e__bit8 -F_0x2e_028_0x2e__0x2e__0x2e__bit9 -F_0x2e_028_0x2e__0x2e__0x2e__bit10 -F_0x2e_028_0x2e__0x2e__0x2e__bit11 -F_0x2e_028_0x2e__0x2e__0x2e__bit12 -F_0x2e_032033_bit_7 -F_0x2e_032033_bit_6 F_0x2e_032033_bit_5 F_0x2e_032033_bit_4 F_0x2e_032033_bit_3 F_0x2e_032033_bit_2 -F_0x2e_032033_bit_1 -F_0x2e_032033_bit0 F_0x2e_032033_bit1 F_0x2e_032033_bit2 -F_0x2e_032033_bit3 -F_0x2e_032033_bit4 -F_0x2e_032033_bit5 -F_0x2e_032033_bit6 -F_0x2e_032033_bit7 -F_0x2e_032033_bit8 -F_0x2e_032033_bit9 -F_0x2e_032033_bit10 -F_0x2e_032033_bit11 -F_0x2e_032033_bit12 -F_0x2e_033037_bit_7 -F_0x2e_033037_bit_6 F_0x2e_033037_bit_5 F_0x2e_033037_bit_4 F_0x2e_033037_bit_3 F_0x2e_033037_bit_2 -F_0x2e_033037_bit_1 -F_0x2e_033037_bit0 F_0x2e_033037_bit1 F_0x2e_033037_bit2 -F_0x2e_033037_bit3 -F_0x2e_033037_bit4 -F_0x2e_033037_bit5 -F_0x2e_033037_bit6 -F_0x2e_033037_bit7 -F_0x2e_033037_bit8 -F_0x2e_033037_bit9 -F_0x2e_033037_bit10 -F_0x2e_033037_bit11 -F_0x2e_033037_bit12 -F_0x2e_034036_bit_7 -F_0x2e_034036_bit_6 -F_0x2e_034036_bit_5 -F_0x2e_034036_bit_4 -F_0x2e_034036_bit_3 -F_0x2e_034036_bit_2 -F_0x2e_034036_bit_1 -F_0x2e_034036_bit0 -F_0x2e_034036_bit1 -F_0x2e_034036_bit2 -F_0x2e_034036_bit3 -F_0x2e_034036_bit4 -F_0x2e_034036_bit5 -F_0x2e_034036_bit6 -F_0x2e_034036_bit7 -F_0x2e_034036_bit8 -F_0x2e_034036_bit9 -F_0x2e_034036_bit10 -F_0x2e_034036_bit11 -F_0x2e_034036_bit12 -F_0x2e_035036_bit_7 -F_0x2e_035036_bit_6 -F_0x2e_035036_bit_5 -F_0x2e_035036_bit_4 -F_0x2e_035036_bit_3 -F_0x2e_035036_bit_2 -F_0x2e_035036_bit_1 -F_0x2e_035036_bit0 -F_0x2e_035036_bit1 -F_0x2e_035036_bit2 -F_0x2e_035036_bit3 -F_0x2e_035036_bit4 -F_0x2e_035036_bit5 -F_0x2e_035036_bit6 -F_0x2e_035036_bit7 -F_0x2e_035036_bit8 -F_0x2e_035036_bit9 -F_0x2e_035036_bit10 -F_0x2e_035036_bit11 -F_0x2e_035036_bit12 -F_0x2e_037038_bit_7 -F_0x2e_037038_bit_6 F_0x2e_037038_bit_5 F_0x2e_037038_bit_4 F_0x2e_037038_bit_3 F_0x2e_037038_bit_2 -F_0x2e_037038_bit_1 -F_0x2e_037038_bit0 F_0x2e_037038_bit1 F_0x2e_037038_bit2 -F_0x2e_037038_bit3 -F_0x2e_037038_bit4 -F_0x2e_037038_bit5 -F_0x2e_037038_bit6 -F_0x2e_037038_bit7 -F_0x2e_037038_bit8 -F_0x2e_037038_bit9 -F_0x2e_037038_bit10 -F_0x2e_037038_bit11 -F_0x2e_037038_bit12 -F_0x2e_039040_bit_7 -F_0x2e_039040_bit_6 -F_0x2e_039040_bit_5 -F_0x2e_039040_bit_4 -F_0x2e_039040_bit_3 -F_0x2e_039040_bit_2 -F_0x2e_039040_bit_1 F_0x2e_039040_bit0 -F_0x2e_039040_bit1 F_0x2e_039040_bit2 -F_0x2e_039040_bit3 -F_0x2e_039040_bit4 -F_0x2e_039040_bit5 -F_0x2e_039040_bit6 -F_0x2e_039040_bit7 -F_0x2e_039040_bit8 -F_0x2e_039040_bit9 -F_0x2e_039040_bit10 -F_0x2e_039040_bit11 -F_0x2e_039040_bit12 -F_0x2e_040_0x2e__0x2e__0x2e__bit_7 -F_0x2e_040_0x2e__0x2e__0x2e__bit_6 -F_0x2e_040_0x2e__0x2e__0x2e__bit_5 -F_0x2e_040_0x2e__0x2e__0x2e__bit_4 -F_0x2e_040_0x2e__0x2e__0x2e__bit_3 -F_0x2e_040_0x2e__0x2e__0x2e__bit_2 -F_0x2e_040_0x2e__0x2e__0x2e__bit_1 -F_0x2e_040_0x2e__0x2e__0x2e__bit0 -F_0x2e_040_0x2e__0x2e__0x2e__bit1 -F_0x2e_040_0x2e__0x2e__0x2e__bit2 -F_0x2e_040_0x2e__0x2e__0x2e__bit3 -F_0x2e_040_0x2e__0x2e__0x2e__bit4 -F_0x2e_040_0x2e__0x2e__0x2e__bit5 -F_0x2e_040_0x2e__0x2e__0x2e__bit6 -F_0x2e_040_0x2e__0x2e__0x2e__bit7 -F_0x2e_040_0x2e__0x2e__0x2e__bit8 -F_0x2e_040_0x2e__0x2e__0x2e__bit9 -F_0x2e_040_0x2e__0x2e__0x2e__bit10 -F_0x2e_040_0x2e__0x2e__0x2e__bit11 -F_0x2e_040_0x2e__0x2e__0x2e__bit12 -F_0x2e_041_0x2e__0x2e__0x2e__bit_7 -F_0x2e_041_0x2e__0x2e__0x#### 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.97 0.97 0.95 2/54 7241
Raw data (stat): 7241 (runsolver) R 7240 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489041849 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.0003 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 1930 0 0 0 993 5 0 0 25 0 1 0 489041849 10010624 1900 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2444 1900 603 41 0 2403 0
vsize: 9776
[startup+20.0015 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 2657 0 0 0 1992 6 0 0 25 0 1 0 489041849 12636160 2585 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3085 2585 603 41 0 3044 0
vsize: 12340
[startup+30.0022 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 3389 0 0 0 2989 8 0 0 25 0 1 0 489041849 15863808 3317 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3873 3317 603 41 0 3832 0
vsize: 15492
[startup+40.0025 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 3962 0 0 0 3986 11 0 0 25 0 1 0 489041849 18153472 3890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4432 3890 603 41 0 4391 0
vsize: 17728
[startup+50.0025 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 4593 0 0 0 4984 13 0 0 25 0 1 0 489041849 20836352 4521 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5087 4521 603 41 0 5046 0
vsize: 20348
[startup+60.0036 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 4655 0 0 0 5984 13 0 0 25 0 1 0 489041849 20971520 4583 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5120 4583 603 41 0 5079 0
vsize: 20480
[startup+70.0038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 4655 0 0 0 6984 13 0 0 25 0 1 0 489041849 20971520 4583 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5120 4583 603 41 0 5079 0
vsize: 20480
[startup+80.0049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 4787 0 0 0 7984 13 0 0 25 0 1 0 489041849 21635072 4715 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5282 4715 603 41 0 5241 0
vsize: 21128
[startup+90.0047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 5316 0 0 0 8982 15 0 0 25 0 1 0 489041849 23781376 5244 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5806 5244 603 41 0 5765 0
vsize: 23224
[startup+100.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 5773 0 0 0 9981 17 0 0 25 0 1 0 489041849 25534464 5701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6234 5701 603 41 0 6193 0
vsize: 24936
[startup+110.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 6196 0 0 0 10980 18 0 0 25 0 1 0 489041849 27262976 6124 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6656 6124 603 41 0 6615 0
vsize: 26624
[startup+120.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 6642 0 0 0 11979 20 0 0 25 0 1 0 489041849 29155328 6570 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7118 6570 603 41 0 7077 0
vsize: 28472
[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 7042 0 0 0 12978 20 0 0 25 0 1 0 489041849 30740480 6970 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7505 6970 603 41 0 7464 0
vsize: 30020
[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 7439 0 0 0 13977 22 0 0 25 0 1 0 489041849 32342016 7367 4294967295 134512640 134672761 3221224544 3221223728 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7896 7367 603 41 0 7855 0
vsize: 31584
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 7977 0 0 0 14975 24 0 0 25 0 1 0 489041849 34631680 7905 4294967295 134512640 134672761 3221224544 3221223560 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8455 7905 603 41 0 8414 0
vsize: 33820
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 8580 0 0 0 15973 26 0 0 25 0 1 0 489041849 37044224 8508 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9044 8508 603 41 0 9003 0
vsize: 36176
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 9112 0 0 0 16972 27 0 0 25 0 1 0 489041849 39186432 9040 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9567 9040 603 41 0 9526 0
vsize: 38268
[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 9556 0 0 0 17971 29 0 0 25 0 1 0 489041849 41062400 9484 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10025 9484 603 41 0 9984 0
vsize: 40100
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 9983 0 0 0 18970 30 0 0 25 0 1 0 489041849 42807296 9911 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10451 9911 603 41 0 10410 0
vsize: 41804
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 10423 0 0 0 19969 31 0 0 25 0 1 0 489041849 44548096 10351 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10876 10351 603 41 0 10835 0
vsize: 43504
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 10853 0 0 0 20968 32 0 0 25 0 1 0 489041849 46284800 10781 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11300 10781 603 41 0 11259 0
vsize: 45200
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 11204 0 0 0 21967 33 0 0 25 0 1 0 489041849 47759360 11132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11660 11132 603 41 0 11619 0
vsize: 46640
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 11691 0 0 0 22966 34 0 0 25 0 1 0 489041849 50040832 11619 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11619 603 41 0 12176 0
vsize: 48868
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 12066 0 0 0 23965 35 0 0 25 0 1 0 489041849 51515392 11994 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12577 11994 603 41 0 12536 0
vsize: 50308
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 12500 0 0 0 24965 36 0 0 25 0 1 0 489041849 53268480 12428 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13005 12428 603 41 0 12964 0
vsize: 52020
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 12889 0 0 0 25964 37 0 0 25 0 1 0 489041849 54878208 12817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13398 12817 603 41 0 13357 0
vsize: 53592
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13275 0 0 0 26963 39 0 0 25 0 1 0 489041849 56352768 13203 4294967295 134512640 134672761 3221224544 3221223648 134560483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13203 603 41 0 13717 0
vsize: 55032
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13662 0 0 0 27961 40 0 0 25 0 1 0 489041849 57958400 13590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14150 13590 603 41 0 14109 0
vsize: 56600
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13886 0 0 0 28961 41 0 0 25 0 1 0 489041849 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13814 603 41 0 14336 0
vsize: 57508
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13886 0 0 0 29961 41 0 0 25 0 1 0 489041849 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13814 603 41 0 14336 0
vsize: 57508
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13886 0 0 0 30961 41 0 0 25 0 1 0 489041849 58888192 13814 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13814 603 41 0 14336 0
vsize: 57508
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13886 0 0 0 31961 41 0 0 25 0 1 0 489041849 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13814 603 41 0 14336 0
vsize: 57508
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13886 0 0 0 32962 41 0 0 25 0 1 0 489041849 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13814 603 41 0 14336 0
vsize: 57508
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13886 0 0 0 33962 41 0 0 25 0 1 0 489041849 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13814 603 41 0 14336 0
vsize: 57508
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13886 0 0 0 34962 41 0 0 25 0 1 0 489041849 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13814 603 41 0 14336 0
vsize: 57508
[startup+360.015 s]
Raw data (loadavg): 1.07 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13886 0 0 0 35962 41 0 0 25 0 1 0 489041849 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13814 603 41 0 14336 0
vsize: 57508
[startup+370.015 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13886 0 0 0 36962 41 0 0 25 0 1 0 489041849 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13814 603 41 0 14336 0
vsize: 57508
[startup+380.016 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 37962 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+390.015 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 38962 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223728 134558678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+400.015 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 39962 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+410.015 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 40962 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+420.016 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 41963 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+430.016 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 42963 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+440.016 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 43963 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+450.017 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 44963 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+460.018 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 45964 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+470.018 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 46964 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+480.019 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 47964 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+490.018 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 48964 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+500.018 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 49964 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+510.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 50964 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+520.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13887 0 0 0 51965 41 0 0 25 0 1 0 489041849 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13815 603 41 0 14336 0
vsize: 57508
[startup+530.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 52965 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+540.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 53965 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+550.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 54965 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+560.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 55965 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+570.019 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 56966 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+580.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 57966 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+590.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 58966 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+600.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 59966 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+610.021 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 60966 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+620.021 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 61966 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+630.022 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 62967 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+640.022 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 63967 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+650.022 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 64967 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+660.023 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 65967 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+670.022 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 66967 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+680.023 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 67967 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+690.024 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 68968 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+700.023 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 69968 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+710.024 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 70968 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+720.024 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13888 0 0 0 71968 41 0 0 25 0 1 0 489041849 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13816 603 41 0 14336 0
vsize: 57508
[startup+730.025 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13889 0 0 0 72969 41 0 0 25 0 1 0 489041849 58888192 13817 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13817 603 41 0 14336 0
vsize: 57508
[startup+740.025 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13891 0 0 0 73969 41 0 0 25 0 1 0 489041849 58888192 13819 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13819 603 41 0 14336 0
vsize: 57508
[startup+750.025 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13893 0 0 0 74969 41 0 0 25 0 1 0 489041849 58888192 13821 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13821 603 41 0 14336 0
vsize: 57508
[startup+760.025 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13896 0 0 0 75969 41 0 0 25 0 1 0 489041849 58888192 13824 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13824 603 41 0 14336 0
vsize: 57508
[startup+770.025 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13897 0 0 0 76969 42 0 0 25 0 1 0 489041849 58888192 13825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13825 603 41 0 14336 0
vsize: 57508
[startup+780.026 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 77969 42 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+790.027 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 78970 42 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+800.027 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 79970 42 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+810.028 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 80969 42 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+820.028 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 81968 43 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+830.029 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 82968 43 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223784 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+840.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 83968 43 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+850.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 84968 43 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+860.031 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 85967 44 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+870.031 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 86967 44 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+880.031 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 87967 44 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+890.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 88967 44 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+900.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 89967 45 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+910.033 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 90967 45 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+920.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 91966 45 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+930.033 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 92966 46 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+940.034 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 93966 46 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223728 134558768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+950.034 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 94966 46 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+960.034 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 95965 47 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+970.034 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 96965 47 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+980.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 97965 47 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+990.036 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 98965 48 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 99964 48 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 100964 48 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 101964 49 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13898 0 0 0 102964 49 0 0 25 0 1 0 489041849 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13900 0 0 0 103964 49 0 0 25 0 1 0 489041849 58888192 13828 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13828 603 41 0 14336 0
vsize: 57508
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13903 0 0 0 104964 49 0 0 25 0 1 0 489041849 58888192 13831 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13831 603 41 0 14336 0
vsize: 57508
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13905 0 0 0 105964 49 0 0 25 0 1 0 489041849 58888192 13833 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13833 603 41 0 14336 0
vsize: 57508
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13908 0 0 0 106964 49 0 0 25 0 1 0 489041849 58888192 13836 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13836 603 41 0 14336 0
vsize: 57508
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13910 0 0 0 107965 49 0 0 25 0 1 0 489041849 58888192 13838 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13838 603 41 0 14336 0
vsize: 57508
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13912 0 0 0 108965 49 0 0 25 0 1 0 489041849 58888192 13840 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13840 603 41 0 14336 0
vsize: 57508
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13914 0 0 0 109965 49 0 0 25 0 1 0 489041849 58888192 13842 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13842 603 41 0 14336 0
vsize: 57508
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13916 0 0 0 110965 49 0 0 25 0 1 0 489041849 58888192 13844 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13844 603 41 0 14336 0
vsize: 57508
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13919 0 0 0 111965 49 0 0 25 0 1 0 489041849 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13919 0 0 0 112966 49 0 0 25 0 1 0 489041849 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13919 0 0 0 113966 49 0 0 25 0 1 0 489041849 58888192 13847 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13919 0 0 0 114966 49 0 0 25 0 1 0 489041849 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13919 0 0 0 115966 49 0 0 25 0 1 0 489041849 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13919 0 0 0 116966 49 0 0 25 0 1 0 489041849 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13919 0 0 0 117966 49 0 0 25 0 1 0 489041849 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13919 0 0 0 118966 49 0 0 25 0 1 0 489041849 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7241
Raw data (stat): 7241 (minisat+) R 7240 32461 32460 0 -1 0 13919 0 0 0 119966 49 0 0 25 0 1 0 489041849 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.95 1/54 7241
Raw data (stat): 7241 (minisat+) Z 7240 32461 32460 0 -1 12 13922 0 0 0 119967 51 0 0 25 0 1 0 489041849 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.19
CPU user time (s): 1199.67
CPU system time (s): 0.518921
CPU usage (%): 100.009
Max. virtual memory (Kb): 57508
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####