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-bal8x12.opb
MD5SUM	69e7430fb77e7d40f128bdde5f7776a3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	13476271
Optimality of the best value was proved	NO
Number of terms in the objective function	2016
Biggest coefficient in the objective function	402653184
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	34444990400
Number of bits of the sum of numbers in the objective function	36
Biggest number in a constraint	402653184
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	34444990400
Number of bits of the biggest sum of numbers	36
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.37
Number of variables	2016
Total number of constraints	116
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	116
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 17855

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 12:25:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18964 boxname=wulflinc8 idbench=1459 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  69e7430fb77e7d40f128bdde5f7776a3  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-bal8x12.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-bal8x12.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-bal8x12.opb
IDLAUNCH: 18964
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        678640 kB
Buffers:         29636 kB
Cached:         304040 kB
SwapCached:          0 kB
Active:          75380 kB
Inactive:       261240 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        678388 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            13580 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 12:45:04 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 18964 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 136 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 134]---> Adder-cost: 240   maxlim: 20596   bits: 15/15
c ---[ 132]---> Adder-cost: 254   maxlim: 32244   bits: 16/15
c ---[ 130]---> Adder-cost: 254   maxlim: 33140   bits: 16/16
c ---[ 128]---> Adder-cost: 254   maxlim: 34420   bits: 16/16
c ---[ 126]---> Adder-cost: 254   maxlim: 31604   bits: 16/15
c ---[ 124]---> Adder-cost: 254   maxlim: 34420   bits: 16/16
c ---[ 122]---> Adder-cost: 240   maxlim: 21236   bits: 15/15
c ---[ 120]---> Adder-cost: 254   maxlim: 31604   bits: 16/15
c ---[ 118]---> Adder-cost: 166   maxlim: 26104   bits: 15/15
c ---[ 116]---> Adder-cost: 154   maxlim: 14456   bits: 14/14
c ---[ 114]---> Adder-cost: 154   maxlim: 15096   bits: 14/14
c ---[ 112]---> Adder-cost: 140   maxlim: 7544   bits: 13/13
c ---[ 110]---> Adder-cost: 166   maxlim: 26104   bits: 15/15
c ---[ 108]---> Adder-cost: 154   maxlim: 14456   bits: 14/14
c ---[ 106]---> Adder-cost: 140   maxlim: 7544   bits: 13/13
c ---[ 104]---> Adder-cost: 166   maxlim: 26104   bits: 15/15
c ---[ 102]---> Adder-cost: 166   maxlim: 24824   bits: 15/15
c ---[ 100]---> Adder-cost: 154   maxlim: 15096   bits: 14/14
c ---[  98]---> Adder-cost: 172   maxlim: 36472   bits: 16/16
c ---[  96]---> Adder-cost: 166   maxlim: 25464   bits: 15/15
c ---[  95]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  94]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  93]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  92]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  91]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  90]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  89]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  88]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  87]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  86]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  85]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  84]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  83]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  82]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  81]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  80]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  79]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  78]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  77]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  76]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  75]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  74]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  73]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  72]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  71]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  70]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  69]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  68]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  67]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  66]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  65]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  64]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  63]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  62]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  61]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  60]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  59]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  58]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  57]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  56]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  55]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  54]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  53]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  52]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  51]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  50]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  48]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  47]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  46]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  45]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  44]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  43]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  42]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  41]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  37]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  36]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  35]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  34]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  33]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  32]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  31]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  30]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  29]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  28]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  27]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  26]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  25]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  24]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  23]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  22]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  21]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  20]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  19]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  18]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  17]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  16]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  15]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  14]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  13]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  11]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  10]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[   9]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   8]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   7]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[   6]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   4]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[   3]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   2]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   1]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[   0]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29832   109862 |    9944       0        0     nan |  0.000 % |
c |       100 |   29832   109862 |   10938     100      325     3.2 | 31.665 % |
c |       250 |   29825   109839 |   12032     249     1132     4.5 | 31.678 % |
c |       475 |   29802   109764 |   13235     469     2247     4.8 | 31.728 % |
c |       812 |   29732   109530 |   14559     798     3951     5.0 | 31.904 % |
c |      1318 |   29724   109504 |   16014    1303     7445     5.7 | 31.917 % |
c |      2077 |   29524   108828 |   17616    2036    11115     5.5 | 32.382 % |
c |      3216 |   29483   108695 |   19378    3170    16752     5.3 | 32.482 % |
c |      4924 |   29388   108374 |   21315    4863    25652     5.3 | 32.684 % |
c |      7486 |   29141   107561 |   23447    7388    39508     5.3 | 33.275 % |
c |     11330 |   28949   106915 |   25792   11202    61021     5.4 | 33.690 % |
c ==============================================================================
c [1mFound solution: 25104663[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8994   maxlim: 85334697   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17095 |   91577   330669 |   30525   16943   118335     7.0 | 33.690 % |
c |     17196 |   91577   330669 |   33577   17044   119098     7.0 | 16.089 % |
c |     17347 |   91577   330669 |   36935   17195   120316     7.0 | 16.089 % |
c |     17573 |   91577   330669 |   40628   17421   122058     7.0 | 16.089 % |
c |     17911 |   91577   330669 |   44691   17759   125054     7.0 | 16.089 % |
c |     18418 |   91561   330617 |   49160   18264   129592     7.1 | 16.106 % |
c |     19179 |   91561   330617 |   54076   19025   142463     7.5 | 16.106 % |
c |     20319 |   91545   330565 |   59484   20159   155811     7.7 | 16.124 % |
c |     22027 |   91515   330467 |   65433   21862   174468     8.0 | 16.154 % |
c |     24590 |   91472   330328 |   71976   24418   215149     8.8 | 16.207 % |
c |     28435 |   91413   330137 |   79173   28250   746205    26.4 | 16.277 % |
c ==============================================================================
c [1mFound solution: 24134111[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 86305249   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29977 |   91442   330381 |   30480   29792   782235    26.3 | 16.277 % |
c |     30078 |   91442   330381 |   33528   29893   783284    26.2 | 16.332 % |
c |     30228 |   91442   330381 |   36880   30043   785078    26.1 | 16.332 % |
c |     30453 |   91442   330381 |   40568   30268   787880    26.0 | 16.332 % |
c |     30791 |   91426   330329 |   44625   30602   791420    25.9 | 16.349 % |
c |     31298 |   91426   330329 |   49088   31109   823355    26.5 | 16.349 % |
c |     32057 |   91426   330329 |   53997   31868   831299    26.1 | 16.349 % |
c ==============================================================================
c [1mFound solution: 19992720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 90446640   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33033 |   91446   330515 |   30482   32844   859817    26.2 | 16.349 % |
c |     33133 |   91446   330515 |   33530   32944   860809    26.1 | 16.394 % |
c |     33285 |   91446   330515 |   36883   33096   863008    26.1 | 16.394 % |
c |     33510 |   91446   330515 |   40571   33321   865829    26.0 | 16.394 % |
c |     33848 |   91446   330515 |   44628   33659   936428    27.8 | 16.394 % |
c |     34354 |   91446   330515 |   49091   34165   941407    27.6 | 16.394 % |
c |     35113 |   91446   330515 |   54000   34924  1113576    31.9 | 16.394 % |
c |     36252 |   91446   330515 |   59400   36063  1174258    32.6 | 16.394 % |
c |     37962 |   91446   330515 |   65340   37773  1188196    31.5 | 16.394 % |
c |     40524 |   91446   330515 |   71874   40335  1254580    31.1 | 16.394 % |
c |     44368 |   91446   330515 |   79062   44179  1331444    30.1 | 16.394 % |
c |     50134 |   91446   330515 |   86968   49945  1579317    31.6 | 16.394 % |
c |     58783 |   91446   330515 |   95665   58594  2193428    37.4 | 16.394 % |
c ==============================================================================
c [1mFound solution: 17991001[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 92448359   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61875 |   91462   330681 |   30487   61686  2262730    36.7 | 16.394 % |
c |     61976 |   91462   330681 |   33535   20692   720985    34.8 | 16.437 % |
c |     62126 |   91462   330681 |   36889   20842   721798    34.6 | 16.437 % |
c |     62351 |   91462   330681 |   40578   21067   723249    34.3 | 16.437 % |
c |     62688 |   91462   330681 |   44636   21404   725573    33.9 | 16.437 % |
c |     63195 |   91462   330681 |   49099   21911   730091    33.3 | 16.437 % |
c |     63954 |   91462   330681 |   54009   22670   743221    32.8 | 16.437 % |
c |     65093 |   91462   330681 |   59410   23809   752748    31.6 | 16.437 % |
c |     66801 |   91462   330681 |   65351   25517   770876    30.2 | 16.437 % |
c |     69363 |   91462   330681 |   71886   28079   934604    33.3 | 16.437 % |
c |     73209 |   91462   330681 |   79075   31925  1016552    31.8 | 16.437 % |
c |     78975 |   91462   330681 |   86982   37691  1141799    30.3 | 16.437 % |
c |     87624 |   91447   330628 |   95681   46337  1832044    39.5 | 16.443 % |
c |    100599 |   91447   330628 |  105249   59312  4968456    83.8 | 16.443 % |
c |    120062 |   91447   330628 |  115774   78775 11321886   143.7 | 16.443 % |
c |    149254 |   91440   330605 |  127351  107965 14336498   132.8 | 16.449 % |
c |    193043 |   91440   330605 |  140086   30970 10945496   353.4 | 16.449 % |
c |    258729 |   91440   330605 |  154095   96656 21010651   217.4 | 16.449 % |
c ==============================================================================
c [1mFound solution: 17787518[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 92651842   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    267748 |   91457   330771 |   30485  105675 21383017   202.3 | 16.449 % |
c |    267848 |   91457   330771 |   33533   24129  1481022    61.4 | 16.485 % |
c |    267998 |   91457   330771 |   36886   24279  1481772    61.0 | 16.485 % |
c |    268227 |   91457   330771 |   40575   24508  1484554    60.6 | 16.485 % |
c |    268564 |   91457   330771 |   44633   24845  1490074    60.0 | 16.485 % |
c |    269071 |   91457   330771 |   49096   25352  1496289    59.0 | 16.485 % |
c |    269830 |   91457   330771 |   54006   26111  1505139    57.6 | 16.485 % |
c |    270970 |   91457   330771 |   59406   27251  1524657    55.9 | 16.485 % |
c |    272680 |   91457   330771 |   65347   28961  1791209    61.8 | 16.485 % |
c |    275242 |   91457   330771 |   71882   31523  1964285    62.3 | 16.485 % |
c |    279086 |   91457   330771 |   79070   35367  2164193    61.2 | 16.485 % |
c |    284855 |   91457   330771 |   86977   41136  2354483    57.2 | 16.485 % |
c |    293504 |   91457   330771 |   95674   49785  3589922    72.1 | 16.485 % |
c ==============================================================================
c [1mFound solution: 17533648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 92905712   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    302641 |   91472   330943 |   30490   58922  4196646    71.2 | 16.485 % |
c |    302741 |   91472   330943 |   33539   23275   822059    35.3 | 16.526 % |
c |    302891 |   91472   330943 |   36892   23425   822961    35.1 | 16.526 % |
c |    303116 |   91472   330943 |   40582   23650   824492    34.9 | 16.526 % |
c |    303456 |   91472   330943 |   44640   23990   827061    34.5 | 16.526 % |
c |    303962 |   91472   330943 |   49104   24496   835238    34.1 | 16.526 % |
c |    304721 |   91472   330943 |   54014   25255   840835    33.3 | 16.526 % |
c |    305860 |   91472   330943 |   59416   26394   850849    32.2 | 16.526 % |
c |    307569 |   91472   330943 |   65358   28103   894544    31.8 | 16.526 % |
c |    310131 |   91472   330943 |   71893   30665  1031528    33.6 | 16.526 % |
c |    313975 |   91472   330943 |   79083   34509  1808280    52.4 | 16.526 % |
c |    319742 |   91472   330943 |   86991   40276  4231244   105.1 | 16.526 % |
c |    328392 |   91472   330943 |   95690   48926  4474831    91.5 | 16.526 % |
c |    341367 |   91467   330927 |  105259   61899  5974613    96.5 | 16.532 % |
c ==============================================================================
c [1mFound solution: 12415296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 98024064   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    341608 |   91485   331102 |   30495   62140  5990443    96.4 | 16.532 % |
c |    341708 |   91485   331102 |   33544   23038  1265737    54.9 | 16.584 % |
c |    341858 |   91485   331102 |   36898   23188  1266413    54.6 | 16.584 % |
c |    342083 |   91476   331071 |   40588   23405  1267848    54.2 | 16.590 % |
c |    342420 |   91476   331071 |   44647   23742  1270238    53.5 | 16.590 % |
c |    342929 |   91476   331071 |   49112   24251  1272946    52.5 | 16.590 % |
c |    343688 |   91476   331071 |   54023   25010  1278068    51.1 | 16.590 % |
c |    344827 |   91476   331071 |   59426   26149  1287667    49.2 | 16.590 % |
c |    346535 |   91476   331071 |   65368   27857  1422554    51.1 | 16.590 % |
c |    349097 |   91476   331071 |   71905   30419  1459136    48.0 | 16.590 % |
c |    352942 |   91476   331071 |   79096   34264  1751508    51.1 | 16.590 % |
c |    358708 |   91476   331071 |   87005   40030  2826584    70.6 | 16.590 % |
c |    367359 |   91476   331071 |   95706   48681  3837064    78.8 | 16.590 % |
c |    380333 |   91476   331071 |  105277   61655  5724606    92.8 | 16.590 % |
c |    399795 |   91476   331071 |  115804   81117  8743443   107.8 | 16.590 % |
c |    428987 |   91476   331071 |  127385  110309 16194504   146.8 | 16.590 % |
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 -Y0_bit0 -Y1_bit0 Y2_bit0 Y3_bit0 -Y4_bit0 -Y5_bit0 -Y6_bit0 Y7_bit0 -Y8_bit0 -Y9_bit0 -Y10_bit0 Y11_bit0 Y12_bit0 Y13_bit0 Y14_bit0 -Y15_bit0 -Y16_bit0 -Y17_bit0 -Y18_bit0 -Y19_bit0 Y20_bit0 -Y21_bit0 -Y22_bit0 Y23_bit0 Y24_bit0 -Y25_bit0 -Y26_bit0 Y27_bit0 -Y28_bit0 Y29_bit0 -Y30_bit0 -Y31_bit0 -Y32_bit0 -Y33_bit0 Y34_bit0 Y35_bit0 -Y36_bit0 Y37_bit0 -Y38_bit0 -Y39_bit0 Y40_bit0 -Y41_bit0 Y42_bit0 -Y43_bit0 -Y44_bit0 -Y45_bit0 -Y46_bit0 Y47_bit0 Y48_bit0 Y49_bit0 -Y50_bit0 -Y51_bit0 -Y52_bit0 -Y53_bit0 Y54_bit0 Y55_bit0 Y56_bit0 -Y57_bit0 -Y58_bit0 -Y59_bit0 -Y60_bit0 -Y61_bit0 Y62_bit0 -Y63_bit0 -Y64_bit0 -Y65_bit0 -Y66_bit0 Y67_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.60 0.85 0.88 2/54 30277
Raw data (stat): 30277 (runsolver) R 30276 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 473274292 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+10.0008 s]
Raw data (loadavg): 0.66 0.86 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 1302 0 0 0 995 3 0 0 25 0 1 0 473274292 6836224 1273 4294967295 134512640 134672761 3221224544 3221223696 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1669 1273 603 41 0 1628 0
vsize: 6676
[startup+20.0012 s]
Raw data (loadavg): 0.71 0.86 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 2624 0 0 0 1991 6 0 0 25 0 1 0 473274292 13320192 2553 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2553 603 41 0 3211 0
vsize: 13008
[startup+30.0016 s]
Raw data (loadavg): 0.76 0.87 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 3221 0 0 0 2990 8 0 0 25 0 1 0 473274292 15732736 3150 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3841 3150 603 41 0 3800 0
vsize: 15364
[startup+40.0024 s]
Raw data (loadavg): 0.79 0.87 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 3571 0 0 0 3989 9 0 0 25 0 1 0 473274292 17346560 3500 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4235 3500 603 41 0 4194 0
vsize: 16940
[startup+50.0025 s]
Raw data (loadavg): 0.82 0.87 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 3888 0 0 0 4989 9 0 0 25 0 1 0 473274292 18554880 3817 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4530 3817 603 41 0 4489 0
vsize: 18120
[startup+60.0029 s]
Raw data (loadavg): 0.85 0.88 0.88 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 4382 0 0 0 5987 11 0 0 25 0 1 0 473274292 20574208 4311 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5023 4311 603 41 0 4982 0
vsize: 20092
[startup+70.0035 s]
Raw data (loadavg): 0.87 0.88 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 5020 0 0 0 6983 14 0 0 25 0 1 0 473274292 23126016 4949 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5646 4949 603 41 0 5605 0
vsize: 22584
[startup+80.0029 s]
Raw data (loadavg): 0.89 0.89 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 5111 0 0 0 7983 15 0 0 25 0 1 0 473274292 23457792 5040 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5727 5040 603 41 0 5686 0
vsize: 22908
[startup+90.003 s]
Raw data (loadavg): 0.91 0.89 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 5111 0 0 0 8983 15 0 0 25 0 1 0 473274292 23457792 5040 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5727 5040 603 41 0 5686 0
vsize: 22908
[startup+100.003 s]
Raw data (loadavg): 0.92 0.89 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 5112 0 0 0 9983 15 0 0 25 0 1 0 473274292 23457792 5041 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5727 5041 603 41 0 5686 0
vsize: 22908
[startup+110.003 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 5112 0 0 0 10983 15 0 0 25 0 1 0 473274292 23457792 5041 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5727 5041 603 41 0 5686 0
vsize: 22908
[startup+120.003 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 5710 0 0 0 11982 16 0 0 25 0 1 0 473274292 25894912 5639 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6322 5639 603 41 0 6281 0
vsize: 25288
[startup+130.003 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 7236 0 0 0 12979 20 0 0 25 0 1 0 473274292 32247808 7165 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7873 7165 603 41 0 7832 0
vsize: 31492
[startup+140.004 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 8117 0 0 0 13976 23 0 0 25 0 1 0 473274292 35749888 8046 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8728 8046 603 41 0 8687 0
vsize: 34912
[startup+150.004 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 9047 0 0 0 14974 25 0 0 25 0 1 0 473274292 39649280 8976 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9680 8976 603 41 0 9639 0
vsize: 38720
[startup+160.005 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 9980 0 0 0 15972 27 0 0 25 0 1 0 473274292 43442176 9909 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10606 9910 603 41 0 10565 0
vsize: 42424
[startup+170.005 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 10949 0 0 0 16970 29 0 0 25 0 1 0 473274292 47640576 10878 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11631 10878 603 41 0 11590 0
vsize: 46524
[startup+180.005 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 11888 0 0 0 17968 31 0 0 25 0 1 0 473274292 51499008 11817 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12573 11817 603 41 0 12532 0
vsize: 50292
[startup+190.006 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 12799 0 0 0 18966 34 0 0 25 0 1 0 473274292 55287808 12728 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13498 12728 603 41 0 13457 0
vsize: 53992
[startup+200.005 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 13554 0 0 0 19964 36 0 0 25 0 1 0 473274292 58253312 13483 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14222 13483 603 41 0 14181 0
vsize: 56888
[startup+210.005 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 14112 0 0 0 20963 37 0 0 25 0 1 0 473274292 60547072 14041 4294967295 134512640 134672761 3221224544 3221223712 134559063 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14782 14041 603 41 0 14741 0
vsize: 59128
[startup+220.006 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 14543 0 0 0 21962 38 0 0 25 0 1 0 473274292 62296064 14472 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15209 14472 603 41 0 15168 0
vsize: 60836
[startup+230.006 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 14873 0 0 0 22960 40 0 0 25 0 1 0 473274292 63639552 14802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15537 14802 603 41 0 15496 0
vsize: 62148
[startup+240.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 15569 0 0 0 23958 43 0 0 25 0 1 0 473274292 66453504 15498 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16224 15498 603 41 0 16183 0
vsize: 64896
[startup+250.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 16272 0 0 0 24956 45 0 0 25 0 1 0 473274292 69275648 16201 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16913 16201 603 41 0 16872 0
vsize: 67652
[startup+260.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 16924 0 0 0 25955 46 0 0 25 0 1 0 473274292 71962624 16853 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17569 16853 603 41 0 17528 0
vsize: 70276
[startup+270.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 17525 0 0 0 26953 48 0 0 25 0 1 0 473274292 74391552 17454 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18162 17454 603 41 0 18121 0
vsize: 72648
[startup+280.006 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 17982 0 0 0 27952 49 0 0 25 0 1 0 473274292 76283904 17911 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18624 17911 603 41 0 18583 0
vsize: 74496
[startup+290.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 18514 0 0 0 28950 51 0 0 25 0 1 0 473274292 78446592 18443 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19152 18443 603 41 0 19111 0
vsize: 76608
[startup+300.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 19344 0 0 0 29947 54 0 0 25 0 1 0 473274292 81833984 19273 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19979 19273 603 41 0 19938 0
vsize: 79916
[startup+310.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 20268 0 0 0 30946 55 0 0 25 0 1 0 473274292 85561344 20197 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20889 20197 603 41 0 20848 0
vsize: 83556
[startup+320.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 21188 0 0 0 31943 58 0 0 25 0 1 0 473274292 89427968 21117 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21833 21117 603 41 0 21792 0
vsize: 87332
[startup+330.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 22034 0 0 0 32941 61 0 0 25 0 1 0 473274292 92786688 21963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22653 21963 603 41 0 22612 0
vsize: 90612
[startup+340.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 22907 0 0 0 33939 63 0 0 25 0 1 0 473274292 96419840 22836 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23540 22836 603 41 0 23499 0
vsize: 94160
[startup+350.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 23815 0 0 0 34937 65 0 0 25 0 1 0 473274292 100061184 23744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24429 23744 603 41 0 24388 0
vsize: 97716
[startup+360.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 24652 0 0 0 35936 67 0 0 25 0 1 0 473274292 103555072 24581 4294967295 134512640 134672761 3221224544 3221223672 1075347105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25282 24581 603 41 0 25241 0
vsize: 101128
[startup+370.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 25516 0 0 0 36933 69 0 0 25 0 1 0 473274292 107585536 25445 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26266 25445 603 41 0 26225 0
vsize: 105064
[startup+380.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 26366 0 0 0 37932 71 0 0 25 0 1 0 473274292 111022080 26295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27105 26295 603 41 0 27064 0
vsize: 108420
[startup+390.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 27129 0 0 0 38929 73 0 0 25 0 1 0 473274292 114249728 27058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27893 27058 603 41 0 27852 0
vsize: 111572
[startup+400.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 27907 0 0 0 39928 75 0 0 25 0 1 0 473274292 117350400 27836 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28650 27836 603 41 0 28609 0
vsize: 114600
[startup+410.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 28771 0 0 0 40927 77 0 0 25 0 1 0 473274292 120971264 28700 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29534 28700 603 41 0 29493 0
vsize: 118136
[startup+420.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 29534 0 0 0 41925 78 0 0 25 0 1 0 473274292 124067840 29463 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30290 29463 603 41 0 30249 0
vsize: 121160
[startup+430.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30297 0 0 0 42923 81 0 0 25 0 1 0 473274292 127160320 30226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31045 30226 603 41 0 31004 0
vsize: 124180
[startup+440.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 43922 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+450.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 44922 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223680 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+460.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 45922 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+470.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 46922 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+480.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 47922 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+490.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 48922 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+500.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 49923 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+510.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 50923 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+520.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 51925 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+530.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 52925 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+540.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 53925 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+550.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 54925 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+560.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 55925 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 56926 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 57926 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+590.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 58926 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+600.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 59926 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223728 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+610.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 60926 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+620.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 61926 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223728 134559356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+630.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30839 0 0 0 62926 82 0 0 25 0 1 0 473274292 129437696 30768 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31601 30768 603 41 0 31560 0
vsize: 126404
[startup+640.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30840 0 0 0 63926 82 0 0 25 0 1 0 473274292 129417216 30769 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31596 30769 603 41 0 31555 0
vsize: 126384
[startup+650.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30840 0 0 0 64925 82 0 0 25 0 1 0 473274292 129417216 30769 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31596 30769 603 41 0 31555 0
vsize: 126384
[startup+660.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30840 0 0 0 65926 82 0 0 25 0 1 0 473274292 129417216 30769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31596 30769 603 41 0 31555 0
vsize: 126384
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30840 0 0 0 66926 82 0 0 25 0 1 0 473274292 129417216 30769 4294967295 134512640 134672761 3221224544 3221223668 134566136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31596 30769 603 41 0 31555 0
vsize: 126384
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30840 0 0 0 67926 82 0 0 25 0 1 0 473274292 129417216 30769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31596 30769 603 41 0 31555 0
vsize: 126384
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30840 0 0 0 68926 82 0 0 25 0 1 0 473274292 129413120 30769 4294967295 134512640 134672761 3221224544 3221223680 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30769 603 41 0 31554 0
vsize: 126380
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 69926 82 0 0 25 0 1 0 473274292 129413120 30771 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30771 603 41 0 31554 0
vsize: 126380
[startup+710.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 70927 82 0 0 25 0 1 0 473274292 129413120 30771 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30771 603 41 0 31554 0
vsize: 126380
[startup+720.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 71927 82 0 0 25 0 1 0 473274292 129413120 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30771 603 41 0 31554 0
vsize: 126380
[startup+730.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 72927 83 0 0 25 0 1 0 473274292 129413120 30771 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30771 603 41 0 31554 0
vsize: 126380
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 73927 83 0 0 25 0 1 0 473274292 129413120 30771 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30771 603 41 0 31554 0
vsize: 126380
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 74927 83 0 0 25 0 1 0 473274292 129413120 30771 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30771 603 41 0 31554 0
vsize: 126380
[startup+760.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 75927 83 0 0 25 0 1 0 473274292 129413120 30771 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30771 603 41 0 31554 0
vsize: 126380
[startup+770.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 76928 83 0 0 25 0 1 0 473274292 129413120 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30771 603 41 0 31554 0
vsize: 126380
[startup+780.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 77928 83 0 0 25 0 1 0 473274292 129413120 30771 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31595 30771 603 41 0 31554 0
vsize: 126380
[startup+790.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 78928 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 79928 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+810.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 80928 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+820.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 81928 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 82928 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 83929 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+850.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 84929 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223728 134559514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+860.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 85929 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+870.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 86929 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+880.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 87929 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+890.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 88930 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+900.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 89930 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+910.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 90930 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+920.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 91930 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223808 134562492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+930.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 92930 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+940.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 93931 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+950.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 94931 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+960.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 95931 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+970.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 96931 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+980.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 97931 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+990.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 98932 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 99932 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 100932 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 101932 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 102932 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 103933 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 104933 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 105933 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 106933 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 107933 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 108934 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 109934 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 110934 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 111934 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 112934 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 113934 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30842 0 0 0 114935 83 0 0 25 0 1 0 473274292 129409024 30771 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30771 603 41 0 31553 0
vsize: 126376
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30844 0 0 0 115935 83 0 0 25 0 1 0 473274292 129409024 30773 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30773 603 41 0 31553 0
vsize: 126376
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30844 0 0 0 116935 83 0 0 25 0 1 0 473274292 129409024 30773 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30773 603 41 0 31553 0
vsize: 126376
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30844 0 0 0 117935 83 0 0 25 0 1 0 473274292 129409024 30773 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30773 603 41 0 31553 0
vsize: 126376
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30844 0 0 0 118936 83 0 0 25 0 1 0 473274292 129409024 30773 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30773 603 41 0 31553 0
vsize: 126376
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30277
Raw data (stat): 30277 (minisat+) R 30276 26667 26666 0 -1 0 30844 0 0 0 119936 83 0 0 25 0 1 0 473274292 129409024 30773 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31594 30773 603 41 0 31553 0
vsize: 126376
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30277
Raw data (stat): 30277 (minisat+) Z 30276 26667 26666 0 -1 12 30847 0 0 0 119936 89 0 0 25 0 1 0 473274292 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.12
CPU time (s): 1200.26
CPU user time (s): 1199.37
CPU system time (s): 0.893864
CPU usage (%): 100.012
Max. virtual memory (Kb): 126404
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####