PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-misc07.opb
MD5SUM	54df16ee65da54d5975ffedee80d2bb9
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 18089

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 13:31:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18588 boxname=wulflinc2 idbench=1430 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  54df16ee65da54d5975ffedee80d2bb9  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 18588
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        678984 kB
Buffers:         23032 kB
Cached:         311636 kB
SwapCached:        504 kB
Active:          61176 kB
Inactive:       275704 kB
HighTotal:      131008 kB
HighFree:         1036 kB
LowTotal:       903652 kB
LowFree:        677948 kB
SwapTotal:     2097136 kB
SwapFree:      2095900 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5712 kB
Slab:            13168 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:51:17 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 18588 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.36679 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: 6.01309 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.0383 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.3771 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.943 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.5174 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.281 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: 370.009 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: 382.804 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: 673.796 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 -COL04#### 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.92 0.98 0.95 2/54 28157
Raw data (stat): 28157 (runsolver) R 28156 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487238578 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99995 s]
Raw data (loadavg): 0.93 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 2895 0 0 0 991 6 0 0 25 0 1 0 487238578 11579392 2388 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2827 2388 603 41 0 2786 0
vsize: 11308
[startup+19.9994 s]
Raw data (loadavg): 0.94 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 3890 0 0 0 1987 10 0 0 25 0 1 0 487238578 15093760 3252 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3685 3252 603 41 0 3644 0
vsize: 14740
[startup+30.0001 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 5040 0 0 0 2985 12 0 0 25 0 1 0 487238578 19939328 4402 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4868 4402 603 41 0 4827 0
vsize: 19472
[startup+40.0003 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 5556 0 0 0 3983 14 0 0 25 0 1 0 487238578 20561920 4586 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5020 4586 603 41 0 4979 0
vsize: 20080
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 5556 0 0 0 4983 14 0 0 25 0 1 0 487238578 20561920 4586 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5020 4586 603 41 0 4979 0
vsize: 20080
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 6012 0 0 0 5981 16 0 0 25 0 1 0 487238578 22532096 5042 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5501 5042 603 41 0 5460 0
vsize: 22004
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 6938 0 0 0 6979 19 0 0 25 0 1 0 487238578 26226688 5968 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6403 5968 603 41 0 6362 0
vsize: 25612
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 7453 0 0 0 7977 20 0 0 25 0 1 0 487238578 28336128 6483 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6918 6483 603 41 0 6877 0
vsize: 27672
[startup+90.0013 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 7685 0 0 0 8977 21 0 0 25 0 1 0 487238578 28479488 6526 4294967295 134512640 134672761 3221224544 3221223800 134616317 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.002 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 7689 0 0 0 9977 21 0 0 25 0 1 0 487238578 28676096 6530 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7001 6530 603 41 0 6960 0
vsize: 28004
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 7689 0 0 0 10977 21 0 0 25 0 1 0 487238578 28676096 6530 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7001 6530 603 41 0 6960 0
vsize: 28004
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 7689 0 0 0 11977 21 0 0 25 0 1 0 487238578 28676096 6530 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7001 6530 603 41 0 6960 0
vsize: 28004
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 7689 0 0 0 12977 21 0 0 25 0 1 0 487238578 28676096 6530 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7001 6530 603 41 0 6960 0
vsize: 28004
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8300 0 0 0 13975 23 0 0 25 0 1 0 487238578 30060544 6901 4294967295 134512640 134672761 3221224544 3221223712 134553613 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.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8300 0 0 0 14975 23 0 0 25 0 1 0 487238578 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8300 0 0 0 15975 24 0 0 25 0 1 0 487238578 30060544 6901 4294967295 134512640 134672761 3221224544 3221223584 134614263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7339 6901 603 41 0 7298 0
vsize: 29356
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8300 0 0 0 16975 24 0 0 25 0 1 0 487238578 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+180.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8300 0 0 0 17974 24 0 0 25 0 1 0 487238578 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615828 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8300 0 0 0 18975 24 0 0 25 0 1 0 487238578 30060544 6901 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8300 0 0 0 19975 24 0 0 25 0 1 0 487238578 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.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8300 0 0 0 20975 24 0 0 25 0 1 0 487238578 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+220.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8474 0 0 0 21975 25 0 0 25 0 1 0 487238578 30855168 7075 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7533 7075 603 41 0 7492 0
vsize: 30132
[startup+230.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8714 0 0 0 22974 25 0 0 25 0 1 0 487238578 31752192 7315 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8714 0 0 0 23975 25 0 0 25 0 1 0 487238578 31752192 7315 4294967295 134512640 134672761 3221224544 3221223728 134615632 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.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8714 0 0 0 24975 25 0 0 25 0 1 0 487238578 31752192 7315 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 8980 0 0 0 25974 26 0 0 25 0 1 0 487238578 33062912 7581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8072 7581 603 41 0 8031 0
vsize: 32288
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 9296 0 0 0 26974 26 0 0 25 0 1 0 487238578 34246656 7894 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 9296 0 0 0 27974 27 0 0 25 0 1 0 487238578 34246656 7894 4294967295 134512640 134672761 3221224544 3221223728 134615625 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 9296 0 0 0 28974 27 0 0 25 0 1 0 487238578 34246656 7894 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 9528 0 0 0 29974 27 0 0 25 0 1 0 487238578 35291136 8126 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8616 8126 603 41 0 8575 0
vsize: 34464
[startup+310.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 10243 0 0 0 30972 29 0 0 25 0 1 0 487238578 38191104 8841 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9324 8841 603 41 0 9283 0
vsize: 37296
[startup+320.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 10946 0 0 0 31970 32 0 0 25 0 1 0 487238578 41099264 9544 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10034 9544 603 41 0 9993 0
vsize: 40136
[startup+330.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11231 0 0 0 32969 32 0 0 25 0 1 0 487238578 41992192 9790 4294967295 134512640 134672761 3221224544 3221223584 134612663 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11231 0 0 0 33969 32 0 0 25 0 1 0 487238578 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11231 0 0 0 34969 32 0 0 25 0 1 0 487238578 41992192 9790 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11231 0 0 0 35970 32 0 0 25 0 1 0 487238578 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+370.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11231 0 0 0 36970 32 0 0 25 0 1 0 487238578 41992192 9790 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10252 9790 603 41 0 10211 0
vsize: 41008
[startup+380.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11363 0 0 0 37968 34 0 0 25 0 1 0 487238578 41984000 9796 4294967295 134512640 134672761 3221224544 3221223744 134610707 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 38967 34 0 0 25 0 1 0 487238578 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+400.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 39967 34 0 0 25 0 1 0 487238578 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10250 9798 603 41 0 10209 0
vsize: 41000
[startup+410.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 40966 35 0 0 25 0 1 0 487238578 41984000 9798 4294967295 134512640 134672761 3221224544 3221223680 134614677 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.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 41967 35 0 0 25 0 1 0 487238578 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+430.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 42967 35 0 0 25 0 1 0 487238578 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+440.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 43967 35 0 0 25 0 1 0 487238578 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 44967 35 0 0 25 0 1 0 487238578 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615916 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.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 45967 35 0 0 25 0 1 0 487238578 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615739 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.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 46967 35 0 0 25 0 1 0 487238578 41984000 9798 4294967295 134512640 134672761 3221224544 3221223728 134615758 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.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 47968 35 0 0 25 0 1 0 487238578 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+490.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 48968 35 0 0 25 0 1 0 487238578 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.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11535 0 0 0 49968 35 0 0 25 0 1 0 487238578 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+510.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11536 0 0 0 50968 35 0 0 25 0 1 0 487238578 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11536 0 0 0 51968 35 0 0 25 0 1 0 487238578 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615741 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.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11536 0 0 0 52969 35 0 0 25 0 1 0 487238578 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11536 0 0 0 53969 35 0 0 25 0 1 0 487238578 41984000 9799 4294967295 134512640 134672761 3221224544 3221223744 134610667 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.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11571 0 0 0 54969 35 0 0 25 0 1 0 487238578 41984000 9799 4294967295 134512640 134672761 3221224544 3221223744 134610686 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.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11571 0 0 0 55969 35 0 0 25 0 1 0 487238578 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.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11571 0 0 0 56969 35 0 0 25 0 1 0 487238578 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11571 0 0 0 57969 35 0 0 25 0 1 0 487238578 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615732 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.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11571 0 0 0 58970 35 0 0 25 0 1 0 487238578 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+600.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11571 0 0 0 59970 35 0 0 25 0 1 0 487238578 41984000 9799 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 11907 0 0 0 60969 36 0 0 25 0 1 0 487238578 43425792 10135 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10602 10135 603 41 0 10561 0
vsize: 42408
[startup+620.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12371 0 0 0 61968 38 0 0 25 0 1 0 487238578 45113344 10562 4294967295 134512640 134672761 3221224544 3221223376 1075350544 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.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12371 0 0 0 62968 38 0 0 25 0 1 0 487238578 45113344 10562 4294967295 134512640 134672761 3221224544 3221223728 134615632 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.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12371 0 0 0 63968 38 0 0 25 0 1 0 487238578 45113344 10562 4294967295 134512640 134672761 3221224544 3221223728 134615807 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.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12371 0 0 0 64968 38 0 0 25 0 1 0 487238578 45113344 10562 4294967295 134512640 134672761 3221224544 3221223584 134612628 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.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12371 0 0 0 65968 38 0 0 25 0 1 0 487238578 45113344 10562 4294967295 134512640 134672761 3221224544 3221223688 134616263 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.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12371 0 0 0 66969 38 0 0 25 0 1 0 487238578 45113344 10562 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11014 10562 603 41 0 10973 0
vsize: 44056
[startup+680.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 67968 38 0 0 25 0 1 0 487238578 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615643 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.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 68968 38 0 0 25 0 1 0 487238578 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+700.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 69968 38 0 0 25 0 1 0 487238578 45072384 10554 4294967295 134512640 134672761 3221224544 3221223668 134566089 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.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 70969 38 0 0 25 0 1 0 487238578 45072384 10554 4294967295 134512640 134672761 3221224544 3221223584 134613815 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.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 71969 38 0 0 25 0 1 0 487238578 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 72969 38 0 0 25 0 1 0 487238578 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615758 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.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 73969 38 0 0 25 0 1 0 487238578 45072384 10554 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 74969 38 0 0 25 0 1 0 487238578 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.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 75970 38 0 0 25 0 1 0 487238578 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+770.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 76970 38 0 0 25 0 1 0 487238578 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+780.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 77970 38 0 0 25 0 1 0 487238578 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+790.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12535 0 0 0 78970 38 0 0 25 0 1 0 487238578 45072384 10554 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11004 10554 603 41 0 10963 0
vsize: 44016
[startup+800.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12555 0 0 0 79970 38 0 0 25 0 1 0 487238578 45158400 10574 4294967295 134512640 134672761 3221224544 3221223728 134615736 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.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12555 0 0 0 80971 38 0 0 25 0 1 0 487238578 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+820.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12555 0 0 0 81971 38 0 0 25 0 1 0 487238578 45158400 10574 4294967295 134512640 134672761 3221224544 3221223688 134616350 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.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12555 0 0 0 82971 38 0 0 25 0 1 0 487238578 45158400 10574 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12555 0 0 0 83971 38 0 0 25 0 1 0 487238578 45158400 10574 4294967295 134512640 134672761 3221224544 3221223584 134612684 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.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12555 0 0 0 84971 38 0 0 25 0 1 0 487238578 45158400 10574 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12555 0 0 0 85972 38 0 0 25 0 1 0 487238578 45158400 10574 4294967295 134512640 134672761 3221224544 3221223728 134615720 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.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12628 0 0 0 86971 38 0 0 25 0 1 0 487238578 45555712 10647 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11122 10647 603 41 0 11081 0
vsize: 44488
[startup+880.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12817 0 0 0 87971 39 0 0 25 0 1 0 487238578 46088192 10802 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12817 0 0 0 88971 39 0 0 25 0 1 0 487238578 46088192 10802 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12818 0 0 0 89971 39 0 0 25 0 1 0 487238578 46088192 10803 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10803 603 41 0 11211 0
vsize: 45008
[startup+910.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12819 0 0 0 90971 40 0 0 25 0 1 0 487238578 46088192 10804 4294967295 134512640 134672761 3221224544 3221223728 134615919 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12819 0 0 0 91971 40 0 0 25 0 1 0 487238578 46088192 10804 4294967295 134512640 134672761 3221224544 3221223728 134615804 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.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12819 0 0 0 92972 40 0 0 25 0 1 0 487238578 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12819 0 0 0 93972 40 0 0 25 0 1 0 487238578 46088192 10804 4294967295 134512640 134672761 3221224544 3221223728 134615663 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.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 12834 0 0 0 94972 40 0 0 25 0 1 0 487238578 46219264 10819 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11284 10819 603 41 0 11243 0
vsize: 45136
[startup+960.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13209 0 0 0 95971 41 0 0 25 0 1 0 487238578 47812608 11194 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11673 11194 603 41 0 11632 0
vsize: 46692
[startup+970.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13612 0 0 0 96969 42 0 0 25 0 1 0 487238578 49401856 11597 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12061 11597 603 41 0 12020 0
vsize: 48244
[startup+980.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13812 0 0 0 97969 43 0 0 25 0 1 0 487238578 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+990.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13812 0 0 0 98969 43 0 0 25 0 1 0 487238578 50036736 11761 4294967295 134512640 134672761 3221224544 3221223728 134615732 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13812 0 0 0 99970 43 0 0 25 0 1 0 487238578 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+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13812 0 0 0 100970 43 0 0 25 0 1 0 487238578 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13812 0 0 0 101970 43 0 0 25 0 1 0 487238578 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+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13812 0 0 0 102970 43 0 0 25 0 1 0 487238578 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+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13812 0 0 0 103970 43 0 0 25 0 1 0 487238578 50036736 11761 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11761 603 41 0 12175 0
vsize: 48864
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13813 0 0 0 104971 43 0 0 25 0 1 0 487238578 50036736 11762 4294967295 134512640 134672761 3221224544 3221223728 134615833 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13813 0 0 0 105971 43 0 0 25 0 1 0 487238578 50036736 11762 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12216 11762 603 41 0 12175 0
vsize: 48864
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13852 0 0 0 106971 43 0 0 25 0 1 0 487238578 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13852 0 0 0 107971 43 0 0 25 0 1 0 487238578 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+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13852 0 0 0 108971 43 0 0 25 0 1 0 487238578 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615627 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13852 0 0 0 109971 43 0 0 25 0 1 0 487238578 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+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13852 0 0 0 110971 43 0 0 25 0 1 0 487238578 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615549 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13852 0 0 0 111972 43 0 0 25 0 1 0 487238578 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615720 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13852 0 0 0 112972 43 0 0 25 0 1 0 487238578 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615619 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13852 0 0 0 113972 43 0 0 25 0 1 0 487238578 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+1150.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13891 0 0 0 114972 43 0 0 25 0 1 0 487238578 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+1160.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13891 0 0 0 115972 43 0 0 25 0 1 0 487238578 49983488 11749 4294967295 134512640 134672761 3221224544 3221223648 134603709 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13891 0 0 0 116972 43 0 0 25 0 1 0 487238578 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615665 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13891 0 0 0 117973 43 0 0 25 0 1 0 487238578 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+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13891 0 0 0 118973 43 0 0 25 0 1 0 487238578 49983488 11749 4294967295 134512640 134672761 3221224544 3221223728 134615705 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 0.98 0.95 2/54 28157
Raw data (stat): 28157 (minisat+) R 28156 20937 20936 0 -1 0 13891 0 0 0 119973 43 0 0 25 0 1 0 487238578 49983488 11749 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12203 11749 603 41 0 12162 0
vsize: 48812
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.95 1/54 28157
Raw data (stat): 28157 (minisat+) Z 28156 20937 20936 0 -1 12 13892 0 0 0 119973 46 0 0 25 0 1 0 487238578 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.04
CPU time (s): 1200.2
CPU user time (s): 1199.73
CPU system time (s): 0.460929
CPU usage (%): 100.013
Max. virtual memory (Kb): 48864
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####