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/miplib2003/normalized-mps-v2-13-7-markshare1.opb
MD5SUM	6f06e375914e0285ec75de90ad627758
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3712
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	6291450
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	6291450
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.1
Number of variables	170
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	70
Trace number 15415

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 04:18:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17639 boxname=wulflinc29 idbench=1357 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6f06e375914e0285ec75de90ad627758  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare1.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare1.opb
IDLAUNCH: 17639
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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	: 3
cpu MHz		: 451.020
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:        849264 kB
Buffers:         15696 kB
Cached:         141872 kB
SwapCached:        464 kB
Active:          40852 kB
Inactive:       118864 kB
HighTotal:      131008 kB
HighFree:         1120 kB
LowTotal:       903652 kB
LowFree:        848144 kB
SwapTotal:     2097892 kB
SwapFree:      2096700 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            20120 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 04:38:48 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 17639 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> Adder-cost: 304   maxlim: 405119   bits: 20/19
c ---[   8]---> Adder-cost: 314   maxlim: 431743   bits: 20/19
c ---[   6]---> Adder-cost: 348   maxlim: 435327   bits: 20/19
c ---[   4]---> Adder-cost: 318   maxlim: 411775   bits: 20/19
c ---[   2]---> Adder-cost: 312   maxlim: 410751   bits: 20/19
c ---[   0]---> Adder-cost: 314   maxlim: 411135   bits: 20/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   13134    47568 |    3940       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1948          
c   -- var.elim.:  1948/1948          
c   -- var.elim.:  255/255          
c   -- subsuming                       
c   -- var.elim.:  89/89          
c |         0 |   12429    44143 |      --       0       --      -- |     --   | -364/-1112
c |         0 |   12429    44143 |    4971       0        0     nan |  0.000 % |
c |       100 |   12429    44143 |    5468     100      445     4.5 | 12.612 % |
c ==============================================================================
c (current CPU-time: 0.394939 s)
c ==============================================================================
c [1mFound solution: 762752[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  853     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       126 |   14501    48987 |    4350     126      763     6.1 | 12.612 % |
c   -- subsuming                       
c   -- var.elim.:  792/792          
c   -- var.elim.:  434/434          
c   -- var.elim.:  13/13          
c   -- subsuming                       
c   -- var.elim.:  140/140          
c   -- var.elim.:  50/50          
c |       126 |   14181    49710 |      --     126       --      -- |     --   | -320/724
c |       126 |   14181    49710 |    5672     126      763     6.1 | 12.612 % |
c ==============================================================================
c (current CPU-time: 0.540917 s)
c ==============================================================================
c [1mFound solution: 745472[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       163 |   14338    50117 |    4301     163     1553     9.5 | 12.612 % |
c   -- subsuming                       
c   -- var.elim.:  273/273          
c   -- var.elim.:  132/132          
c |       163 |   14263    50214 |      --     163       --      -- |     --   | -75/98
c |       163 |   14263    50214 |    5705     163     1553     9.5 | 12.612 % |
c ==============================================================================
c (current CPU-time: 0.605907 s)
c ==============================================================================
c [1mFound solution: 662784[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       176 |   14337    50426 |    4301     176     1643     9.3 | 12.612 % |
c   -- subsuming                       
c   -- var.elim.:  137/137          
c   -- var.elim.:  92/92          
c |       176 |   14302    50495 |      --     176       --      -- |     --   | -35/70
c |       176 |   14302    50495 |    5720     176     1643     9.3 | 12.612 % |
c ==============================================================================
c (current CPU-time: 0.662899 s)
c ==============================================================================
c [1mFound solution: 621312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       188 |   14387    50743 |    4316     188     2162    11.5 | 12.612 % |
c   -- subsuming                       
c   -- var.elim.:  152/152          
c   -- var.elim.:  95/95          
c |       188 |   14338    50794 |      --     188       --      -- |     --   | -49/52
c |       188 |   14338    50794 |    5735     188     2162    11.5 | 12.612 % |
c ==============================================================================
c (current CPU-time: 0.765883 s)
c ==============================================================================
c [1mFound solution: 604288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       205 |   14389    50953 |    4316     205     6796    33.2 | 12.612 % |
c   -- subsuming                       
c   -- var.elim.:  115/115          
c   -- var.elim.:  74/74          
c |       205 |   14364    51018 |      --     205       --      -- |     --   | -25/66
c |       205 |   14364    51018 |    5745     205     6796    33.2 | 12.612 % |
c |       306 |   14364    51018 |    6320     306    25424    83.1 | 10.819 % |
c |       456 |   14364    51018 |    6952     456    51969   114.0 | 10.819 % |
c ==============================================================================
c (current CPU-time: 1.44578 s)
c ==============================================================================
c [1mFound solution: 572928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       570 |   14418    51182 |    4325     570    71939   126.2 | 10.819 % |
c   -- subsuming                       
c   -- var.elim.:  108/108          
c   -- var.elim.:  77/77          
c |       570 |   14394    51234 |      --     570       --      -- |     --   | -24/53
c |       570 |   14394    51234 |    5757     570    71939   126.2 | 10.819 % |
c |       672 |   14394    51234 |    6333     672    92512   137.7 | 10.846 % |
c |       823 |   14394    51234 |    6966     823   125895   153.0 | 10.846 % |
c ==============================================================================
c (current CPU-time: 2.20466 s)
c ==============================================================================
c [1mFound solution: 538624[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       940 |   14447    51398 |    4334     940   148320   157.8 | 10.846 % |
c   -- subsuming                       
c   -- var.elim.:  109/109          
c   -- var.elim.:  76/76          
c |       940 |   14421    51473 |      --     940       --      -- |     --   | -26/76
c |       940 |   14421    51473 |    5768     940   148320   157.8 | 10.846 % |
c |      1040 |   14421    51473 |    6345    1040   167923   161.5 | 10.877 % |
c ==============================================================================
c (current CPU-time: 2.43763 s)
c ==============================================================================
c [1mFound solution: 329344[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1055 |   14476    51636 |    4342    1055   168238   159.5 | 10.877 % |
c   -- subsuming                       
c   -- var.elim.:  104/104          
c   -- var.elim.:  72/72          
c |      1055 |   14453    51696 |      --    1055       --      -- |     --   | -23/61
c |      1055 |   14453    51696 |    5781    1055   168238   159.5 | 10.877 % |
c |      1155 |   14453    51696 |    6359    1155   182223   157.8 | 10.900 % |
c |      1306 |   14453    51696 |    6995    1306   183575   140.6 | 10.900 % |
c |      1533 |   14453    51696 |    7694    1533   189174   123.4 | 10.900 % |
c |      1873 |   14453    51696 |    8464    1873   194840   104.0 | 10.900 % |
c |      2379 |   14453    51696 |    9310    2379   213596    89.8 | 10.900 % |
c |      3138 |   14453    51696 |   10241    3138   242438    77.3 | 10.900 % |
c ==============================================================================
c (current CPU-time: 4.23036 s)
c ==============================================================================
c [1mFound solution: 325632[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3490 |   14507    51863 |    4352    3490   291633    83.6 | 10.900 % |
c   -- subsuming                       
c   -- var.elim.:  109/109          
c   -- var.elim.:  75/75          
c |      3490 |   14480    51945 |      --    3490       --      -- |     --   | -27/83
c |      3490 |   14480    51945 |    5792    3490   291633    83.6 | 10.900 % |
c |      3591 |   14480    51945 |    6371    3591   300896    83.8 | 10.926 % |
c |      3742 |   14480    51945 |    7008    3742   305096    81.5 | 10.926 % |
c |      3967 |   14480    51945 |    7709    3967   315242    79.5 | 10.926 % |
c ==============================================================================
c (current CPU-time: 5.13422 s)
c ==============================================================================
c [1mFound solution: 320768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4303 |   14533    52110 |    4359    4303   347503    80.8 | 10.926 % |
c   -- subsuming                       
c   -- var.elim.:  108/108          
c   -- var.elim.:  75/75          
c |      4303 |   14507    52165 |      --    4303       --      -- |     --   | -26/56
c |      4303 |   14507    52165 |    5802    4303   347503    80.8 | 10.926 % |
c |      4404 |   14507    52165 |    6383    4404   353729    80.3 | 10.953 % |
c ==============================================================================
c (current CPU-time: 5.40818 s)
c ==============================================================================
c [1mFound solution: 319744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4478 |   14561    52331 |    4368    4478   361274    80.7 | 10.953 % |
c   -- subsuming                       
c   -- var.elim.:  108/108          
c   -- var.elim.:  75/75          
c |      4478 |   14535    52386 |      --    4478       --      -- |     --   | -26/56
c |      4478 |   14535    52386 |    5814    4478   361274    80.7 | 10.953 % |
c |      4578 |   14535    52386 |    6395    4578   367803    80.3 | 10.979 % |
c |      4729 |   14535    52386 |    7034    4729   372331    78.7 | 10.979 % |
c |      4956 |   14535    52386 |    7738    4956   384294    77.5 | 10.979 % |
c |      5296 |   14535    52386 |    8512    5296   389914    73.6 | 10.979 % |
c |      5803 |   14535    52386 |    9363    5803   426175    73.4 | 10.980 % |
c |      6565 |   14535    52386 |   10299    6565   477022    72.7 | 10.979 % |
c |      7705 |   14535    52386 |   11329    7705   508869    66.0 | 10.979 % |
c |      9413 |   14535    52386 |   12462    9413   674904    71.7 | 10.979 % |
c ==============================================================================
c (current CPU-time: 10.4264 s)
c ==============================================================================
c [1mFound solution: 225152[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9629 |   14582    52529 |    4374    9629   688840    71.5 | 10.979 % |
c   -- subsuming                       
c   -- var.elim.:  94/94          
c   -- var.elim.:  65/65          
c |      9629 |   14558    52533 |      --    9629       --      -- |     --   | -24/5
c |      9629 |   14558    52533 |    5823    9629   688840    71.5 | 10.979 % |
c |      9730 |   14558    52533 |    6405    4381   235353    53.7 | 10.993 % |
c |      9880 |   14558    52533 |    7046    4531   243474    53.7 | 10.993 % |
c |     10105 |   14558    52533 |    7750    4756   253728    53.3 | 10.993 % |
c |     10442 |   14558    52533 |    8525    5093   266651    52.4 | 10.993 % |
c |     10948 |   14558    52533 |    9378    5599   297469    53.1 | 10.993 % |
c |     11707 |   14558    52533 |   10316    6358   325226    51.2 | 10.993 % |
c |     12846 |   14558    52533 |   11347    7497   380089    50.7 | 10.993 % |
c |     14554 |   14558    52533 |   12482    9205   459839    50.0 | 10.993 % |
c |     17116 |   14558    52533 |   13730   11767   618545    52.6 | 10.993 % |
c |     20960 |   14558    52533 |   15103   10792   572820    53.1 | 10.993 % |
c ==============================================================================
c (current CPU-time: 26.573 s)
c ==============================================================================
c [1mFound solution: 196864[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24254 |   14579    52598 |    4373   14086   818887    58.1 | 10.993 % |
c   -- subsuming                       
c   -- var.elim.:  41/41          
c   -- var.elim.:  31/31          
c   -- var.elim.:  2/2          
c |     24254 |   14568    52602 |      --   14086       --      -- |     --   | -11/5
c |     24254 |   14568    52602 |    5827   14086   818887    58.1 | 10.993 % |
c |     24354 |   14568    52602 |    6409    4274   211794    49.6 | 11.024 % |
c |     24504 |   14568    52602 |    7050    4424   217724    49.2 | 11.024 % |
c |     24730 |   14568    52602 |    7756    4650   224330    48.2 | 11.024 % |
c ==============================================================================
c (current CPU-time: 27.3168 s)
c ==============================================================================
c [1mFound solution: 164736[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24887 |   14589    52667 |    4376    4807   228472    47.5 | 11.024 % |
c   -- subsuming                       
c   -- var.elim.:  42/42          
c   -- var.elim.:  31/31          
c |     24887 |   14578    52683 |      --    4807       --      -- |     --   | -11/17
c |     24887 |   14578    52683 |    5831    4807   228472    47.5 | 11.024 % |
c |     24988 |   14578    52683 |    6414    4908   233741    47.6 | 11.054 % |
c |     25139 |   14396    51309 |    6967    5054   235297    46.6 | 11.290 % |
c |     25364 |   14396    51309 |    7664    5279   237293    45.0 | 11.290 % |
c |     25701 |   14396    51309 |    8430    5616   243871    43.4 | 11.290 % |
c |     26207 |   14396    51309 |    9273    6122   257046    42.0 | 11.290 % |
c |     26967 |   14396    51309 |   10201    6882   284704    41.4 | 11.290 % |
c |     28107 |   14396    51309 |   11221    8022   329523    41.1 | 11.290 % |
c ==============================================================================
c (current CPU-time: 30.3954 s)
c ==============================================================================
c [1mFound solution: 161920[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     29594 |   14403    51295 |    4320    9501   391071    41.2 | 11.290 % |
c   -- subsuming                       
c   -- var.elim.:  138/138          
c   -- var.elim.:  111/111          
c   -- var.elim.:  28/28          
c |     29594 |   14349    51188 |      --    9501       --      -- |     --   | -54/-106
c |     29594 |   14349    51188 |    5739    9252   372381    40.2 | 11.290 % |
c |     29695 |   14349    51188 |    6313    4213   130965    31.1 | 11.567 % |
c |     29846 |   14349    51188 |    6944    4364   132973    30.5 | 11.567 % |
c |     30073 |   14349    51188 |    7639    4591   154110    33.6 | 11.567 % |
c |     30411 |   14349    51188 |    8403    4929   165491    33.6 | 11.567 % |
c |     30917 |   14349    51188 |    9243    5435   185815    34.2 | 11.567 % |
c |     31678 |   14349    51188 |   10168    6196   213300    34.4 | 11.567 % |
c |     32817 |   14349    51188 |   11184    7335   249275    34.0 | 11.567 % |
c |     34525 |   14349    51188 |   12303    9043   322694    35.7 | 11.567 % |
c |     37090 |   14349    51188 |   13533   11608   445550    38.4 | 11.567 % |
c |     40935 |   14349    51188 |   14887   10694   466679    43.6 | 11.567 % |
c |     46702 |   14349    51188 |   16375   11309   846886    74.9 | 11.567 % |
c |     55351 |   14334    51117 |   17994   14212   934301    65.7 | 11.646 % |
c |     68325 |   14334    51117 |   19793   14456   960470    66.4 | 11.646 % |
c |     87787 |   14334    51117 |   21773   18220   920407    50.5 | 11.646 % |
c |    116981 |   14334    51117 |   23950   18043  1068252    59.2 | 11.646 % |
c |    160770 |   14334    51117 |   26345   21651  1405403    64.9 | 11.646 % |
c ==============================================================================
c (current CPU-time: 279.532 s)
c ==============================================================================
c [1mFound solution: 155264[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    198954 |   14363    51217 |    4308   21821  1367351    62.7 | 11.646 % |
c   -- subsuming                       
c   -- var.elim.:  131/131          
c   -- var.elim.:  71/71          
c |    198954 |   14343    51205 |      --   21821       --      -- |     --   | -20/-11
c |    198954 |   14343    51205 |    5737   21812  1366506    62.6 | 11.646 % |
c |    199057 |   14343    51205 |    6310    4413   169423    38.4 | 11.690 % |
c |    199207 |   14343    51205 |    6942    4563   171428    37.6 | 11.690 % |
c |    199435 |   14343    51205 |    7636    4791   175676    36.7 | 11.690 % |
c |    199772 |   14343    51205 |    8399    5128   185703    36.2 | 11.690 % |
c |    200279 |   14343    51205 |    9239    5635   197229    35.0 | 11.690 % |
c ==============================================================================
c (current CPU-time: 282.363 s)
c ==============================================================================
c [1mFound solution: 129152[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    200896 |   14361    51272 |    4308    6252   263144    42.1 | 11.690 % |
c   -- subsuming                       
c   -- var.elim.:  70/70          
c   -- var.elim.:  88/88          
c   -- var.elim.:  72/72          
c   -- var.elim.:  84/84          
c   -- var.elim.:  103/103          
c   -- var.elim.:  46/46          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  33/33          
c |    200896 |   14014    49153 |      --    6252       --      -- |     --   | -315/-2023
c |    200896 |   14014    49153 |    5605    5616   215325    38.3 | 11.690 % |
c |    200997 |   14014    49153 |    6166    5717   218811    38.3 | 12.303 % |
c |    201147 |   14014    49153 |    6782    5867   220815    37.6 | 12.303 % |
c |    201372 |   14014    49153 |    7461    6092   228062    37.4 | 12.303 % |
c |    201710 |   14014    49153 |    8207    6430   239943    37.3 | 12.303 % |
c |    202217 |   14014    49153 |    9027    6937   259630    37.4 | 12.303 % |
c |    202976 |   14014    49153 |    9930    7696   296808    38.6 | 12.303 % |
c |    204117 |   14014    49153 |   10923    8837   395728    44.8 | 12.303 % |
c |    205825 |   14014    49153 |   12016   10545   467726    44.4 | 12.303 % |
c |    208387 |   14014    49153 |   13217    8843   364297    41.2 | 12.303 % |
c |    212233 |   14014    49153 |   14539   12689   564524    44.5 | 12.303 % |
c |    217999 |   14014    49153 |   15993   13292   634465    47.7 | 12.303 % |
c |    226649 |   14014    49153 |   17592   16372  1009321    61.6 | 12.303 % |
c |    239623 |   14014    49153 |   19352   17087  1082173    63.3 | 12.303 % |
c |    259084 |   14014    49153 |   21287   16206   937570    57.9 | 12.303 % |
c |    288276 |   14014    49153 |   23415   19853  1324348    66.7 | 12.303 % |
c ==============================================================================
c (current CPU-time: 428.264 s)
c ==============================================================================
c [1mFound solution: 121088[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    306225 |   14078    49343 |    4223   17995   965379    53.6 | 12.303 % |
c   -- subsuming                       
c   -- var.elim.:  116/116          
c   -- var.elim.:  74/74          
c |    306225 |   14039    49447 |      --   17995       --      -- |     --   | -39/105
c |    306225 |   14039    49447 |    5615   17995   965379    53.6 | 12.303 % |
c |    306325 |   14039    49447 |    6177    5432   241714    44.5 | 12.318 % |
c |    306476 |   14039    49447 |    6794    5583   244698    43.8 | 12.318 % |
c ==============================================================================
c (current CPU-time: 429.067 s)
c ==============================================================================
c [1mFound solution: 67456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    306637 |   14076    49564 |    4222    5744   249789    43.5 | 12.318 % |
c   -- subsuming                       
c   -- var.elim.:  78/78          
c   -- var.elim.:  55/55          
c |    306637 |   14052    49544 |      --    5744       --      -- |     --   | -24/-19
c |    306637 |   14052    49544 |    5620    5744   249789    43.5 | 12.318 % |
c |    306737 |   14052    49544 |    6182    5844   252594    43.2 | 12.344 % |
c |    306887 |   14052    49544 |    6801    5994   258214    43.1 | 12.344 % |
c |    307112 |   14052    49544 |    7481    6219   264702    42.6 | 12.344 % |
c |    307449 |   14052    49544 |    8229    6556   303152    46.2 | 12.344 % |
c |    307955 |   14052    49544 |    9052    7062   320449    45.4 | 12.344 % |
c |    308714 |   14052    49544 |    9957    7821   343510    43.9 | 12.344 % |
c |    309853 |   14052    49544 |   10953    8960   390919    43.6 | 12.344 % |
c |    311561 |   14037    49369 |   12035   10667   449803    42.2 | 12.384 % |
c |    314125 |   14037    49369 |   13239    9007   328529    36.5 | 12.384 % |
c |    317970 |   14037    49369 |   14563   12852   508091    39.5 | 12.384 % |
c |    323736 |   14014    49273 |   15993   13565   501401    37.0 | 12.465 % |
c |    332386 |   14014    49273 |   17592   11214   400096    35.7 | 12.465 % |
c ==============================================================================
c (current CPU-time: 464.965 s)
c ==============================================================================
c [1mFound solution: 66432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    340791 |   14051    49388 |    4215   13534   649861    48.0 | 12.465 % |
c   -- subsuming                       
c   -- var.elim.:  105/105          
c   -- var.elim.:  78/78          
c |    340791 |   14013    49400 |      --   13534       --      -- |     --   | -38/13
c |    340791 |   14013    49400 |    5605   13532   649857    48.0 | 12.465 % |
c |    340893 |   14013    49400 |    6165    4112   186927    45.5 | 12.576 % |
c |    341043 |   14013    49400 |    6782    4262   189206    44.4 | 12.576 % |
c |    341271 |   14013    49400 |    7460    4490   191950    42.8 | 12.576 % |
c |    341608 |   14013    49400 |    8206    4827   200975    41.6 | 12.576 % |
c |    342114 |   14013    49400 |    9027    5333   223913    42.0 | 12.576 % |
c |    342874 |   14013    49400 |    9929    6093   263529    43.3 | 12.576 % |
c |    344013 |   14013    49400 |   10922    7232   313069    43.3 | 12.576 % |
c |    345721 |   14013    49400 |   12015    8940   367690    41.1 | 12.576 % |
c |    348286 |   14013    49400 |   13216   11505   463790    40.3 | 12.576 % |
c |    352131 |   14013    49400 |   14538   10761   401276    37.3 | 12.576 % |
c |    357897 |   14013    49400 |   15992   11454   490445    42.8 | 12.576 % |
c |    366546 |   14013    49400 |   17591   14516   574100    39.5 | 12.576 % |
c |    379520 |   13997    49335 |   19328   15466   576421    37.3 | 12.657 % |
c |    398982 |   13997    49335 |   21261   14305   771687    53.9 | 12.657 % |
c |    428175 |   13978    49255 |   23355   17670   785847    44.5 | 12.738 % |
c |    471966 |   13978    49255 |   25691   19140  1137529    59.4 | 12.738 % |
c ==============================================================================
c (current CPU-time: 669.882 s)
c ==============================================================================
c [1mFound solution: 63744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT            #### 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.93 0.98 0.92 2/54 22049
Raw data (stat): 22049 (runsolver) R 22048 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542139696 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 2329 0 0 0 992 6 0 0 25 0 1 0 542139696 8478720 1695 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2070 1695 603 41 0 2029 0
vsize: 8280
[startup+20.0015 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 2562 0 0 0 1990 7 0 0 25 0 1 0 542139696 9355264 1903 4294967295 134512640 134672761 3221224544 3221223576 134614386 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2284 1903 603 41 0 2243 0
vsize: 9136
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 2804 0 0 0 2988 8 0 0 25 0 1 0 542139696 9793536 2033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2391 2033 603 41 0 2350 0
vsize: 9564
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 2858 0 0 0 3987 9 0 0 25 0 1 0 542139696 9793536 2033 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2391 2033 603 41 0 2350 0
vsize: 9564
[startup+50.0026 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 2987 0 0 0 4987 10 0 0 25 0 1 0 542139696 10321920 2162 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2520 2162 603 41 0 2479 0
vsize: 10080
[startup+60.002 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3315 0 0 0 5986 10 0 0 25 0 1 0 542139696 11776000 2490 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2490 603 41 0 2834 0
vsize: 11500
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3336 0 0 0 6987 10 0 0 25 0 1 0 542139696 11845632 2511 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2892 2511 603 41 0 2851 0
vsize: 11568
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3357 0 0 0 7987 10 0 0 25 0 1 0 542139696 11935744 2532 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2914 2532 603 41 0 2873 0
vsize: 11656
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3514 0 0 0 8986 11 0 0 25 0 1 0 542139696 12562432 2689 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3067 2689 603 41 0 3026 0
vsize: 12268
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3519 0 0 0 9987 11 0 0 25 0 1 0 542139696 12570624 2693 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3069 2693 603 41 0 3028 0
vsize: 12276
[startup+110.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3521 0 0 0 10987 11 0 0 25 0 1 0 542139696 12570624 2695 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3069 2695 603 41 0 3028 0
vsize: 12276
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3531 0 0 0 11987 11 0 0 25 0 1 0 542139696 12611584 2704 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3079 2704 603 41 0 3038 0
vsize: 12316
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3534 0 0 0 12987 11 0 0 25 0 1 0 542139696 12611584 2707 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3079 2707 603 41 0 3038 0
vsize: 12316
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3675 0 0 0 13987 11 0 0 25 0 1 0 542139696 13201408 2847 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3223 2847 603 41 0 3182 0
vsize: 12892
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3813 0 0 0 14987 12 0 0 25 0 1 0 542139696 13733888 2985 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2985 603 41 0 3312 0
vsize: 13412
[startup+160.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3860 0 0 0 15987 12 0 0 25 0 1 0 542139696 13942784 3032 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3404 3032 603 41 0 3363 0
vsize: 13616
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3913 0 0 0 16987 12 0 0 25 0 1 0 542139696 14155776 3085 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3456 3085 603 41 0 3415 0
vsize: 13824
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 3913 0 0 0 17987 12 0 0 25 0 1 0 542139696 14155776 3085 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3456 3085 603 41 0 3415 0
vsize: 13824
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4088 0 0 0 18987 12 0 0 25 0 1 0 542139696 14868480 3259 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3630 3259 603 41 0 3589 0
vsize: 14520
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4088 0 0 0 19987 12 0 0 25 0 1 0 542139696 14868480 3259 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3630 3259 603 41 0 3589 0
vsize: 14520
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4152 0 0 0 20987 13 0 0 25 0 1 0 542139696 15138816 3322 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3696 3322 603 41 0 3655 0
vsize: 14784
[startup+220.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4153 0 0 0 21987 13 0 0 25 0 1 0 542139696 15138816 3323 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3696 3323 603 41 0 3655 0
vsize: 14784
[startup+230.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4209 0 0 0 22987 13 0 0 25 0 1 0 542139696 15355904 3379 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3379 603 41 0 3708 0
vsize: 14996
[startup+240.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4218 0 0 0 23987 13 0 0 25 0 1 0 542139696 15388672 3387 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3757 3387 603 41 0 3716 0
vsize: 15028
[startup+250.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4218 0 0 0 24987 13 0 0 25 0 1 0 542139696 15388672 3387 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3757 3387 603 41 0 3716 0
vsize: 15028
[startup+260.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4218 0 0 0 25988 13 0 0 25 0 1 0 542139696 15388672 3387 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3757 3387 603 41 0 3716 0
vsize: 15028
[startup+270.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4387 0 0 0 26987 13 0 0 25 0 1 0 542139696 16076800 3555 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3925 3555 603 41 0 3884 0
vsize: 15700
[startup+280.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4478 0 0 0 27987 14 0 0 25 0 1 0 542139696 16293888 3613 4294967295 134512640 134672761 3221224544 3221223600 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3978 3613 603 41 0 3937 0
vsize: 15912
[startup+290.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 28985 14 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+300.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 29986 14 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+310.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 30986 14 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+320.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 31986 14 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+330.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 32986 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+340.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 33986 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+350.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 34986 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+360.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 35987 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+370.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 36987 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+380.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 37987 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+390.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 38988 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+400.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 39988 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+410.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 40988 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+420.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 41988 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+430.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 42988 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+440.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 43988 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+450.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 44988 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+460.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4503 0 0 0 45988 15 0 0 25 0 1 0 542139696 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+470.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 46988 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+480.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 47987 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+490.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 48988 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+500.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 49989 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+510.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 50989 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+520.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 51989 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+530.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 52989 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+540.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 53989 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+550.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 54990 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+560.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 55990 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+570.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 56990 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+580.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 57990 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+590.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 58990 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+600.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 59990 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+610.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 60991 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+620.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 61991 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+630.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4504 0 0 0 62991 15 0 0 25 0 1 0 542139696 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+640.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4541 0 0 0 63991 15 0 0 25 0 1 0 542139696 16572416 3675 4294967295 134512640 134672761 3221224544 3221223584 134612851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3675 603 41 0 4005 0
vsize: 16184
[startup+650.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4541 0 0 0 64991 15 0 0 25 0 1 0 542139696 16572416 3675 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3675 603 41 0 4005 0
vsize: 16184
[startup+660.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4569 0 0 0 65991 15 0 0 25 0 1 0 542139696 16678912 3703 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4072 3703 603 41 0 4031 0
vsize: 16288
[startup+670.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4653 0 0 0 66991 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223920 134620012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+680.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 67992 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+690.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 68992 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+700.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 69992 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+710.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 70992 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+720.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 71992 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+730.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 72992 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+740.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 73993 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+750.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 74993 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+760.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 75993 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+770.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 76993 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+780.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 77993 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+790.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 78993 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+800.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 79994 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+810.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 80994 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+820.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 81994 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+830.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 82994 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+840.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 83994 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223548 134565030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+850.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 84995 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+860.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 85995 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+870.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 86995 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+880.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 87996 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+890.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 88996 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+900.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4664 0 0 0 89996 16 0 0 25 0 1 0 542139696 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+910.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4750 0 0 0 90996 16 0 0 25 0 1 0 542139696 17178624 3824 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4194 3824 603 41 0 4153 0
vsize: 16776
[startup+920.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4750 0 0 0 91996 16 0 0 25 0 1 0 542139696 17178624 3824 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4194 3824 603 41 0 4153 0
vsize: 16776
[startup+930.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4754 0 0 0 92996 16 0 0 25 0 1 0 542139696 17186816 3827 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4196 3827 603 41 0 4155 0
vsize: 16784
[startup+940.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4754 0 0 0 93997 16 0 0 25 0 1 0 542139696 17186816 3827 4294967295 134512640 134672761 3221224544 3221223728 134615835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4196 3827 603 41 0 4155 0
vsize: 16784
[startup+950.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4762 0 0 0 94997 16 0 0 25 0 1 0 542139696 17219584 3834 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4204 3834 603 41 0 4163 0
vsize: 16816
[startup+960.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4762 0 0 0 95997 16 0 0 25 0 1 0 542139696 17219584 3834 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4204 3834 603 41 0 4163 0
vsize: 16816
[startup+970.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4784 0 0 0 96997 16 0 0 25 0 1 0 542139696 17416192 3856 4294967295 134512640 134672761 3221224544 3221223640 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4252 3856 603 41 0 4211 0
vsize: 17008
[startup+980.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4784 0 0 0 97997 16 0 0 25 0 1 0 542139696 17285120 3855 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4220 3855 603 41 0 4179 0
vsize: 16880
[startup+990.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4784 0 0 0 98997 16 0 0 25 0 1 0 542139696 17285120 3855 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4220 3855 603 41 0 4179 0
vsize: 16880
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4784 0 0 0 99998 16 0 0 25 0 1 0 542139696 17285120 3855 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4220 3855 603 41 0 4179 0
vsize: 16880
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4793 0 0 0 100998 16 0 0 25 0 1 0 542139696 17317888 3863 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4228 3863 603 41 0 4187 0
vsize: 16912
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4793 0 0 0 101998 16 0 0 25 0 1 0 542139696 17317888 3863 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4228 3863 603 41 0 4187 0
vsize: 16912
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4798 0 0 0 102998 16 0 0 25 0 1 0 542139696 17334272 3867 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4232 3867 603 41 0 4191 0
vsize: 16928
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4798 0 0 0 103998 16 0 0 25 0 1 0 542139696 17334272 3867 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4232 3867 603 41 0 4191 0
vsize: 16928
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4807 0 0 0 104998 16 0 0 25 0 1 0 542139696 17367040 3875 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4807 0 0 0 105999 16 0 0 25 0 1 0 542139696 17367040 3875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4807 0 0 0 106999 16 0 0 25 0 1 0 542139696 17367040 3875 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4807 0 0 0 107999 16 0 0 25 0 1 0 542139696 17367040 3875 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 4807 0 0 0 108999 16 0 0 25 0 1 0 542139696 17367040 3875 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5081 0 0 0 109999 16 0 0 25 0 1 0 542139696 18485248 4148 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4513 4148 603 41 0 4472 0
vsize: 18052
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5081 0 0 0 110999 16 0 0 25 0 1 0 542139696 18485248 4148 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4513 4148 603 41 0 4472 0
vsize: 18052
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5081 0 0 0 111999 16 0 0 25 0 1 0 542139696 18485248 4148 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4513 4148 603 41 0 4472 0
vsize: 18052
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5231 0 0 0 112999 17 0 0 25 0 1 0 542139696 19075072 4297 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4657 4297 603 41 0 4616 0
vsize: 18628
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5231 0 0 0 113999 17 0 0 25 0 1 0 542139696 19075072 4297 4294967295 134512640 134672761 3221224544 3221223584 134612797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4657 4297 603 41 0 4616 0
vsize: 18628
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5231 0 0 0 114999 17 0 0 25 0 1 0 542139696 19075072 4297 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4657 4297 603 41 0 4616 0
vsize: 18628
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5232 0 0 0 115999 17 0 0 25 0 1 0 542139696 19075072 4298 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4657 4298 603 41 0 4616 0
vsize: 18628
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5232 0 0 0 117000 17 0 0 25 0 1 0 542139696 19075072 4298 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4657 4298 603 41 0 4616 0
vsize: 18628
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5232 0 0 0 118000 17 0 0 25 0 1 0 542139696 19075072 4298 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4657 4298 603 41 0 4616 0
vsize: 18628
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5333 0 0 0 119000 17 0 0 25 0 1 0 542139696 19623936 4399 4294967295 134512640 134672761 3221224544 3221223392 134645408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4791 4399 603 41 0 4750 0
vsize: 19164
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 22049
Raw data (stat): 22049 (minisat+) R 22048 27222 27221 0 -1 0 5333 0 0 0 120000 17 0 0 25 0 1 0 542139696 19492864 4398 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4759 4398 603 41 0 4718 0
vsize: 19036
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.92 1/54 22049
Raw data (stat): 22049 (minisat+) Z 22048 27222 27221 0 -1 12 5334 0 0 0 120000 18 0 0 25 0 1 0 542139696 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.19
CPU user time (s): 1200
CPU system time (s): 0.182972
CPU usage (%): 100.011
Max. virtual memory (Kb): 19164
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####