PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-egout.opb
MD5SUM	fd101f0ba1a3813e843a38997ab7ed84
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.04984
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 18288

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        301896 kB
Buffers:         35208 kB
Cached:         667208 kB
SwapCached:         24 kB
Active:         194160 kB
Inactive:       510924 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        301644 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22084 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:32:32 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 18301 7 1200.24 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.85 0.97 0.95 2/54 3161
Raw data (stat): 3161 (runsolver) R 3160 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545703878 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99978 s]
Raw data (loadavg): 0.87 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 1929 0 0 0 994 5 0 0 25 0 1 0 545703878 10010624 1899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2444 1899 603 41 0 2403 0
vsize: 9776
[startup+19.9995 s]
Raw data (loadavg): 0.89 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 2653 0 0 0 1992 7 0 0 25 0 1 0 545703878 12636160 2581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3085 2581 603 41 0 3044 0
vsize: 12340
[startup+30.0006 s]
Raw data (loadavg): 0.91 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 3385 0 0 0 2989 10 0 0 25 0 1 0 545703878 15728640 3313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3840 3313 603 41 0 3799 0
vsize: 15360
[startup+39.9999 s]
Raw data (loadavg): 0.92 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 3957 0 0 0 3987 12 0 0 25 0 1 0 545703878 18153472 3885 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4432 3885 603 41 0 4391 0
vsize: 17728
[startup+50.0006 s]
Raw data (loadavg): 0.93 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 4564 0 0 0 4985 14 0 0 25 0 1 0 545703878 20701184 4492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5054 4492 603 41 0 5013 0
vsize: 20216
[startup+60.0007 s]
Raw data (loadavg): 0.94 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 4655 0 0 0 5984 15 0 0 25 0 1 0 545703878 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.001 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 4655 0 0 0 6984 15 0 0 25 0 1 0 545703878 20971520 4583 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5120 4583 603 41 0 5079 0
vsize: 20480
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 4757 0 0 0 7984 16 0 0 25 0 1 0 545703878 21504000 4685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5250 4685 603 41 0 5209 0
vsize: 21000
[startup+90.0018 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 5270 0 0 0 8982 18 0 0 25 0 1 0 545703878 23515136 5198 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5741 5198 603 41 0 5700 0
vsize: 22964
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 5744 0 0 0 9980 19 0 0 25 0 1 0 545703878 25534464 5672 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6234 5672 603 41 0 6193 0
vsize: 24936
[startup+110.002 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 6162 0 0 0 10980 20 0 0 25 0 1 0 545703878 27127808 6090 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6623 6090 603 41 0 6582 0
vsize: 26492
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 6606 0 0 0 11978 22 0 0 25 0 1 0 545703878 29020160 6534 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7085 6534 603 41 0 7044 0
vsize: 28340
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 7013 0 0 0 12977 23 0 0 25 0 1 0 545703878 30605312 6941 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7472 6941 603 41 0 7431 0
vsize: 29888
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 7420 0 0 0 13977 23 0 0 25 0 1 0 545703878 32342016 7348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7896 7348 603 41 0 7855 0
vsize: 31584
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 7935 0 0 0 14976 25 0 0 25 0 1 0 545703878 34361344 7863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8389 7863 603 41 0 8348 0
vsize: 33556
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 8529 0 0 0 15975 25 0 0 25 0 1 0 545703878 36773888 8457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8978 8457 603 41 0 8937 0
vsize: 35912
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 9074 0 0 0 16974 27 0 0 25 0 1 0 545703878 39051264 9002 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9534 9002 603 41 0 9493 0
vsize: 38136
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 9522 0 0 0 17973 28 0 0 25 0 1 0 545703878 40927232 9450 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9992 9450 603 41 0 9951 0
vsize: 39968
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 9954 0 0 0 18971 30 0 0 25 0 1 0 545703878 42672128 9882 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10418 9882 603 41 0 10377 0
vsize: 41672
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 10399 0 0 0 19970 31 0 0 25 0 1 0 545703878 44412928 10327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10327 603 41 0 10802 0
vsize: 43372
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 10833 0 0 0 20970 32 0 0 25 0 1 0 545703878 46284800 10761 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11300 10761 603 41 0 11259 0
vsize: 45200
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 11180 0 0 0 21969 32 0 0 25 0 1 0 545703878 47624192 11108 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11627 11108 603 41 0 11586 0
vsize: 46508
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 11658 0 0 0 22968 34 0 0 25 0 1 0 545703878 49905664 11586 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12184 11586 603 41 0 12143 0
vsize: 48736
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 12043 0 0 0 23966 36 0 0 25 0 1 0 545703878 51380224 11971 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12544 11971 603 41 0 12503 0
vsize: 50176
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 12485 0 0 0 24965 37 0 0 25 0 1 0 545703878 53137408 12413 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12973 12413 603 41 0 12932 0
vsize: 51892
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 12865 0 0 0 25965 38 0 0 25 0 1 0 545703878 54747136 12793 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13366 12793 603 41 0 13325 0
vsize: 53464
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13253 0 0 0 26964 39 0 0 25 0 1 0 545703878 56352768 13181 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 13181 603 41 0 13717 0
vsize: 55032
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13641 0 0 0 27963 40 0 0 25 0 1 0 545703878 57958400 13569 4294967295 134512640 134672761 3221224544 3221223728 134559388 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14150 13569 603 41 0 14109 0
vsize: 56600
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13886 0 0 0 28962 41 0 0 25 0 1 0 545703878 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134561161 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13886 0 0 0 29962 41 0 0 25 0 1 0 545703878 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+310.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13886 0 0 0 30962 41 0 0 25 0 1 0 545703878 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134560867 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13886 0 0 0 31962 41 0 0 25 0 1 0 545703878 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+330.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13886 0 0 0 32962 41 0 0 25 0 1 0 545703878 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+340.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13886 0 0 0 33963 41 0 0 25 0 1 0 545703878 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134560855 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13886 0 0 0 34963 41 0 0 25 0 1 0 545703878 58888192 13814 4294967295 134512640 134672761 3221224544 3221223680 134560729 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13886 0 0 0 35963 41 0 0 25 0 1 0 545703878 58888192 13814 4294967295 134512640 134672761 3221224544 3221223712 134561118 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13886 0 0 0 36963 41 0 0 25 0 1 0 545703878 58888192 13814 4294967295 134512640 134672761 3221224544 3221223648 134560218 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 37963 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560942 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 38963 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560822 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 39963 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223600 134565119 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 40963 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560948 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 41963 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134561215 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 42964 42 0 0 25 0 1 0 545703878 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+440.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 43964 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223728 134558662 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 44964 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 45964 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 46964 42 0 0 25 0 1 0 545703878 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+480.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 47964 42 0 0 25 0 1 0 545703878 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+490.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 48964 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134561118 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 49965 42 0 0 25 0 1 0 545703878 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+510.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 50965 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134561001 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13887 0 0 0 51965 42 0 0 25 0 1 0 545703878 58888192 13815 4294967295 134512640 134672761 3221224544 3221223712 134560852 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 52965 42 0 0 25 0 1 0 545703878 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.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 53965 42 0 0 25 0 1 0 545703878 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+550.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 54965 42 0 0 25 0 1 0 545703878 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+560.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 55965 43 0 0 25 0 1 0 545703878 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+570.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 56965 43 0 0 25 0 1 0 545703878 58888192 13816 4294967295 134512640 134672761 3221224544 3221223728 134559031 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.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 57965 43 0 0 25 0 1 0 545703878 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+590.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 58965 43 0 0 25 0 1 0 545703878 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+600.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 59965 43 0 0 25 0 1 0 545703878 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+610.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 60966 43 0 0 25 0 1 0 545703878 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134561167 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 61966 43 0 0 25 0 1 0 545703878 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+630.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 62966 43 0 0 25 0 1 0 545703878 58888192 13816 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 63965 44 0 0 25 0 1 0 545703878 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+650.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 64965 44 0 0 25 0 1 0 545703878 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 65965 44 0 0 25 0 1 0 545703878 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 66965 44 0 0 25 0 1 0 545703878 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 67966 44 0 0 25 0 1 0 545703878 58888192 13816 4294967295 134512640 134672761 3221224544 3221223712 134560839 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 68966 45 0 0 25 0 1 0 545703878 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+700.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 69965 45 0 0 25 0 1 0 545703878 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 70966 45 0 0 25 0 1 0 545703878 58888192 13816 4294967295 134512640 134672761 3221224544 3221223680 134560709 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13888 0 0 0 71966 45 0 0 25 0 1 0 545703878 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13889 0 0 0 72966 45 0 0 25 0 1 0 545703878 58888192 13817 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13891 0 0 0 73966 45 0 0 25 0 1 0 545703878 58888192 13819 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13893 0 0 0 74966 45 0 0 25 0 1 0 545703878 58888192 13821 4294967295 134512640 134672761 3221224544 3221223712 134560996 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13896 0 0 0 75966 45 0 0 25 0 1 0 545703878 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 76966 45 0 0 25 0 1 0 545703878 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+780.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 77967 45 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 78967 45 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560906 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.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 79967 45 0 0 25 0 1 0 545703878 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+810.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 80967 45 0 0 25 0 1 0 545703878 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+820.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 81967 45 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+830.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 82967 45 0 0 25 0 1 0 545703878 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+840.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 83967 45 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 84967 45 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223728 134558856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+860.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 85967 45 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 86967 46 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+880.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 87968 46 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 88968 46 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 89968 46 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+910.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 90968 46 0 0 25 0 1 0 545703878 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+920.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 91968 46 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+930.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 92968 46 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+940.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 93968 46 0 0 25 0 1 0 545703878 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+950.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 94968 46 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+960.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 95968 46 0 0 25 0 1 0 545703878 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+970.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 96968 46 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 97970 46 0 0 25 0 1 0 545703878 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+990.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 98969 47 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 99970 47 0 0 25 0 1 0 545703878 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+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 100970 47 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223728 134558875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 101970 47 0 0 25 0 1 0 545703878 58888192 13826 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13826 603 41 0 14336 0
vsize: 57508
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13898 0 0 0 102970 47 0 0 25 0 1 0 545703878 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+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13901 0 0 0 103970 47 0 0 25 0 1 0 545703878 58888192 13829 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13829 603 41 0 14336 0
vsize: 57508
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13904 0 0 0 104970 47 0 0 25 0 1 0 545703878 58888192 13832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13832 603 41 0 14336 0
vsize: 57508
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13906 0 0 0 105970 47 0 0 25 0 1 0 545703878 58888192 13834 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13834 603 41 0 14336 0
vsize: 57508
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13908 0 0 0 106970 47 0 0 25 0 1 0 545703878 58888192 13836 4294967295 134512640 134672761 3221224544 3221223712 134561226 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.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13911 0 0 0 107971 47 0 0 25 0 1 0 545703878 58888192 13839 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13839 603 41 0 14336 0
vsize: 57508
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13913 0 0 0 108971 47 0 0 25 0 1 0 545703878 58888192 13841 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13841 603 41 0 14336 0
vsize: 57508
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13915 0 0 0 109971 47 0 0 25 0 1 0 545703878 58888192 13843 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13843 603 41 0 14336 0
vsize: 57508
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13917 0 0 0 110971 47 0 0 25 0 1 0 545703878 58888192 13845 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13845 603 41 0 14336 0
vsize: 57508
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13919 0 0 0 111971 48 0 0 25 0 1 0 545703878 58888192 13847 4294967295 134512640 134672761 3221224544 3221223648 134554642 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.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13919 0 0 0 112971 48 0 0 25 0 1 0 545703878 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134561027 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.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13919 0 0 0 113971 48 0 0 25 0 1 0 545703878 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+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13919 0 0 0 114971 48 0 0 25 0 1 0 545703878 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+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13919 0 0 0 115972 48 0 0 25 0 1 0 545703878 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14377 13847 603 41 0 14336 0
vsize: 57508
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13919 0 0 0 116971 48 0 0 25 0 1 0 545703878 58888192 13847 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13919 0 0 0 117971 48 0 0 25 0 1 0 545703878 58888192 13847 4294967295 134512640 134672761 3221224544 3221223744 134557919 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.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13919 0 0 0 118972 48 0 0 25 0 1 0 545703878 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+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3161
Raw data (stat): 3161 (minisat+) R 3160 26298 26297 0 -1 0 13919 0 0 0 119972 48 0 0 25 0 1 0 545703878 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.95 1/54 3161
Raw data (stat): 3161 (minisat+) Z 3160 26298 26297 0 -1 12 13922 0 0 0 119972 51 0 0 25 0 1 0 545703878 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.06
CPU time (s): 1200.24
CPU user time (s): 1199.72
CPU system time (s): 0.513921
CPU usage (%): 100.015
Max. virtual memory (Kb): 57508
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####