PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc07.opb
MD5SUM	9cc94d1db4d494288ef67a8d5ad5d77e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1408128
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	11486079
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	280
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	253
Trace number 19123

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        346576 kB
Buffers:         31156 kB
Cached:         628152 kB
SwapCached:         20 kB
Active:         118700 kB
Inactive:       543248 kB
HighTotal:      131008 kB
HighFree:         7476 kB
LowTotal:       903652 kB
LowFree:        339100 kB
SwapTotal:     2097892 kB
SwapFree:      2097664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            20444 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:21:05 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 17015 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 243]---> BDD-cost:   51
c ---[ 241]---> BDD-cost:   51
c ---[ 239]---> BDD-cost:   51
c ---[ 237]---> BDD-cost:   51
c ---[ 235]---> BDD-cost:   51
c ---[ 233]---> BDD-cost:   51
c ---[ 231]---> BDD-cost:   51
c ---[ 230]---> BDD-cost:  239
c ---[ 229]---> BDD-cost:  239
c ---[ 228]---> BDD-cost:  239
c ---[  99]---> Sorter-cost:  127     Base:
c ---[  97]---> Sorter-cost:  127     Base:
c ---[  95]---> Sorter-cost:  127     Base:
c ---[  93]---> Sorter-cost:  127     Base:
c ---[  91]---> Sorter-cost:  127     Base:
c ---[  89]---> Sorter-cost:  127     Base:
c ---[  87]---> Sorter-cost:  127     Base:
c ---[  85]---> Sorter-cost:  127     Base:
c ---[  83]---> Sorter-cost:  127     Base:
c ---[  81]---> Sorter-cost:  127     Base:
c ---[  79]---> Sorter-cost:  127     Base:
c ---[  77]---> Sorter-cost:  127     Base:
c ---[  75]---> Sorter-cost:  127     Base:
c ---[  73]---> Sorter-cost:  127     Base:
c ---[  71]---> Sorter-cost:  127     Base:
c ---[  69]---> Sorter-cost:  127     Base:
c ---[  67]---> Sorter-cost:  127     Base:
c ---[  65]---> Sorter-cost:  127     Base:
c ---[  63]---> Sorter-cost:  127     Base:
c ---[  61]---> Sorter-cost:  127     Base:
c ---[  59]---> Sorter-cost:  127     Base:
c ---[  57]---> Sorter-cost:  127     Base:
c ---[  55]---> Sorter-cost:  127     Base:
c ---[  53]---> Sorter-cost:  127     Base:
c ---[  51]---> Sorter-cost:  127     Base:
c ---[  49]---> Sorter-cost:  127     Base:
c ---[  47]---> Sorter-cost:  127     Base:
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   50
c ---[  34]---> BDD-cost:   50
c ---[  33]---> BDD-cost:   50
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   48
c ---[  28]---> BDD-cost:   48
c ---[  27]---> BDD-cost:   48
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   50
c ---[  22]---> BDD-cost:   50
c ---[  21]---> BDD-cost:   50
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   48
c ---[  16]---> BDD-cost:   48
c ---[  15]---> BDD-cost:   48
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   50
c ---[  10]---> BDD-cost:   50
c ---[   9]---> BDD-cost:   50
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:   48
c ---[   3]---> BDD-cost:   48
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   25920    84925 |    7775       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6727          
c   -- var.elim.:  2000/6727          
c   -- var.elim.:  3000/6727          
c   -- var.elim.:  4000/6727          
c   -- var.elim.:  5000/6727          
c   -- var.elim.:  6000/6727          
c   -- var.elim.:  6727/6727          
c   -- var.elim.:  1000/1675          
c   -- var.elim.:  1675/1675          
c   -- var.elim.:  27/27          
c   -- subsuming                       
c   -- var.elim.:  158/158          
c   -- var.elim.:  152/152          
c   -- subsuming                       
c   -- var.elim.:  30/30          
c |         0 |   24670    85296 |      --       0       --      -- |     --   | -1097/1311
c |         0 |   24670    85296 |    9868       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.36879 s)
c ==============================================================================
c [1mFound solution: 1530368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        95 |   24682    85327 |    7404      95     7100    74.7 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  19/19          
c   -- var.elim.:  12/12          
c |        95 |   24675    85325 |      --      95       --      -- |     --   | -7/-1
c |        95 |   24675    85325 |    9870      95     7100    74.7 |  0.000 % |
c |       200 |   24662    85280 |   10851     199    13634    68.5 |  3.385 % |
c |       352 |   24662    85280 |   11936     351    31569    89.9 |  3.385 % |
c |       577 |   24570    84936 |   13081     572    33734    59.0 |  3.542 % |
c |       915 |   24562    84906 |   14384     906    86613    95.6 |  3.560 % |
c |      1423 |   24562    84906 |   15822    1414   128085    90.6 |  3.560 % |
c |      2182 |   24562    84906 |   17405    2173   216933    99.8 |  3.560 % |
c |      3322 |   24562    84906 |   19145    3313   415241   125.3 |  3.560 % |
c ==============================================================================
c (current CPU-time: 5.96509 s)
c ==============================================================================
c [1mFound solution: 1519488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3786 |   24549    84850 |    7364    3769   454493   120.6 |  3.560 % |
c   -- subsuming                       
c   -- var.elim.:  123/123          
c   -- var.elim.:  82/82          
c   -- var.elim.:  24/24          
c |      3786 |   24510    84757 |      --    3769       --      -- |     --   | -39/-92
c |      3786 |   24510    84757 |    9804    3185   322388   101.2 |  3.560 % |
c |      3887 |   24510    84757 |   10784    3286   341749   104.0 |  3.672 % |
c |      4039 |   24510    84757 |   11862    3438   347056   100.9 |  3.672 % |
c |      4265 |   24510    84757 |   13049    3664   373896   102.0 |  3.672 % |
c |      4602 |   24464    84589 |   14327    3997   406393   101.7 |  3.777 % |
c |      5109 |   24464    84589 |   15759    4504   446777    99.2 |  3.777 % |
c |      5868 |   24454    84554 |   17328    5261   510997    97.1 |  3.794 % |
c |      7008 |   24398    84321 |   19017    6396   667222   104.3 |  3.829 % |
c ==============================================================================
c (current CPU-time: 11.0103 s)
c ==============================================================================
c [1mFound solution: 1470208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8149 |   24409    84351 |    7322    7537   773576   102.6 |  3.829 % |
c   -- subsuming                       
c   -- var.elim.:  111/111          
c   -- var.elim.:  46/46          
c |      8149 |   24390    84286 |      --    7537       --      -- |     --   | -19/-64
c |      8149 |   24390    84286 |    9756    7127   675346    94.8 |  3.829 % |
c |      8249 |   24390    84286 |   10731    7227   682232    94.4 |  3.850 % |
c |      8401 |   24390    84286 |   11804    7379   694790    94.2 |  3.850 % |
c |      8626 |   24378    84237 |   12978    7602   722136    95.0 |  3.867 % |
c |      8964 |   24378    84237 |   14276    7940   762119    96.0 |  3.867 % |
c |      9471 |   24378    84237 |   15704    8447   800454    94.8 |  3.867 % |
c |     10232 |   24371    84209 |   17269    9207   944158   102.5 |  3.885 % |
c |     11373 |   24319    84016 |   18956   10345  1129551   109.2 |  3.990 % |
c |     13084 |   24293    83906 |   20829   12047  1311111   108.8 |  4.007 % |
c |     15646 |   24293    83906 |   22912   14609  1720728   117.8 |  4.007 % |
c |     19493 |   24268    83805 |   25177   18453  2405494   130.4 |  4.025 % |
c ==============================================================================
c (current CPU-time: 32.4291 s)
c ==============================================================================
c [1mFound solution: 1442688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20742 |   24219    83595 |    7265   19693  2596265   131.8 |  4.025 % |
c   -- subsuming                       
c   -- var.elim.:  160/160          
c   -- var.elim.:  76/76          
c   -- var.elim.:  15/15          
c |     20742 |   24186    83523 |      --   19693       --      -- |     --   | -33/-71
c |     20742 |   24186    83523 |    9674   19693  2596265   131.8 |  4.025 % |
c ==============================================================================
c (current CPU-time: 32.997 s)
c ==============================================================================
c [1mFound solution: 1435648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20796 |   24195    83547 |    7258    7489   748906   100.0 |  4.025 % |
c   -- subsuming                       
c   -- var.elim.:  34/34          
c   -- var.elim.:  23/23          
c |     20796 |   24177    83489 |      --    7489       --      -- |     --   | -18/-57
c |     20796 |   24177    83489 |    9670    7489   748906   100.0 |  4.025 % |
c |     20896 |   24177    83489 |   10637    7589   762439   100.5 |  4.174 % |
c |     21046 |   24177    83489 |   11701    7739   781012   100.9 |  4.174 % |
c |     21274 |   24177    83489 |   12871    7967   787235    98.8 |  4.174 % |
c |     21612 |   24177    83489 |   14159    8305   824235    99.2 |  4.174 % |
c |     22118 |   24177    83489 |   15574    8811   903265   102.5 |  4.174 % |
c |     22877 |   24177    83489 |   17132    9570  1016480   106.2 |  4.174 % |
c |     24018 |   24177    83489 |   18845   10711  1179878   110.2 |  4.174 % |
c |     25726 |   24177    83489 |   20730   12419  1442138   116.1 |  4.174 % |
c |     28292 |   24108    83194 |   22738   14979  1923792   128.4 |  4.209 % |
c |     32136 |   24077    83080 |   24979   18814  2554960   135.8 |  4.279 % |
c |     37902 |   24070    83052 |   27469   24579  3900468   158.7 |  4.297 % |
c |     46551 |   24040    82935 |   30179   19775  3242861   164.0 |  4.349 % |
c ==============================================================================
c (current CPU-time: 89.7364 s)
c ==============================================================================
c [1mFound solution: 1434368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     46602 |   24052    82966 |    7215   19826  3252242   164.0 |  4.349 % |
c   -- subsuming                       
c   -- var.elim.:  118/118          
c   -- var.elim.:  87/87          
c   -- var.elim.:  18/18          
c |     46602 |   24013    82888 |      --   19826       --      -- |     --   | -39/-77
c |     46602 |   24013    82888 |    9605   12586  1115139    88.6 |  4.349 % |
c |     46703 |   23962    82684 |   10543    8491   627502    73.9 |  4.464 % |
c |     46853 |   23962    82684 |   11597    8641   654177    75.7 |  4.464 % |
c |     47078 |   23962    82684 |   12757    8866   672660    75.9 |  4.464 % |
c |     47415 |   23962    82684 |   14033    9203   724353    78.7 |  4.464 % |
c |     47924 |   23962    82684 |   15436    9712   777151    80.0 |  4.464 % |
c |     48685 |   23962    82684 |   16980   10473   894697    85.4 |  4.464 % |
c |     49825 |   23962    82684 |   18678   11613  1036196    89.2 |  4.464 % |
c |     51533 |   23928    82562 |   20516   13313  1285763    96.6 |  4.534 % |
c |     54095 |   23928    82562 |   22568   15875  1765843   111.2 |  4.534 % |
c |     57942 |   23928    82562 |   24825   19722  2463086   124.9 |  4.534 % |
c |     63708 |   23928    82562 |   27307   25488  3967922   155.7 |  4.534 % |
c ==============================================================================
c (current CPU-time: 138.71 s)
c ==============================================================================
c [1mFound solution: 1431808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     67360 |   23941    82595 |    7182   15784  2859362   181.2 |  4.534 % |
c   -- subsuming                       
c   -- var.elim.:  101/101          
c   -- var.elim.:  69/69          
c   -- subsuming                       
c   -- var.elim.:  6/6          
c |     67360 |   23918    82555 |      --   15784       --      -- |     --   | -23/-39
c |     67360 |   23918    82555 |    9567   12598  1309434   103.9 |  4.534 % |
c |     67461 |   23918    82555 |   10523    8500   702635    82.7 |  4.559 % |
c |     67611 |   23918    82555 |   11576    8650   711704    82.3 |  4.559 % |
c |     67837 |   23918    82555 |   12733    8876   724245    81.6 |  4.559 % |
c |     68176 |   23918    82555 |   14007    9215   758780    82.3 |  4.559 % |
c |     68682 |   23908    82516 |   15401    9719   803897    82.7 |  4.577 % |
c |     69441 |   23885    82431 |   16925   10476   889022    84.9 |  4.612 % |
c |     70580 |   23878    82403 |   18612   11614  1100422    94.7 |  4.629 % |
c |     72288 |   23878    82403 |   20473   13322  1453845   109.1 |  4.629 % |
c |     74850 |   23868    82364 |   22511   15883  1947472   122.6 |  4.647 % |
c |     78695 |   23868    82364 |   24762   19728  2541909   128.8 |  4.647 % |
c |     84465 |   23820    82169 |   27184   25491  3827853   150.2 |  4.700 % |
c |     93114 |   23811    82136 |   29891   22041  3471888   157.5 |  4.717 % |
c |    106088 |   23751    81903 |   32797   19984  2517627   126.0 |  4.788 % |
c |    125551 |   23751    81903 |   36077   21712  3591541   165.4 |  4.788 % |
c |    154743 |   23729    81818 |   39648   28599  5051023   176.6 |  4.823 % |
c ==============================================================================
c (current CPU-time: 368.366 s)
c ==============================================================================
c [1mFound solution: 1421568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    159780 |   23744    81854 |    7123   33636  6292350   187.1 |  4.823 % |
c   -- subsuming                       
c   -- var.elim.:  170/170          
c   -- var.elim.:  89/89          
c   -- subsuming                       
c   -- var.elim.:  19/19          
c   -- var.elim.:  9/9          
c |    159780 |   23708    81770 |      --   33636       --      -- |     --   | -36/-83
c |    159780 |   23708    81770 |    9483   26510  3857460   145.5 |  4.823 % |
c |    159881 |   23708    81770 |   10431    9351   808079    86.4 |  4.854 % |
c |    160031 |   23708    81770 |   11474    9501   834337    87.8 |  4.854 % |
c |    160259 |   23708    81770 |   12622    9729   849181    87.3 |  4.854 % |
c |    160596 |   23708    81770 |   13884   10066   934166    92.8 |  4.854 % |
c |    161108 |   23674    81639 |   15250   10574   990085    93.6 |  4.906 % |
c |    161869 |   23605    81375 |   16727   11331  1112134    98.1 |  5.048 % |
c |    163010 |   23596    81347 |   18392   12455  1331587   106.9 |  5.083 % |
c |    164718 |   23596    81347 |   20232   14163  1594434   112.6 |  5.083 % |
c ==============================================================================
c (current CPU-time: 381.231 s)
c ==============================================================================
c [1mFound solution: 1419008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    165504 |   23611    81384 |    7083   14949  1735342   116.1 |  5.083 % |
c   -- subsuming                       
c   -- var.elim.:  100/100          
c   -- var.elim.:  80/80          
c   -- subsuming                       
c   -- var.elim.:  31/31          
c   -- var.elim.:  18/18          
c |    165504 |   23572    81324 |      --   14949       --      -- |     --   | -39/-59
c |    165504 |   23572    81324 |    9428   11283   635964    56.4 |  5.083 % |
c |    165605 |   23572    81324 |   10371    7623   347831    45.6 |  5.115 % |
c |    165758 |   23572    81324 |   11408    7776   365415    47.0 |  5.115 % |
c |    165984 |   23522    81127 |   12523    7998   397191    49.7 |  5.186 % |
c |    166324 |   23522    81127 |   13775    8338   426547    51.2 |  5.186 % |
c |    166831 |   23522    81127 |   15152    8845   496229    56.1 |  5.186 % |
c |    167591 |   23522    81127 |   16668    9605   619217    64.5 |  5.186 % |
c |    168730 |   23522    81127 |   18335   10744   882604    82.1 |  5.186 % |
c |    170440 |   23522    81127 |   20168   12454  1276764   102.5 |  5.186 % |
c |    173002 |   23522    81127 |   22185   15016  1814104   120.8 |  5.186 % |
c |    176846 |   23475    80943 |   24355   18855  2452632   130.1 |  5.274 % |
c |    182612 |   23454    80865 |   26766   24613  3308107   134.4 |  5.327 % |
c |    191261 |   23454    80865 |   29443   21457  2930376   136.6 |  5.327 % |
c |    204236 |   23454    80865 |   32387   21331  3807968   178.5 |  5.327 % |
c |    223698 |   23454    80865 |   35626   22484  4125969   183.5 |  5.327 % |
c |    252891 |   23423    80755 |   39137   30503  6593060   216.1 |  5.398 % |
c ==============================================================================
c (current CPU-time: 669.053 s)
c ==============================================================================
c [1mFound solution: 1408128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    255887 |   23419    80719 |    7025   33497  7290673   217.7 |  5.398 % |
c   -- subsuming                       
c   -- var.elim.:  165/165          
c   -- var.elim.:  120/120          
c   -- subsuming                       
c   -- var.elim.:  21/21          
c   -- var.elim.:  17/17          
c |    255887 |   23384    80697 |      --   33497       --      -- |     --   | -35/-21
c |    255887 |   23384    80697 |    9353   16941  1117480    66.0 |  5.398 % |
c |    255988 |   23384    80697 |   10288    7379   304582    41.3 |  5.452 % |
c |    256138 |   23384    80697 |   11317    7529   326594    43.4 |  5.452 % |
c |    256363 |   23370    80644 |   12442    7753   339649    43.8 |  5.470 % |
c |    256705 |   23370    80644 |   13686    8095   356667    44.1 |  5.470 % |
c |    257211 |   23370    80644 |   15055    8601   441716    51.4 |  5.470 % |
c |    257971 |   23370    80644 |   16560    9361   596239    63.7 |  5.470 % |
c |    259112 |   23370    80644 |   18216   10502   739938    70.5 |  5.470 % |
c |    260821 |   23370    80644 |   20038   12211  1018820    83.4 |  5.470 % |
c |    263385 |   23370    80644 |   22042   14775  1540549   104.3 |  5.470 % |
c |    267230 |   23370    80644 |   24246   18620  2502246   134.4 |  5.470 % |
c |    272998 |   23370    80644 |   26670   24388  4526016   185.6 |  5.470 % |
c |    281647 |   23370    80644 |   29338   22395  4946959   220.9 |  5.470 % |
c |    294624 |   23370    80644 |   32271   22156  4900612   221.2 |  5.470 % |
c |    314085 |   23344    80545 |   35459   24871  4993045   200.8 |  5.523 % |
c |    343277 |   23287    80319 |   38910   35659  7956215   223.1 |  5.576 % |
c |    387066 |   23287    80319 |   42801   34386  7737309   225.0 |  5.576 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -COL260_bit_7 -COL260_bit_6 -COL260_bit_5 -COL260_bit_4 -COL260_bit_3 -COL260_bit_2 -COL260_bit_1 COL260_bit0 -COL260_bit1 -COL260_bit2 COL260_bit3 COL260_bit4 COL260_bit5 COL260_bit6 COL260_bit7 -COL260_bit8 COL260_bit9 -COL260_bit10 COL260_bit11 -COL260_bit12 COL260_bit13 -COL001_bit0 -COL002_bit0 -COL003_bit0 -COL004_bit0 -COL005_bit0 COL006_bit0 -COL007_bit0 -COL008_bit0 -COL009_bit0 -COL010_bit0 -COL011_bit0 -COL012_bit0 -COL013_bit0 -COL014_bit0 -COL015_bit0 -COL016_bit0 -COL017_bit0 -COL018_bit0 -COL019_bit0 -COL020_bit0 -COL021_bit0 -COL022_bit0 -COL023_bit0 -COL024_bit0 -COL025_bit0 -COL026_bit0 -COL027_bit0 -COL028_bit0 -COL029_bit0 -COL030_bit0 -COL031_bit0 -COL032_bit0 -COL033_bit0 -COL034_bit0 -COL035_bit0 COL036_bit0 -COL037_bit0 -COL038_bit0 -COL039_bit0 -COL040_bit0 -COL041_bit0 -COL042_bit0 -COL043_bit0 -COL044_bit0 -COL045_bit0 -COL046#### 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.96 1.00 0.93 2/54 5482
Raw data (stat): 5482 (runsolver) R 5481 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547075373 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.0012 s]
Raw data (loadavg): 0.96 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 2899 0 0 0 992 7 0 0 25 0 1 0 547075373 11579392 2392 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2827 2392 603 41 0 2786 0
vsize: 11308
[startup+20.0013 s]
Raw data (loadavg): 0.97 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 3889 0 0 0 1988 10 0 0 25 0 1 0 547075373 15093760 3251 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3685 3251 603 41 0 3644 0
vsize: 14740
[startup+30.001 s]
Raw data (loadavg): 0.97 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 5037 0 0 0 2986 12 0 0 25 0 1 0 547075373 19808256 4399 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4836 4399 603 41 0 4795 0
vsize: 19344
[startup+40.001 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 5556 0 0 0 3984 14 0 0 25 0 1 0 547075373 20561920 4586 4294967295 134512640 134672761 3221224544 3221223688 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5020 4586 603 41 0 4979 0
vsize: 20080
[startup+50.0014 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 5556 0 0 0 4984 14 0 0 25 0 1 0 547075373 20561920 4586 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5020 4586 603 41 0 4979 0
vsize: 20080
[startup+60.0011 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 5994 0 0 0 5984 14 0 0 25 0 1 0 547075373 22396928 5024 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5468 5025 603 41 0 5427 0
vsize: 21872
[startup+70.0011 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 6932 0 0 0 6981 17 0 0 25 0 1 0 547075373 26226688 5962 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6403 5962 603 41 0 6362 0
vsize: 25612
[startup+80.0005 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 7444 0 0 0 7980 19 0 0 25 0 1 0 547075373 28336128 6474 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6918 6474 603 41 0 6877 0
vsize: 27672
[startup+90.0004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 7685 0 0 0 8979 20 0 0 25 0 1 0 547075373 28479488 6526 4294967295 134512640 134672761 3221224544 3221222876 134642779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6953 6526 603 41 0 6912 0
vsize: 27812
[startup+100 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 7689 0 0 0 9978 20 0 0 25 0 1 0 547075373 28676096 6530 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7001 6530 603 41 0 6960 0
vsize: 28004
[startup+110.001 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 7689 0 0 0 10979 20 0 0 25 0 1 0 547075373 28676096 6530 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7001 6530 603 41 0 6960 0
vsize: 28004
[startup+120 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 7689 0 0 0 11978 20 0 0 25 0 1 0 547075373 28676096 6530 4294967295 134512640 134672761 3221224544 3221223708 134614558 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7001 6530 603 41 0 6960 0
vsize: 28004
[startup+130 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 7689 0 0 0 12978 21 0 0 25 0 1 0 547075373 28676096 6530 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7001 6530 603 41 0 6960 0
vsize: 28004
[startup+140.001 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8300 0 0 0 13977 23 0 0 25 0 1 0 547075373 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6901 603 41 0 7298 0
vsize: 29356
[startup+150.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8300 0 0 0 14976 23 0 0 25 0 1 0 547075373 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6901 603 41 0 7298 0
vsize: 29356
[startup+160.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8300 0 0 0 15975 23 0 0 25 0 1 0 547075373 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7339 6901 603 41 0 7298 0
vsize: 29356
[startup+170.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8300 0 0 0 16975 24 0 0 25 0 1 0 547075373 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7339 6901 603 41 0 7298 0
vsize: 29356
[startup+180.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8300 0 0 0 17976 24 0 0 25 0 1 0 547075373 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7339 6901 603 41 0 7298 0
vsize: 29356
[startup+190.003 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8300 0 0 0 18976 24 0 0 25 0 1 0 547075373 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7339 6901 603 41 0 7298 0
vsize: 29356
[startup+200.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8300 0 0 0 19976 24 0 0 25 0 1 0 547075373 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7339 6901 603 41 0 7298 0
vsize: 29356
[startup+210.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8300 0 0 0 20976 24 0 0 25 0 1 0 547075373 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7339 6901 603 41 0 7298 0
vsize: 29356
[startup+220.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8455 0 0 0 21976 24 0 0 25 0 1 0 547075373 30724096 7056 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7501 7056 603 41 0 7460 0
vsize: 30004
[startup+230.001 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8714 0 0 0 22975 25 0 0 25 0 1 0 547075373 31752192 7315 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7752 7315 603 41 0 7711 0
vsize: 31008
[startup+240.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8714 0 0 0 23975 26 0 0 25 0 1 0 547075373 31752192 7315 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7752 7315 603 41 0 7711 0
vsize: 31008
[startup+250.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 8714 0 0 0 24975 26 0 0 25 0 1 0 547075373 31752192 7315 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7752 7315 603 41 0 7711 0
vsize: 31008
[startup+260.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 9027 0 0 0 25974 26 0 0 25 0 1 0 547075373 33198080 7628 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8105 7628 603 41 0 8064 0
vsize: 32420
[startup+270.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 9296 0 0 0 26974 27 0 0 25 0 1 0 547075373 34246656 7894 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7894 603 41 0 8320 0
vsize: 33444
[startup+280.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 9296 0 0 0 27974 27 0 0 25 0 1 0 547075373 34246656 7894 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7894 603 41 0 8320 0
vsize: 33444
[startup+290.003 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5484
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 9296 0 0 0 28974 27 0 0 25 0 1 0 547075373 34246656 7894 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7894 603 41 0 8320 0
vsize: 33444
[startup+300.002 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 9581 0 0 0 29974 28 0 0 25 0 1 0 547075373 35426304 8179 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8179 603 41 0 8608 0
vsize: 34596
[startup+310.003 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 10295 0 0 0 30971 30 0 0 25 0 1 0 547075373 38457344 8893 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9389 8893 603 41 0 9348 0
vsize: 37556
[startup+320.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11060 0 0 0 31969 33 0 0 25 0 1 0 547075373 41488384 9658 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10129 9658 603 41 0 10088 0
vsize: 40516
[startup+330.003 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11231 0 0 0 32969 33 0 0 25 0 1 0 547075373 41992192 9790 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10252 9790 603 41 0 10211 0
vsize: 41008
[startup+340.003 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11231 0 0 0 33969 33 0 0 25 0 1 0 547075373 41992192 9790 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10252 9790 603 41 0 10211 0
vsize: 41008
[startup+350.003 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11231 0 0 0 34969 33 0 0 25 0 1 0 547075373 41992192 9790 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10252 9790 603 41 0 10211 0
vsize: 41008
[startup+360.003 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11231 0 0 0 35969 33 0 0 25 0 1 0 547075373 41992192 9790 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10252 9790 603 41 0 10211 0
vsize: 41008
[startup+370.003 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11363 0 0 0 36969 33 0 0 25 0 1 0 547075373 41984000 9796 4294967295 134512640 134672761 3221224544 3221223640 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10250 9796 603 41 0 10209 0
vsize: 41000
[startup+380.003 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11363 0 0 0 37969 34 0 0 25 0 1 0 547075373 41984000 9796 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9796 603 41 0 10209 0
vsize: 41000
[startup+390.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 38968 34 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+400.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 39968 34 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+410.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 40968 34 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+420.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 41968 34 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+430.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 42968 34 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+440.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 43969 34 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+450.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 44969 34 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+460.005 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 45969 34 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+470.005 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 46969 35 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+480.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 47969 35 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+490.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11535 0 0 0 48969 35 0 0 25 0 1 0 547075373 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+500.005 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11536 0 0 0 49969 35 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+510.005 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11536 0 0 0 50969 35 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+520.005 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11536 0 0 0 51969 35 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+530.005 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11536 0 0 0 52969 35 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+540.005 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11536 0 0 0 53969 35 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+550.005 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11571 0 0 0 54969 35 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+560.006 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11571 0 0 0 55970 36 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+570.006 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11571 0 0 0 56970 36 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+580.006 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11571 0 0 0 57970 36 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+590.007 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11571 0 0 0 58970 36 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+600.007 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 11571 0 0 0 59970 36 0 0 25 0 1 0 547075373 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 9799 603 41 0 10209 0
vsize: 41000
[startup+610.007 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12280 0 0 0 60969 37 0 0 25 0 1 0 547075373 45006848 10508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10988 10508 603 41 0 10947 0
vsize: 43952
[startup+620.007 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12371 0 0 0 61969 37 0 0 25 0 1 0 547075373 45113344 10562 4294967295 134512640 134672761 3221224544 3221223744 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11014 10562 603 41 0 10973 0
vsize: 44056
[startup+630.007 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12371 0 0 0 62970 37 0 0 25 0 1 0 547075373 45113344 10562 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11014 10562 603 41 0 10973 0
vsize: 44056
[startup+640.008 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12371 0 0 0 63970 37 0 0 25 0 1 0 547075373 45113344 10562 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11014 10562 603 41 0 10973 0
vsize: 44056
[startup+650.007 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12371 0 0 0 64970 37 0 0 25 0 1 0 547075373 45113344 10562 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11014 10562 603 41 0 10973 0
vsize: 44056
[startup+660.008 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12371 0 0 0 65970 37 0 0 25 0 1 0 547075373 45113344 10562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11014 10562 603 41 0 10973 0
vsize: 44056
[startup+670.009 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 66970 37 0 0 25 0 1 0 547075373 45092864 10559 4294967295 134512640 134672761 3221224544 3221223760 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11009 10559 603 41 0 10968 0
vsize: 44036
[startup+680.008 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 67969 38 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+690.008 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 68969 38 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+700.009 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 69969 38 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+710.01 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 70969 38 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+720.009 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 71969 38 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+730.009 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 72969 39 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+740.009 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 73969 39 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+750.009 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 74969 39 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+760.01 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 75969 39 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+770.01 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 76969 39 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+780.01 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12535 0 0 0 77969 39 0 0 25 0 1 0 547075373 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+790.01 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12555 0 0 0 78969 39 0 0 25 0 1 0 547075373 45223936 10574 4294967295 134512640 134672761 3221224544 3221223640 134616279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11041 10574 603 41 0 11000 0
vsize: 44164
[startup+800.011 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12555 0 0 0 79970 39 0 0 25 0 1 0 547075373 45158400 10574 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11025 10574 603 41 0 10984 0
vsize: 44100
[startup+810.012 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12555 0 0 0 80970 39 0 0 25 0 1 0 547075373 45158400 10574 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11025 10574 603 41 0 10984 0
vsize: 44100
[startup+820.011 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12555 0 0 0 81970 39 0 0 25 0 1 0 547075373 45158400 10574 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11025 10574 603 41 0 10984 0
vsize: 44100
[startup+830.011 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12555 0 0 0 82970 39 0 0 25 0 1 0 547075373 45158400 10574 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11025 10574 603 41 0 10984 0
vsize: 44100
[startup+840.012 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12555 0 0 0 83970 39 0 0 25 0 1 0 547075373 45158400 10574 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11025 10574 603 41 0 10984 0
vsize: 44100
[startup+850.011 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12555 0 0 0 84970 39 0 0 25 0 1 0 547075373 45158400 10574 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11025 10574 603 41 0 10984 0
vsize: 44100
[startup+860.012 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12555 0 0 0 85971 39 0 0 25 0 1 0 547075373 45158400 10574 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11025 10574 603 41 0 10984 0
vsize: 44100
[startup+870.013 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12817 0 0 0 86970 40 0 0 25 0 1 0 547075373 46088192 10802 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10802 603 41 0 11211 0
vsize: 45008
[startup+880.013 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12817 0 0 0 87970 40 0 0 25 0 1 0 547075373 46088192 10802 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10802 603 41 0 11211 0
vsize: 45008
[startup+890.013 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12817 0 0 0 88970 40 0 0 25 0 1 0 547075373 46088192 10802 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10802 603 41 0 11211 0
vsize: 45008
[startup+900.014 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12819 0 0 0 89970 40 0 0 25 0 1 0 547075373 46088192 10804 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10804 603 41 0 11211 0
vsize: 45008
[startup+910.015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12819 0 0 0 90971 41 0 0 25 0 1 0 547075373 46088192 10804 4294967295 134512640 134672761 3221224544 3221223584 134612625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10804 603 41 0 11211 0
vsize: 45008
[startup+920.014 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12819 0 0 0 91971 41 0 0 25 0 1 0 547075373 46088192 10804 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10804 603 41 0 11211 0
vsize: 45008
[startup+930.014 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12819 0 0 0 92971 41 0 0 25 0 1 0 547075373 46088192 10804 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10804 603 41 0 11211 0
vsize: 45008
[startup+940.015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 12819 0 0 0 93971 41 0 0 25 0 1 0 547075373 46088192 10804 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10804 603 41 0 11211 0
vsize: 45008
[startup+950.015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13148 0 0 0 94970 42 0 0 25 0 1 0 547075373 47546368 11133 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11608 11133 603 41 0 11567 0
vsize: 46432
[startup+960.015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13529 0 0 0 95969 43 0 0 25 0 1 0 547075373 49139712 11514 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11997 11514 603 41 0 11956 0
vsize: 47988
[startup+970.016 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13812 0 0 0 96969 44 0 0 25 0 1 0 547075373 50036736 11761 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11761 603 41 0 12175 0
vsize: 48864
[startup+980.015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13812 0 0 0 97969 44 0 0 25 0 1 0 547075373 50036736 11761 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11761 603 41 0 12175 0
vsize: 48864
[startup+990.015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13812 0 0 0 98969 44 0 0 25 0 1 0 547075373 50036736 11761 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11761 603 41 0 12175 0
vsize: 48864
[startup+1000.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13812 0 0 0 99969 44 0 0 25 0 1 0 547075373 50036736 11761 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11761 603 41 0 12175 0
vsize: 48864
[startup+1010.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13812 0 0 0 100969 44 0 0 25 0 1 0 547075373 50036736 11761 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11761 603 41 0 12175 0
vsize: 48864
[startup+1020.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13812 0 0 0 101969 44 0 0 25 0 1 0 547075373 50036736 11761 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11761 603 41 0 12175 0
vsize: 48864
[startup+1030.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13812 0 0 0 102969 44 0 0 25 0 1 0 547075373 50036736 11761 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11761 603 41 0 12175 0
vsize: 48864
[startup+1040.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13813 0 0 0 103969 44 0 0 25 0 1 0 547075373 50036736 11762 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11762 603 41 0 12175 0
vsize: 48864
[startup+1050.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13813 0 0 0 104970 44 0 0 25 0 1 0 547075373 50036736 11762 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11762 603 41 0 12175 0
vsize: 48864
[startup+1060.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13852 0 0 0 105970 44 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1070.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13852 0 0 0 106970 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1080.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13852 0 0 0 107970 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1090.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13852 0 0 0 108970 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1100.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13852 0 0 0 109970 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1110.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13852 0 0 0 110970 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1120.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13852 0 0 0 111970 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1130.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13852 0 0 0 112970 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1140.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13891 0 0 0 113970 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1150.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13891 0 0 0 114970 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1160.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13891 0 0 0 115971 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1170.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13891 0 0 0 116971 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1180.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13891 0 0 0 117971 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1190.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13891 0 0 0 118971 45 0 0 25 0 1 0 547075373 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
[startup+1200.02 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 5486
Raw data (stat): 5482 (minisat+) R 5481 26298 26297 0 -1 0 13981 0 0 0 119971 46 0 0 25 0 1 0 547075373 50376704 11839 4294967295 134512640 134672761 3221224544 3221223728 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12299 11839 603 41 0 12258 0
vsize: 49196
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 1.00 0.93 1/54 5486
Raw data (stat): 5482 (minisat+) Z 5481 26298 26297 0 -1 12 13982 0 0 0 119971 48 0 0 25 0 1 0 547075373 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.05
CPU time (s): 1200.2
CPU user time (s): 1199.72
CPU system time (s): 0.485926
CPU usage (%): 100.013
Max. virtual memory (Kb): 49196
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####