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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10b.opb
MD5SUM	c76102ddcf7f5ab3b2677033d320eaa3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	756736
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	502612132
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	502612132
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	422.405
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 14818

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        688276 kB
Buffers:         30820 kB
Cached:         293944 kB
SwapCached:          4 kB
Active:          99812 kB
Inactive:       227472 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        688024 kB
SwapTotal:     2097136 kB
SwapFree:      2096768 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5924 kB
Slab:            13416 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:55:27 (client local time) WITH STATUS 10 IN 1200.45 SECONDS
stats: 19213 7 1200.45 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> BDD-cost: 1135
c ---[ 136]---> BDD-cost:  973
c ---[ 134]---> BDD-cost:  886
c ---[ 132]---> BDD-cost: 1137
c ---[ 130]---> BDD-cost:  918
c ---[ 128]---> BDD-cost: 1080
c ---[ 126]---> BDD-cost: 1031
c ---[ 124]---> BDD-cost:  815
c ---[ 122]---> BDD-cost:  886
c ---[ 120]---> BDD-cost: 1169
c ---[ 118]---> BDD-cost:  817
c ---[ 116]---> BDD-cost: 1118
c ---[ 114]---> BDD-cost:  960
c ---[ 112]---> BDD-cost: 1164
c ---[ 110]---> BDD-cost: 1153
c ---[ 108]---> BDD-cost:  817
c ---[ 106]---> BDD-cost: 1164
c ---[ 104]---> BDD-cost: 1040
c ---[ 102]---> BDD-cost:  607
c ---[ 100]---> BDD-cost: 1040
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   12
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   15
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   12
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   15
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:   11
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   12
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   57945   166633 |   19315       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 3554095[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:142488     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        19 |  451839  1086276 |  150613      19      407    21.4 |  0.000 % |
c |       119 |  451839  1086276 |  165674     119     6132    51.5 |  0.719 % |
c |       271 |  450725  1083741 |  182241     262     8372    32.0 |  0.916 % |
c |       498 |  450725  1083741 |  200465     489     9823    20.1 |  0.916 % |
c |       835 |  450725  1083741 |  220512     826    20152    24.4 |  0.916 % |
c ==============================================================================
c [1mFound solution: 2991769[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1025 |  452391  1088540 |  150797    1013    25464    25.1 |  0.916 % |
c |      1125 |  452391  1088540 |  165876    1113    26020    23.4 |  0.916 % |
c |      1277 |  452363  1088477 |  182464    1264    29328    23.2 |  0.921 % |
c |      1505 |  452363  1088477 |  200710    1492    47856    32.1 |  0.921 % |
c |      1842 |  452363  1088477 |  220781    1829   131633    72.0 |  0.921 % |
c |      2348 |  452363  1088477 |  242860    2335   140684    60.3 |  0.921 % |
c |      3109 |  452363  1088477 |  267146    3096   147102    47.5 |  0.921 % |
c |      4248 |  452363  1088477 |  293860    4235   159852    37.7 |  0.921 % |
c |      5956 |  452363  1088477 |  323246    5943   178132    30.0 |  0.921 % |
c |      8518 |  452363  1088477 |  355571    8505   207079    24.3 |  0.921 % |
c |     12362 |  452128  1087947 |  391128   12346   372248    30.2 |  0.960 % |
c |     18129 |  452128  1087947 |  430241   18113   626340    34.6 |  0.960 % |
c ==============================================================================
c [1mFound solution: 2465935[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18481 |  450352  1084070 |  150117   18425   639305    34.7 |  0.960 % |
c |     18581 |  450352  1084070 |  165128   18525   641180    34.6 |  1.384 % |
c |     18731 |  450352  1084070 |  181641   18675   644570    34.5 |  1.384 % |
c |     18956 |  450352  1084070 |  199805   18900   653860    34.6 |  1.384 % |
c |     19293 |  450352  1084070 |  219786   19237   659781    34.3 |  1.384 % |
c |     19800 |  450352  1084070 |  241764   19744   664387    33.7 |  1.384 % |
c |     20559 |  450352  1084070 |  265941   20503   670011    32.7 |  1.384 % |
c |     21700 |  449814  1082847 |  292535   21629   703984    32.5 |  1.481 % |
c |     23409 |  449724  1082642 |  321789   23337   723736    31.0 |  1.498 % |
c |     25971 |  449712  1082615 |  353968   25897   760457    29.4 |  1.499 % |
c |     29816 |  449712  1082615 |  389364   29742  1044732    35.1 |  1.499 % |
c |     35582 |  449712  1082615 |  428301   35508  1153707    32.5 |  1.499 % |
c |     44233 |  449712  1082615 |  471131   44159  1346382    30.5 |  1.499 % |
c |     57207 |  449712  1082615 |  518244   57133  1611565    28.2 |  1.499 % |
c ==============================================================================
c [1mFound solution: 2004246[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74957 |  450532  1084799 |  150177   74878  2230234    29.8 |  1.499 % |
c |     75057 |  450453  1084620 |  165194   74972  2233402    29.8 |  1.585 % |
c |     75209 |  450245  1084143 |  181714   75114  2234609    29.7 |  1.625 % |
c |     75435 |  450245  1084143 |  199885   75340  2236778    29.7 |  1.625 % |
c |     75772 |  450245  1084143 |  219874   75677  2239981    29.6 |  1.625 % |
c |     76278 |  450245  1084143 |  241861   76183  2246982    29.5 |  1.625 % |
c |     77037 |  450245  1084143 |  266047   76942  2252208    29.3 |  1.625 % |
c |     78176 |  450245  1084143 |  292652   78081  2271138    29.1 |  1.625 % |
c |     79884 |  450245  1084143 |  321917   79789  2293573    28.7 |  1.625 % |
c |     82446 |  450245  1084143 |  354109   82351  2545845    30.9 |  1.625 % |
c ==============================================================================
c [1mFound solution: 1634335[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82599 |  450511  1084971 |  150170   82504  2555090    31.0 |  1.625 % |
c |     82699 |  450511  1084971 |  165187   82604  2555944    30.9 |  1.624 % |
c |     82849 |  450511  1084971 |  181705   82754  2556727    30.9 |  1.624 % |
c |     83074 |  450221  1084315 |  199876   82936  2559843    30.9 |  1.675 % |
c |     83412 |  450221  1084315 |  219863   83274  2576658    30.9 |  1.675 % |
c |     83919 |  450221  1084315 |  241850   83781  2651590    31.6 |  1.675 % |
c |     84678 |  450221  1084315 |  266035   84540  2683234    31.7 |  1.675 % |
c |     85822 |  450221  1084315 |  292638   85684  2695210    31.5 |  1.675 % |
c |     87530 |  449807  1083374 |  321902   87367  2797333    32.0 |  1.750 % |
c |     90092 |  449807  1083374 |  354093   89929  3433440    38.2 |  1.750 % |
c |     93940 |  449807  1083374 |  389502   93777  3806073    40.6 |  1.750 % |
c |     99706 |  449807  1083374 |  428452   99543  4030589    40.5 |  1.750 % |
c |    108355 |  449764  1083277 |  471297  108191  4251518    39.3 |  1.758 % |
c |    121330 |  449659  1083036 |  518427  121165  6299349    52.0 |  1.777 % |
c ==============================================================================
c [1mFound solution: 1632925[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    121883 |  450049  1083999 |  150016  121717  6318891    51.9 |  1.777 % |
c |    121983 |  450049  1083999 |  165017  121817  6325444    51.9 |  1.781 % |
c |    122133 |  450049  1083999 |  181519  121967  6326342    51.9 |  1.781 % |
c |    122358 |  450049  1083999 |  199671  122192  6345604    51.9 |  1.781 % |
c |    122695 |  450049  1083999 |  219638  122529  6383044    52.1 |  1.781 % |
c ==============================================================================
c [1mFound solution: 1496403[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122862 |  450159  1084290 |  150053  122696  6391355    52.1 |  1.781 % |
c |    122964 |  450159  1084290 |  165058  122798  6399593    52.1 |  1.781 % |
c |    123114 |  450159  1084290 |  181564  122948  6400603    52.1 |  1.781 % |
c |    123341 |  450159  1084290 |  199720  123175  6408555    52.0 |  1.781 % |
c |    123678 |  450159  1084290 |  219692  123512  6419657    52.0 |  1.781 % |
c |    124185 |  450159  1084290 |  241661  124019  6439491    51.9 |  1.781 % |
c |    124946 |  450159  1084290 |  265828  124780  6541832    52.4 |  1.781 % |
c |    126086 |  450159  1084290 |  292410  125920  6649726    52.8 |  1.781 % |
c |    127794 |  449672  1083169 |  321651  127572  7022762    55.0 |  1.878 % |
c |    130357 |  449672  1083169 |  353817  130135  7676190    59.0 |  1.878 % |
c |    134201 |  449672  1083169 |  389198  133979  7729697    57.7 |  1.878 % |
c |    139968 |  449617  1083045 |  428118  139745  7945961    56.9 |  1.888 % |
c |    148618 |  449517  1082816 |  470930  148393  8179059    55.1 |  1.906 % |
c ==============================================================================
c [1mFound solution: 1464834[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150916 |  448514  1080532 |  149504  150608  8337031    55.4 |  1.906 % |
c |    151016 |  448514  1080532 |  164454  150708  8337632    55.3 |  2.110 % |
c |    151166 |  448493  1080486 |  180899  150856  8338695    55.3 |  2.114 % |
c |    151391 |  448493  1080486 |  198989  151081  8341444    55.2 |  2.114 % |
c |    151728 |  448416  1080310 |  218888  151414  8343716    55.1 |  2.128 % |
c |    152234 |  447905  1079142 |  240777  151888  8352890    55.0 |  2.222 % |
c |    152993 |  447905  1079142 |  264855  152647  8410937    55.1 |  2.222 % |
c |    154133 |  447905  1079142 |  291341  153787  8682887    56.5 |  2.222 % |
c |    155841 |  447905  1079142 |  320475  155495  8717725    56.1 |  2.222 % |
c |    158407 |  447665  1078596 |  352522  158054  9040255    57.2 |  2.264 % |
c ==============================================================================
c [1mFound solution: 1396323[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    158783 |  447734  1078785 |  149244  158430  9059659    57.2 |  2.264 % |
c |    158883 |  447734  1078785 |  164168   34029  1084457    31.9 |  2.264 % |
c |    159035 |  447734  1078785 |  180585   34181  1085391    31.8 |  2.264 % |
c |    159263 |  447734  1078785 |  198643   34409  1087596    31.6 |  2.264 % |
c |    159600 |  447734  1078785 |  218508   34746  1093375    31.5 |  2.264 % |
c |    160106 |  447734  1078785 |  240358   35252  1112539    31.6 |  2.264 % |
c |    160867 |  447734  1078785 |  264394   36013  1236961    34.3 |  2.264 % |
c |    162006 |  447734  1078785 |  290834   37152  1250526    33.7 |  2.264 % |
c |    163714 |  447734  1078785 |  319917   38860  1482573    38.2 |  2.264 % |
c ==============================================================================
c [1mFound solution: 780995[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165968 |  448044  1079523 |  149348   41114  1886613    45.9 |  2.264 % |
c |    166071 |  448044  1079523 |  164282   41217  1898309    46.1 |  2.262 % |
c |    166222 |  448044  1079523 |  180711   41368  1901097    46.0 |  2.262 % |
c |    166447 |  447765  1078880 |  198782   41592  1915132    46.0 |  2.318 % |
c |    166784 |  447662  1078646 |  218660   41924  1922316    45.9 |  2.336 % |
c |    167292 |  447460  1078181 |  240526   42412  1978442    46.6 |  2.375 % |
c |    168051 |  447460  1078181 |  264579   43171  2100330    48.7 |  2.375 % |
c ==============================================================================
c [1mFound solution: 765056[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    168184 |  447495  1078277 |  149165   43304  2114380    48.8 |  2.375 % |
c |    168285 |  447495  1078277 |  164081   43405  2120084    48.8 |  2.376 % |
c |    168435 |  447495  1078277 |  180489   43555  2127503    48.8 |  2.376 % |
c |    168660 |  447495  1078277 |  198538   43780  2153537    49.2 |  2.376 % |
c |    168998 |  447495  1078277 |  218392   44118  2160897    49.0 |  2.376 % |
c |    169506 |  447495  1078277 |  240231   44626  2164575    48.5 |  2.376 % |
c |    170265 |  447495  1078277 |  264254   45385  2225715    49.0 |  2.376 % |
c |    171405 |  447484  1078254 |  290680   46524  2290349    49.2 |  2.378 % |
c |    173114 |  447484  1078254 |  319748   48233  2740940    56.8 |  2.378 % |
c |    175676 |  447484  1078254 |  351723   50795  3385891    66.7 |  2.378 % |
c |    179524 |  447484  1078254 |  386895   54643  4667185    85.4 |  2.378 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 X3_bit0 X3_bit1 X3_bit2 X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 X19_bit0 -X19_bit1 X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 X41_bit0 -X41_bit1 X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 X55_bit0 X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 X57_bit0 -X57_bit1 -X57_bit2 X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 X60_bit0 X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 X61_bit1 X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 X73_bit0 X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 X92_bit1 X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -#### 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.94 0.90 1/54 27929
Raw data (stat): 27929 (runsolver) R 27928 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482940354 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99995 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 13138 0 0 0 969 29 0 0 25 0 1 0 482940354 62873600 12803 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15350 12803 603 41 0 15309 0
vsize: 61400
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 13414 0 0 0 1969 29 0 0 25 0 1 0 482940354 63987712 13079 4294967295 134512640 134672761 3221224528 3221223740 1075346912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15622 13079 603 41 0 15581 0
vsize: 62488
[startup+30.0023 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 13536 0 0 0 2968 29 0 0 25 0 1 0 482940354 64528384 13201 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15754 13201 603 41 0 15713 0
vsize: 63016
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 13610 0 0 0 3968 30 0 0 25 0 1 0 482940354 64942080 13275 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 13275 603 41 0 15814 0
vsize: 63420
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 13791 0 0 0 4968 31 0 0 25 0 1 0 482940354 65609728 13456 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16018 13456 603 41 0 15977 0
vsize: 64072
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14046 0 0 0 5967 31 0 0 25 0 1 0 482940354 66670592 13711 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16277 13711 603 41 0 16236 0
vsize: 65108
[startup+70.004 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14115 0 0 0 6966 32 0 0 25 0 1 0 482940354 66834432 13768 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16317 13768 603 41 0 16276 0
vsize: 65268
[startup+80.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14183 0 0 0 7966 32 0 0 25 0 1 0 482940354 67104768 13836 4294967295 134512640 134672761 3221224528 3221223664 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16383 13836 603 41 0 16342 0
vsize: 65532
[startup+90.0055 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14288 0 0 0 8966 33 0 0 25 0 1 0 482940354 67641344 13941 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16514 13941 603 41 0 16473 0
vsize: 66056
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14351 0 0 0 9966 33 0 0 25 0 1 0 482940354 67776512 14004 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16547 14004 603 41 0 16506 0
vsize: 66188
[startup+110.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14399 0 0 0 10966 33 0 0 25 0 1 0 482940354 68034560 14052 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16610 14052 603 41 0 16569 0
vsize: 66440
[startup+120.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14562 0 0 0 11966 34 0 0 25 0 1 0 482940354 68784128 14215 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16793 14215 603 41 0 16752 0
vsize: 67172
[startup+130.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14644 0 0 0 12966 34 0 0 25 0 1 0 482940354 69054464 14297 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16859 14297 603 41 0 16818 0
vsize: 67436
[startup+140.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14744 0 0 0 13966 34 0 0 25 0 1 0 482940354 69582848 14397 4294967295 134512640 134672761 3221224528 3221223696 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16988 14397 603 41 0 16947 0
vsize: 67952
[startup+150.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 14923 0 0 0 14966 35 0 0 25 0 1 0 482940354 70254592 14576 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17152 14576 603 41 0 17111 0
vsize: 68608
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 15098 0 0 0 15966 35 0 0 25 0 1 0 482940354 70930432 14751 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17317 14751 603 41 0 17276 0
vsize: 69268
[startup+170.011 s]
Raw data (loadavg): 0.99 0.96 0.91 3/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 15235 0 0 0 16966 36 0 0 25 0 1 0 482940354 71471104 14888 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17449 14888 603 41 0 17408 0
vsize: 69796
[startup+180.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 15356 0 0 0 17965 37 0 0 25 0 1 0 482940354 72007680 15009 4294967295 134512640 134672761 3221224528 3221223728 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17580 15009 603 41 0 17539 0
vsize: 70320
[startup+190.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 15418 0 0 0 18966 37 0 0 25 0 1 0 482940354 72265728 15071 4294967295 134512640 134672761 3221224528 3221223712 134559159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17643 15071 603 41 0 17602 0
vsize: 70572
[startup+200.012 s]
Raw data (loadavg): 0.99 0.96 0.91 3/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 15522 0 0 0 19966 37 0 0 25 0 1 0 482940354 72646656 15175 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17736 15175 603 41 0 17695 0
vsize: 70944
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 15643 0 0 0 20966 37 0 0 25 0 1 0 482940354 73179136 15296 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17866 15296 603 41 0 17825 0
vsize: 71464
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 15845 0 0 0 21965 38 0 0 25 0 1 0 482940354 74244096 15498 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18126 15498 603 41 0 18085 0
vsize: 72504
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 15950 0 0 0 22966 38 0 0 25 0 1 0 482940354 74645504 15603 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18224 15603 603 41 0 18183 0
vsize: 72896
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16057 0 0 0 23965 39 0 0 25 0 1 0 482940354 75042816 15710 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18321 15710 603 41 0 18280 0
vsize: 73284
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16161 0 0 0 24966 39 0 0 25 0 1 0 482940354 75309056 15797 4294967295 134512640 134672761 3221224528 3221223700 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18386 15797 603 41 0 18345 0
vsize: 73544
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16234 0 0 0 25966 39 0 0 25 0 1 0 482940354 75710464 15870 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18484 15870 603 41 0 18443 0
vsize: 73936
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16344 0 0 0 26966 39 0 0 25 0 1 0 482940354 76111872 15980 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18582 15980 603 41 0 18541 0
vsize: 74328
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16439 0 0 0 27966 40 0 0 25 0 1 0 482940354 76509184 16075 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18679 16075 603 41 0 18638 0
vsize: 74716
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16515 0 0 0 28966 40 0 0 25 0 1 0 482940354 76771328 16151 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18743 16151 603 41 0 18702 0
vsize: 74972
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16580 0 0 0 29966 40 0 0 25 0 1 0 482940354 77045760 16200 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18810 16200 603 41 0 18769 0
vsize: 75240
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16671 0 0 0 30966 40 0 0 25 0 1 0 482940354 77316096 16291 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18876 16291 603 41 0 18835 0
vsize: 75504
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16756 0 0 0 31966 41 0 0 25 0 1 0 482940354 77721600 16376 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18975 16376 603 41 0 18934 0
vsize: 75900
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16839 0 0 0 32967 41 0 0 25 0 1 0 482940354 77991936 16459 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19041 16459 603 41 0 19000 0
vsize: 76164
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 16933 0 0 0 33967 41 0 0 25 0 1 0 482940354 78393344 16553 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19139 16553 603 41 0 19098 0
vsize: 76556
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 17216 0 0 0 34966 42 0 0 25 0 1 0 482940354 79618048 16836 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19438 16836 603 41 0 19397 0
vsize: 77752
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 17537 0 0 0 35966 43 0 0 25 0 1 0 482940354 80805888 17157 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19728 17157 603 41 0 19687 0
vsize: 78912
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 17805 0 0 0 36966 43 0 0 25 0 1 0 482940354 82006016 17425 4294967295 134512640 134672761 3221224528 3221223632 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20021 17425 603 41 0 19980 0
vsize: 80084
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 17972 0 0 0 37965 44 0 0 25 0 1 0 482940354 82681856 17592 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20186 17592 603 41 0 20145 0
vsize: 80744
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 18050 0 0 0 38965 44 0 0 25 0 1 0 482940354 82948096 17670 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20251 17670 603 41 0 20210 0
vsize: 81004
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 18162 0 0 0 39965 45 0 0 25 0 1 0 482940354 83353600 17782 4294967295 134512640 134672761 3221224528 3221223696 134564467 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20350 17782 603 41 0 20309 0
vsize: 81400
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 18277 0 0 0 40965 45 0 0 25 0 1 0 482940354 83890176 17897 4294967295 134512640 134672761 3221224528 3221223696 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20481 17897 603 41 0 20440 0
vsize: 81924
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 18396 0 0 0 41965 45 0 0 25 0 1 0 482940354 84295680 18016 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20580 18016 603 41 0 20539 0
vsize: 82320
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 18497 0 0 0 42965 46 0 0 25 0 1 0 482940354 84701184 18117 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20679 18117 603 41 0 20638 0
vsize: 82716
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 18696 0 0 0 43965 47 0 0 25 0 1 0 482940354 85508096 18316 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20876 18316 603 41 0 20835 0
vsize: 83504
[startup+450.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 18897 0 0 0 44965 47 0 0 25 0 1 0 482940354 86310912 18517 4294967295 134512640 134672761 3221224528 3221223620 1075351142 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21072 18517 603 41 0 21031 0
vsize: 84288
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 19091 0 0 0 45964 48 0 0 25 0 1 0 482940354 87097344 18711 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21264 18711 603 41 0 21223 0
vsize: 85056
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 19192 0 0 0 46964 48 0 0 25 0 1 0 482940354 87625728 18812 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21393 18812 603 41 0 21352 0
vsize: 85572
[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 19399 0 0 0 47965 49 0 0 25 0 1 0 482940354 88432640 19019 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21590 19019 603 41 0 21549 0
vsize: 86360
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 19501 0 0 0 48964 49 0 0 25 0 1 0 482940354 88838144 19121 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21689 19121 603 41 0 21648 0
vsize: 86756
[startup+500.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 19665 0 0 0 49964 50 0 0 25 0 1 0 482940354 89513984 19285 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21854 19285 603 41 0 21813 0
vsize: 87416
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 19803 0 0 0 50965 50 0 0 25 0 1 0 482940354 90079232 19423 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21992 19423 603 41 0 21951 0
vsize: 87968
[startup+520.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 20000 0 0 0 51964 50 0 0 25 0 1 0 482940354 90857472 19620 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22182 19620 603 41 0 22141 0
vsize: 88728
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 20251 0 0 0 52964 51 0 0 25 0 1 0 482940354 91922432 19871 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22442 19871 603 41 0 22401 0
vsize: 89768
[startup+540.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 20490 0 0 0 53964 51 0 0 25 0 1 0 482940354 92864512 20110 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22672 20110 603 41 0 22631 0
vsize: 90688
[startup+550.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 20615 0 0 0 54964 51 0 0 25 0 1 0 482940354 93212672 20219 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22757 20219 603 41 0 22716 0
vsize: 91028
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 20658 0 0 0 55963 52 0 0 25 0 1 0 482940354 93478912 20262 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22822 20262 603 41 0 22781 0
vsize: 91288
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 20723 0 0 0 56963 52 0 0 25 0 1 0 482940354 93585408 20312 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22848 20312 603 41 0 22807 0
vsize: 91392
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 20826 0 0 0 57963 52 0 0 25 0 1 0 482940354 94117888 20415 4294967295 134512640 134672761 3221224528 3221223696 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22978 20415 603 41 0 22937 0
vsize: 91912
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 20965 0 0 0 58963 53 0 0 25 0 1 0 482940354 94658560 20554 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23110 20554 603 41 0 23069 0
vsize: 92440
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 21050 0 0 0 59963 53 0 0 25 0 1 0 482940354 94928896 20639 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23176 20639 603 41 0 23135 0
vsize: 92704
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 21206 0 0 0 60963 53 0 0 25 0 1 0 482940354 95604736 20795 4294967295 134512640 134672761 3221224528 3221223684 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23341 20795 603 41 0 23300 0
vsize: 93364
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 21358 0 0 0 61963 54 0 0 25 0 1 0 482940354 96284672 20947 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23507 20947 603 41 0 23466 0
vsize: 94028
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 21582 0 0 0 62962 55 0 0 25 0 1 0 482940354 97083392 21171 4294967295 134512640 134672761 3221224528 3221223632 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23702 21171 603 41 0 23661 0
vsize: 94808
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 21767 0 0 0 63962 56 0 0 25 0 1 0 482940354 97910784 21356 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23904 21356 603 41 0 23863 0
vsize: 95616
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 21994 0 0 0 64962 56 0 0 25 0 1 0 482940354 98840576 21583 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 21583 603 41 0 24090 0
vsize: 96524
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22076 0 0 0 65962 57 0 0 25 0 1 0 482940354 99627008 21665 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24323 21665 603 41 0 24282 0
vsize: 97292
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22159 0 0 0 66962 57 0 0 25 0 1 0 482940354 100024320 21748 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24420 21748 603 41 0 24379 0
vsize: 97680
[startup+680.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22235 0 0 0 67962 57 0 0 25 0 1 0 482940354 100294656 21824 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24486 21824 603 41 0 24445 0
vsize: 97944
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22298 0 0 0 68962 57 0 0 25 0 1 0 482940354 100564992 21887 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24552 21887 603 41 0 24511 0
vsize: 98208
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22398 0 0 0 69962 58 0 0 25 0 1 0 482940354 100966400 21987 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24650 21987 603 41 0 24609 0
vsize: 98600
[startup+710.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22460 0 0 0 70962 58 0 0 25 0 1 0 482940354 101232640 22049 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24715 22049 603 41 0 24674 0
vsize: 98860
[startup+720.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22495 0 0 0 71962 58 0 0 25 0 1 0 482940354 101363712 22084 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24747 22084 603 41 0 24706 0
vsize: 98988
[startup+730.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22632 0 0 0 72962 59 0 0 25 0 1 0 482940354 101896192 22221 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24877 22221 603 41 0 24836 0
vsize: 99508
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22674 0 0 0 73963 59 0 0 25 0 1 0 482940354 102027264 22263 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24909 22263 603 41 0 24868 0
vsize: 99636
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22716 0 0 0 74963 59 0 0 25 0 1 0 482940354 102162432 22305 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24942 22305 603 41 0 24901 0
vsize: 99768
[startup+760.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22882 0 0 0 75962 60 0 0 25 0 1 0 482940354 102756352 22455 4294967295 134512640 134672761 3221224528 3221223664 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25087 22455 603 41 0 25046 0
vsize: 100348
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22885 0 0 0 76963 60 0 0 25 0 1 0 482940354 102887424 22458 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25119 22458 603 41 0 25078 0
vsize: 100476
[startup+780.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 22968 0 0 0 77963 60 0 0 25 0 1 0 482940354 103149568 22541 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25183 22541 603 41 0 25142 0
vsize: 100732
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23192 0 0 0 78963 61 0 0 25 0 1 0 482940354 104067072 22765 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25407 22765 603 41 0 25366 0
vsize: 101628
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23265 0 0 0 79963 61 0 0 25 0 1 0 482940354 104333312 22838 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25472 22838 603 41 0 25431 0
vsize: 101888
[startup+810.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23404 0 0 0 80963 61 0 0 25 0 1 0 482940354 104988672 22977 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25632 22977 603 41 0 25591 0
vsize: 102528
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23498 0 0 0 81963 61 0 0 25 0 1 0 482940354 105254912 23071 4294967295 134512640 134672761 3221224528 3221223712 134559512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25697 23071 603 41 0 25656 0
vsize: 102788
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23550 0 0 0 82963 62 0 0 25 0 1 0 482940354 105521152 23123 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25762 23123 603 41 0 25721 0
vsize: 103048
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23606 0 0 0 83963 62 0 0 25 0 1 0 482940354 105791488 23179 4294967295 134512640 134672761 3221224528 3221223696 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25828 23179 603 41 0 25787 0
vsize: 103312
[startup+850.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23667 0 0 0 84963 62 0 0 25 0 1 0 482940354 105873408 23223 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23223 603 41 0 25807 0
vsize: 103392
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23667 0 0 0 85964 62 0 0 25 0 1 0 482940354 105873408 23223 4294967295 134512640 134672761 3221224528 3221223664 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23223 603 41 0 25807 0
vsize: 103392
[startup+870.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23667 0 0 0 86964 62 0 0 25 0 1 0 482940354 105873408 23223 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23223 603 41 0 25807 0
vsize: 103392
[startup+880.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23667 0 0 0 87964 62 0 0 25 0 1 0 482940354 105873408 23223 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23223 603 41 0 25807 0
vsize: 103392
[startup+890.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23667 0 0 0 88965 62 0 0 25 0 1 0 482940354 105873408 23223 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23223 603 41 0 25807 0
vsize: 103392
[startup+900.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23667 0 0 0 89965 62 0 0 25 0 1 0 482940354 105873408 23223 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23223 603 41 0 25807 0
vsize: 103392
[startup+910.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23667 0 0 0 90966 62 0 0 25 0 1 0 482940354 105873408 23223 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23223 603 41 0 25807 0
vsize: 103392
[startup+920.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23667 0 0 0 91966 62 0 0 25 0 1 0 482940354 105873408 23223 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23223 603 41 0 25807 0
vsize: 103392
[startup+930.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23667 0 0 0 92966 62 0 0 25 0 1 0 482940354 105873408 23223 4294967295 134512640 134672761 3221224528 3221223632 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23223 603 41 0 25807 0
vsize: 103392
[startup+940.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23668 0 0 0 93967 62 0 0 25 0 1 0 482940354 105873408 23224 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23224 603 41 0 25807 0
vsize: 103392
[startup+950.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23668 0 0 0 94967 62 0 0 25 0 1 0 482940354 105873408 23224 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23224 603 41 0 25807 0
vsize: 103392
[startup+960.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23668 0 0 0 95968 62 0 0 25 0 1 0 482940354 105873408 23224 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25848 23224 603 41 0 25807 0
vsize: 103392
[startup+970.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23711 0 0 0 96968 62 0 0 25 0 1 0 482940354 106135552 23267 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23267 603 41 0 25871 0
vsize: 103648
[startup+980.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 97969 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+990.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 98969 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 99969 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 100970 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 101970 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 102970 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 103971 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 104971 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 105971 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 106972 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1080.06 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 107972 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1090.06 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 108973 62 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1100.06 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 109973 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1110.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 110973 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1120.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 111974 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1130.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 112974 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1140.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 113974 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1150.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 114975 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1160.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 115975 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1170.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 116976 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1180.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 117976 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223632 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1190.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 118976 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
[startup+1200.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27929
Raw data (stat): 27929 (minisat+) R 27928 29653 29652 0 -1 0 23714 0 0 0 119977 63 0 0 25 0 1 0 482940354 106135552 23270 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23270 603 41 0 25871 0
vsize: 103648
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.01 0.99 0.91 1/54 27929
Raw data (stat): 27929 (minisat+) Z 27928 29653 29652 0 -1 12 23717 0 0 0 119977 67 0 0 25 0 1 0 482940354 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.12
CPU time (s): 1200.45
CPU user time (s): 1199.78
CPU system time (s): 0.675897
CPU usage (%): 100.028
Max. virtual memory (Kb): 103648
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####