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-markshare1.opb
MD5SUM	ba87f5dfbaed559dc55bc00bf07dc880
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.68
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 18128

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 13:40:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18510 boxname=wulflinc27 idbench=1424 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ba87f5dfbaed559dc55bc00bf07dc880  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-markshare1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-markshare1.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-markshare1.opb
IDLAUNCH: 18510
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        877220 kB
Buffers:          9716 kB
Cached:         124004 kB
SwapCached:        512 kB
Active:          12816 kB
Inactive:       122904 kB
HighTotal:      131008 kB
HighFree:        70924 kB
LowTotal:       903652 kB
LowFree:        806296 kB
SwapTotal:     2097892 kB
SwapFree:      2096472 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            15960 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:00:11 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 18510 7 1200.18 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.383941 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.532918 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.596909 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.6519 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.752885 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.44078 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.20666 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.44263 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.25735 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.17421 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.45017 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.5824 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: 27.0059 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.7678 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.8943 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: 282.281 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: 285.115 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: 432.307 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: 433.117 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: 469.305 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: 676.435 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.91 0.95 0.91 2/54 20018
Raw data (stat): 20018 (runsolver) R 20017 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545508549 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 2317 0 0 0 990 9 0 0 25 0 1 0 545508549 8478720 1683 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2070 1683 603 41 0 2029 0
vsize: 8280
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 2542 0 0 0 1988 10 0 0 25 0 1 0 545508549 9224192 1883 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2252 1883 603 41 0 2211 0
vsize: 9008
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 2804 0 0 0 2987 11 0 0 25 0 1 0 545508549 9793536 2033 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2391 2033 603 41 0 2350 0
vsize: 9564
[startup+40.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 2858 0 0 0 3985 12 0 0 25 0 1 0 545508549 9793536 2033 4294967295 134512640 134672761 3221224544 3221223728 134615948 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.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 2956 0 0 0 4985 13 0 0 25 0 1 0 545508549 10321920 2131 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2520 2131 603 41 0 2479 0
vsize: 10080
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3315 0 0 0 5984 13 0 0 25 0 1 0 545508549 11776000 2490 4294967295 134512640 134672761 3221224544 3221223680 134614560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2875 2490 603 41 0 2834 0
vsize: 11500
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3336 0 0 0 6984 14 0 0 25 0 1 0 545508549 11845632 2511 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2892 2511 603 41 0 2851 0
vsize: 11568
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3357 0 0 0 7984 14 0 0 25 0 1 0 545508549 11935744 2532 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2914 2532 603 41 0 2873 0
vsize: 11656
[startup+90.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3514 0 0 0 8984 14 0 0 25 0 1 0 545508549 12562432 2689 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3067 2689 603 41 0 3026 0
vsize: 12268
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3519 0 0 0 9984 14 0 0 25 0 1 0 545508549 12570624 2693 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3069 2693 603 41 0 3028 0
vsize: 12276
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3521 0 0 0 10985 14 0 0 25 0 1 0 545508549 12570624 2695 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3069 2695 603 41 0 3028 0
vsize: 12276
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3521 0 0 0 11985 14 0 0 25 0 1 0 545508549 12570624 2695 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3069 2695 603 41 0 3028 0
vsize: 12276
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3531 0 0 0 12985 14 0 0 25 0 1 0 545508549 12611584 2704 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3079 2704 603 41 0 3038 0
vsize: 12316
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3675 0 0 0 13985 14 0 0 25 0 1 0 545508549 13201408 2847 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3223 2847 603 41 0 3182 0
vsize: 12892
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3729 0 0 0 14985 14 0 0 25 0 1 0 545508549 13467648 2901 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3288 2901 603 41 0 3247 0
vsize: 13152
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3860 0 0 0 15985 15 0 0 25 0 1 0 545508549 13942784 3032 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3404 3032 603 41 0 3363 0
vsize: 13616
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3913 0 0 0 16985 15 0 0 25 0 1 0 545508549 14155776 3085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3456 3085 603 41 0 3415 0
vsize: 13824
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 3913 0 0 0 17985 15 0 0 25 0 1 0 545508549 14155776 3085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3456 3085 603 41 0 3415 0
vsize: 13824
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4088 0 0 0 18985 15 0 0 25 0 1 0 545508549 14868480 3259 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3630 3259 603 41 0 3589 0
vsize: 14520
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4088 0 0 0 19985 15 0 0 25 0 1 0 545508549 14868480 3259 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3630 3259 603 41 0 3589 0
vsize: 14520
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4152 0 0 0 20985 15 0 0 25 0 1 0 545508549 15138816 3322 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3696 3322 603 41 0 3655 0
vsize: 14784
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4152 0 0 0 21985 15 0 0 25 0 1 0 545508549 15138816 3322 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3696 3322 603 41 0 3655 0
vsize: 14784
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4209 0 0 0 22986 15 0 0 25 0 1 0 545508549 15355904 3379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3749 3379 603 41 0 3708 0
vsize: 14996
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4209 0 0 0 23986 15 0 0 25 0 1 0 545508549 15355904 3379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3749 3379 603 41 0 3708 0
vsize: 14996
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4218 0 0 0 24986 15 0 0 25 0 1 0 545508549 15388672 3387 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3757 3387 603 41 0 3716 0
vsize: 15028
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4218 0 0 0 25986 15 0 0 25 0 1 0 545508549 15388672 3387 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3757 3387 603 41 0 3716 0
vsize: 15028
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4387 0 0 0 26986 16 0 0 25 0 1 0 545508549 16076800 3555 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3925 3555 603 41 0 3884 0
vsize: 15700
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4387 0 0 0 27986 16 0 0 25 0 1 0 545508549 16076800 3555 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3925 3555 603 41 0 3884 0
vsize: 15700
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 28985 17 0 0 25 0 1 0 545508549 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+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 29985 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223640 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 30985 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 31985 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 32985 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 33986 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 34986 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 35986 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 36986 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 37987 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223600 134644281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 38987 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 39987 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 40987 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 41987 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 42988 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615807 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.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 43986 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 44986 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4503 0 0 0 45987 17 0 0 25 0 1 0 545508549 16424960 3638 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3638 603 41 0 3969 0
vsize: 16040
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 46987 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134616001 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 47987 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 48987 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221222976 134645479 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 49987 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 50987 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 51988 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 52988 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 53988 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 54988 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 55988 17 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 56988 18 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 57989 18 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 58989 18 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 59989 18 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 60989 18 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223648 134604802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 61989 18 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 62989 18 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4504 0 0 0 63990 18 0 0 25 0 1 0 545508549 16424960 3639 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4010 3639 603 41 0 3969 0
vsize: 16040
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4541 0 0 0 64990 18 0 0 25 0 1 0 545508549 16572416 3675 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3675 603 41 0 4005 0
vsize: 16184
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4541 0 0 0 65990 18 0 0 25 0 1 0 545508549 16572416 3675 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3675 603 41 0 4005 0
vsize: 16184
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4569 0 0 0 66990 18 0 0 25 0 1 0 545508549 16678912 3703 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4072 3703 603 41 0 4031 0
vsize: 16288
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 67989 18 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223536 134565149 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.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 68988 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 69988 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 70989 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223680 134614505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 71989 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 72989 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 73989 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 74989 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223584 134612848 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 75989 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 76990 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 77990 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 78990 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 79990 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 80990 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 81991 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 82991 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 83991 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 84991 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 85991 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 86991 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 87992 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 88992 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 89992 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4664 0 0 0 90992 19 0 0 25 0 1 0 545508549 16801792 3738 4294967295 134512640 134672761 3221224544 3221223744 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4102 3738 603 41 0 4061 0
vsize: 16408
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4750 0 0 0 91992 19 0 0 25 0 1 0 545508549 17178624 3824 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4194 3824 603 41 0 4153 0
vsize: 16776
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4750 0 0 0 92992 19 0 0 25 0 1 0 545508549 17178624 3824 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4194 3824 603 41 0 4153 0
vsize: 16776
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4754 0 0 0 93992 19 0 0 25 0 1 0 545508549 17186816 3827 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4196 3827 603 41 0 4155 0
vsize: 16784
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4754 0 0 0 94993 19 0 0 25 0 1 0 545508549 17186816 3827 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4196 3827 603 41 0 4155 0
vsize: 16784
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4762 0 0 0 95993 19 0 0 25 0 1 0 545508549 17219584 3834 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4204 3834 603 41 0 4163 0
vsize: 16816
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4762 0 0 0 96993 19 0 0 25 0 1 0 545508549 17219584 3834 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4204 3834 603 41 0 4163 0
vsize: 16816
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4784 0 0 0 97993 19 0 0 25 0 1 0 545508549 17285120 3855 4294967295 134512640 134672761 3221224544 3221223536 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4220 3855 603 41 0 4179 0
vsize: 16880
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4784 0 0 0 98993 19 0 0 25 0 1 0 545508549 17285120 3855 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4220 3855 603 41 0 4179 0
vsize: 16880
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4784 0 0 0 99993 19 0 0 25 0 1 0 545508549 17285120 3855 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4220 3855 603 41 0 4179 0
vsize: 16880
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4784 0 0 0 100994 19 0 0 25 0 1 0 545508549 17285120 3855 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4220 3855 603 41 0 4179 0
vsize: 16880
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4793 0 0 0 101994 19 0 0 25 0 1 0 545508549 17317888 3863 4294967295 134512640 134672761 3221224544 3221223668 134566136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4228 3863 603 41 0 4187 0
vsize: 16912
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4793 0 0 0 102994 19 0 0 25 0 1 0 545508549 17317888 3863 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4228 3863 603 41 0 4187 0
vsize: 16912
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4798 0 0 0 103994 19 0 0 25 0 1 0 545508549 17334272 3867 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4232 3867 603 41 0 4191 0
vsize: 16928
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4798 0 0 0 104994 19 0 0 25 0 1 0 545508549 17334272 3867 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4232 3867 603 41 0 4191 0
vsize: 16928
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4807 0 0 0 105994 19 0 0 25 0 1 0 545508549 17367040 3875 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4807 0 0 0 106995 19 0 0 25 0 1 0 545508549 17367040 3875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4807 0 0 0 107995 19 0 0 25 0 1 0 545508549 17367040 3875 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4807 0 0 0 108995 19 0 0 25 0 1 0 545508549 17367040 3875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 4807 0 0 0 109995 19 0 0 25 0 1 0 545508549 17367040 3875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3875 603 41 0 4199 0
vsize: 16960
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5081 0 0 0 110994 21 0 0 25 0 1 0 545508549 18485248 4148 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4148 603 41 0 4472 0
vsize: 18052
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5081 0 0 0 111994 21 0 0 25 0 1 0 545508549 18485248 4148 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4148 603 41 0 4472 0
vsize: 18052
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5081 0 0 0 112994 21 0 0 25 0 1 0 545508549 18485248 4148 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4513 4148 603 41 0 4472 0
vsize: 18052
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5231 0 0 0 113994 21 0 0 25 0 1 0 545508549 19075072 4297 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4657 4297 603 41 0 4616 0
vsize: 18628
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5231 0 0 0 114994 21 0 0 25 0 1 0 545508549 19075072 4297 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4657 4297 603 41 0 4616 0
vsize: 18628
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5231 0 0 0 115995 21 0 0 25 0 1 0 545508549 19075072 4297 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4657 4297 603 41 0 4616 0
vsize: 18628
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5232 0 0 0 116995 21 0 0 25 0 1 0 545508549 19075072 4298 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4657 4298 603 41 0 4616 0
vsize: 18628
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5232 0 0 0 117995 21 0 0 25 0 1 0 545508549 19075072 4298 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4657 4298 603 41 0 4616 0
vsize: 18628
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20018
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5232 0 0 0 118995 21 0 0 25 0 1 0 545508549 19075072 4298 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4657 4298 603 41 0 4616 0
vsize: 18628
[startup+1200.03 s]
Raw data (loadavg): 1.15 1.00 0.92 3/56 20066
Raw data (stat): 20018 (minisat+) R 20017 18865 18864 0 -1 0 5245 0 0 0 119994 22 0 0 25 0 1 0 545508549 19206144 4311 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4689 4311 603 41 0 4648 0
vsize: 18756
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.15 1.00 0.92 2/56 20066
Raw data (stat): 20018 (minisat+) Z 20017 18865 18864 0 -1 12 5246 0 0 0 119995 23 0 0 25 0 1 0 545508549 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.18
CPU user time (s): 1199.95
CPU system time (s): 0.231964
CPU usage (%): 100.011
Max. virtual memory (Kb): 18756
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####