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-markshare2.opb
MD5SUM	b54bb080800e2327586cd478559c04ff
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10368
Optimality of the best value was proved	NO
Number of terms in the objective function	140
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	7340025
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	7340025
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.09
Number of variables	200
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	7
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 18112

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 13:35:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18523 boxname=wulflinc29 idbench=1425 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b54bb080800e2327586cd478559c04ff  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare2.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare2.opb
IDLAUNCH: 18523
/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:        881464 kB
Buffers:          1948 kB
Cached:         128672 kB
SwapCached:        552 kB
Active:          22192 kB
Inactive:       110456 kB
HighTotal:      131008 kB
HighFree:        42420 kB
LowTotal:       903652 kB
LowFree:        839044 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14764 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:55:41 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 18523 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 431615   bits: 20/19
c ---[  10]---> Adder-cost: 380   maxlim: 461183   bits: 20/19
c ---[   8]---> Adder-cost: 350   maxlim: 445183   bits: 20/19
c ---[   6]---> Adder-cost: 340   maxlim: 477951   bits: 20/19
c ---[   4]---> Adder-cost: 390   maxlim: 451839   bits: 20/19
c ---[   2]---> Adder-cost: 358   maxlim: 468735   bits: 20/19
c ---[   0]---> Adder-cost: 374   maxlim: 444543   bits: 20/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   17605    63696 |    5281       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2592          
c   -- var.elim.:  2000/2592          
c   -- var.elim.:  2592/2592          
c   -- var.elim.:  281/281          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  118/118          
c |         0 |   16771    59554 |      --       0       --      -- |     --   | -418/-1339
c |         0 |   16771    59554 |    6708       0        0     nan |  0.000 % |
c |       101 |   16771    59554 |    7379     101      642     6.4 | 11.163 % |
c ==============================================================================
c (current CPU-time: 0.505923 s)
c ==============================================================================
c [1mFound solution: 1008128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1068     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 |       131 |   19413    65725 |    5823     131      793     6.1 | 11.163 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1003          
c   -- var.elim.:  1003/1003          
c   -- var.elim.:  541/541          
c   -- subsuming                       
c   -- var.elim.:  53/53          
c   -- var.elim.:  13/13          
c |       131 |   19058    66527 |      --     131       --      -- |     --   | -355/803
c |       131 |   19058    66527 |    7623     131      793     6.1 | 11.163 % |
c ==============================================================================
c (current CPU-time: 0.687895 s)
c ==============================================================================
c [1mFound solution: 974592[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 |       168 |   19155    66803 |    5746     168     1956    11.6 | 11.163 % |
c   -- subsuming                       
c   -- var.elim.:  177/177          
c   -- var.elim.:  113/113          
c |       168 |   19104    66872 |      --     168       --      -- |     --   | -51/70
c |       168 |   19104    66872 |    7641     168     1956    11.6 | 11.163 % |
c |       268 |   19104    66872 |    8405     268    12843    47.9 |  9.528 % |
c ==============================================================================
c (current CPU-time: 0.950855 s)
c ==============================================================================
c [1mFound solution: 937088[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 |       354 |   19198    67142 |    5759     354    16893    47.7 |  9.528 % |
c   -- subsuming                       
c   -- var.elim.:  167/167          
c   -- var.elim.:  110/110          
c |       354 |   19151    67253 |      --     354       --      -- |     --   | -47/112
c |       354 |   19151    67253 |    7660     354    16893    47.7 |  9.528 % |
c ==============================================================================
c (current CPU-time: 1.02384 s)
c ==============================================================================
c [1mFound solution: 912128[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 |       363 |   19231    67493 |    5769     363    17264    47.6 |  9.528 % |
c   -- subsuming                       
c   -- var.elim.:  153/153          
c   -- var.elim.:  101/101          
c |       363 |   19185    67821 |      --     363       --      -- |     --   | -46/329
c |       363 |   19185    67821 |    7674     363    17264    47.6 |  9.528 % |
c ==============================================================================
c (current CPU-time: 1.26681 s)
c ==============================================================================
c [1mFound solution: 894464[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 |       427 |   19239    67985 |    5771     427    34649    81.1 |  9.528 % |
c   -- subsuming                       
c   -- var.elim.:  117/117          
c   -- var.elim.:  75/75          
c |       427 |   19214    68189 |      --     427       --      -- |     --   | -25/205
c |       427 |   19214    68189 |    7685     427    34649    81.1 |  9.528 % |
c |       527 |   19214    68189 |    8454     527    36795    69.8 |  9.561 % |
c |       677 |   19214    68189 |    9299     677    39235    58.0 |  9.561 % |
c ==============================================================================
c (current CPU-time: 1.59476 s)
c ==============================================================================
c [1mFound solution: 873856[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 |       764 |   19273    68375 |    5781     764    56455    73.9 |  9.561 % |
c   -- subsuming                       
c   -- var.elim.:  125/125          
c   -- var.elim.:  90/90          
c |       764 |   19246    68474 |      --     764       --      -- |     --   | -27/100
c |       764 |   19246    68474 |    7698     764    56455    73.9 |  9.561 % |
c |       864 |   19246    68474 |    8468     864    82547    95.5 |  9.577 % |
c ==============================================================================
c (current CPU-time: 1.9437 s)
c ==============================================================================
c [1mFound solution: 843520[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     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 |       937 |   19283    68585 |    5784     937    89544    95.6 |  9.577 % |
c   -- subsuming                       
c   -- var.elim.:  72/72          
c   -- var.elim.:  49/49          
c |       937 |   19267    68644 |      --     937       --      -- |     --   | -16/60
c |       937 |   19267    68644 |    7706     937    89544    95.6 |  9.577 % |
c |      1038 |   19267    68644 |    8477    1038   116512   112.2 |  9.601 % |
c |      1188 |   19267    68644 |    9325    1188   127329   107.2 |  9.601 % |
c |      1413 |   19267    68644 |   10257    1413   168236   119.1 |  9.601 % |
c ==============================================================================
c (current CPU-time: 2.84757 s)
c ==============================================================================
c [1mFound solution: 797440[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 |      1421 |   19305    68755 |    5791    1421   168686   118.7 |  9.601 % |
c   -- subsuming                       
c   -- var.elim.:  71/71          
c   -- var.elim.:  49/49          
c |      1421 |   19290    68816 |      --    1421       --      -- |     --   | -15/62
c |      1421 |   19290    68816 |    7716    1421   168686   118.7 |  9.601 % |
c ==============================================================================
c (current CPU-time: 2.93755 s)
c ==============================================================================
c [1mFound solution: 738432[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 |      1434 |   19343    68990 |    5802    1434   169086   117.9 |  9.601 % |
c   -- subsuming                       
c   -- var.elim.:  119/119          
c   -- var.elim.:  86/86          
c |      1434 |   19312    68999 |      --    1434       --      -- |     --   | -31/10
c |      1434 |   19312    68999 |    7724    1434   169086   117.9 |  9.601 % |
c |      1534 |   19312    68999 |    8497    1534   184955   120.6 |  9.644 % |
c |      1684 |   19312    68999 |    9347    1684   211514   125.6 |  9.644 % |
c |      1910 |   19312    68999 |   10281    1910   238725   125.0 |  9.644 % |
c |      2248 |   19312    68999 |   11309    2248   276274   122.9 |  9.644 % |
c ==============================================================================
c (current CPU-time: 4.67429 s)
c ==============================================================================
c [1mFound solution: 727552[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 |      2535 |   19339    69103 |    5801    2535   322506   127.2 |  9.644 % |
c   -- subsuming                       
c   -- var.elim.:  75/75          
c   -- var.elim.:  58/58          
c |      2535 |   19322    69132 |      --    2535       --      -- |     --   | -17/30
c |      2535 |   19322    69132 |    7728    2535   322506   127.2 |  9.644 % |
c |      2636 |   19322    69132 |    8501    2636   339476   128.8 |  9.668 % |
c |      2787 |   19322    69132 |    9351    2787   375627   134.8 |  9.668 % |
c |      3012 |   19322    69132 |   10287    3012   425768   141.4 |  9.668 % |
c |      3350 |   19322    69132 |   11315    3350   491743   146.8 |  9.668 % |
c |      3856 |   19322    69132 |   12447    3856   617677   160.2 |  9.668 % |
c ==============================================================================
c (current CPU-time: 8.5227 s)
c ==============================================================================
c [1mFound solution: 699008[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 |      4174 |   19356    69263 |    5806    4174   657859   157.6 |  9.668 % |
c   -- subsuming                       
c   -- var.elim.:  95/95          
c   -- var.elim.:  72/72          
c |      4174 |   19333    69313 |      --    4174       --      -- |     --   | -23/51
c |      4174 |   19333    69313 |    7733    4174   657859   157.6 |  9.668 % |
c |      4275 |   19333    69313 |    8506    4275   667124   156.1 |  9.692 % |
c |      4425 |   19333    69313 |    9357    4425   703897   159.1 |  9.692 % |
c |      4651 |   19333    69313 |   10292    4651   763892   164.2 |  9.692 % |
c |      4988 |   19333    69313 |   11322    4988   824378   165.3 |  9.692 % |
c |      5494 |   19333    69313 |   12454    5494   920835   167.6 |  9.692 % |
c ==============================================================================
c (current CPU-time: 12.6121 s)
c ==============================================================================
c [1mFound solution: 682368[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 |      5774 |   19365    69439 |    5809    5774   967188   167.5 |  9.692 % |
c   -- subsuming                       
c   -- var.elim.:  93/93          
c   -- var.elim.:  72/72          
c |      5774 |   19344    69511 |      --    5774       --      -- |     --   | -21/73
c |      5774 |   19344    69511 |    7737    5774   967188   167.5 |  9.692 % |
c |      5877 |   19344    69511 |    8511    5877   989023   168.3 |  9.716 % |
c |      6028 |   19344    69511 |    9362    6028   993765   164.9 |  9.716 % |
c ==============================================================================
c (current CPU-time: 13.199 s)
c ==============================================================================
c [1mFound solution: 643200[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 |      6051 |   19390    69670 |    5816    6051   998582   165.0 |  9.716 % |
c   -- subsuming                       
c   -- var.elim.:  112/112          
c   -- var.elim.:  83/83          
c |      6051 |   19365    69811 |      --    6051       --      -- |     --   | -25/142
c |      6051 |   19365    69811 |    7746    6051   998582   165.0 |  9.716 % |
c ==============================================================================
c (current CPU-time: 13.38 s)
c ==============================================================================
c [1mFound solution: 616192[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 |      6064 |   19404    69947 |    5821    6064   999049   164.8 |  9.716 % |
c   -- subsuming                       
c   -- var.elim.:  97/97          
c   -- var.elim.:  71/71          
c |      6064 |   19383    70181 |      --    6064       --      -- |     --   | -21/235
c |      6064 |   19383    70181 |    7753    6064   999049   164.8 |  9.716 % |
c |      6164 |   19383    70181 |    8528    6164  1020544   165.6 |  9.755 % |
c |      6315 |   19383    70181 |    9381    6315  1049389   166.2 |  9.755 % |
c |      6540 |   19383    70181 |   10319    6540  1093398   167.2 |  9.755 % |
c |      6877 |   19383    70181 |   11351    6877  1115242   162.2 |  9.755 % |
c ==============================================================================
c (current CPU-time: 14.8917 s)
c ==============================================================================
c [1mFound solution: 582528[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 |      7035 |   19423    70327 |    5826    7035  1117300   158.8 |  9.755 % |
c   -- subsuming                       
c   -- var.elim.:  106/106          
c   -- var.elim.:  80/80          
c |      7035 |   19397    70416 |      --    7035       --      -- |     --   | -26/90
c |      7035 |   19397    70416 |    7758    7035  1117300   158.8 |  9.755 % |
c |      7137 |   19397    70416 |    8534    7137  1130019   158.3 |  9.779 % |
c |      7287 |   19397    70416 |    9388    7287  1141688   156.7 |  9.779 % |
c |      7512 |   19397    70416 |   10326    7512  1180119   157.1 |  9.779 % |
c |      7849 |   19397    70416 |   11359    7849  1213275   154.6 |  9.779 % |
c ==============================================================================
c (current CPU-time: 16.7844 s)
c ==============================================================================
c [1mFound solution: 536448[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 |      8055 |   19439    70564 |    5831    8055  1222529   151.8 |  9.779 % |
c   -- subsuming                       
c   -- var.elim.:  106/106          
c   -- var.elim.:  81/81          
c |      8055 |   19414    70559 |      --    8055       --      -- |     --   | -25/-4
c |      8055 |   19414    70559 |    7765    8055  1222529   151.8 |  9.779 % |
c |      8156 |   19414    70559 |    8542    8156  1233274   151.2 |  9.800 % |
c |      8307 |   19414    70559 |    9396    8307  1244656   149.8 |  9.800 % |
c |      8532 |   19414    70559 |   10336    8532  1290491   151.3 |  9.800 % |
c |      8870 |   19414    70559 |   11369    8870  1329239   149.9 |  9.800 % |
c ==============================================================================
c (current CPU-time: 19.0831 s)
c ==============================================================================
c [1mFound solution: 532864[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 |      9033 |   19458    70710 |    5837    9033  1345037   148.9 |  9.800 % |
c   -- subsuming                       
c   -- var.elim.:  107/107          
c   -- var.elim.:  80/80          
c |      9033 |   19431    70735 |      --    9033       --      -- |     --   | -27/26
c |      9033 |   19431    70735 |    7772    9033  1345037   148.9 |  9.800 % |
c |      9134 |   19431    70735 |    8549    6123   745039   121.7 |  9.824 % |
c |      9284 |   19431    70735 |    9404    6273   774430   123.5 |  9.824 % |
c |      9509 |   19431    70735 |   10345    6498   798478   122.9 |  9.824 % |
c |      9847 |   19431    70735 |   11379    6836   872178   127.6 |  9.824 % |
c |     10354 |   19431    70735 |   12517    7343   922209   125.6 |  9.824 % |
c |     11114 |   19431    70735 |   13769    8103  1067291   131.7 |  9.824 % |
c |     12253 |   19431    70735 |   15146    9242  1240920   134.3 |  9.824 % |
c ==============================================================================
c (current CPU-time: 26.8999 s)
c ==============================================================================
c [1mFound solution: 529408[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 |     12384 |   19470    70874 |    5840    9373  1260283   134.5 |  9.824 % |
c   -- subsuming                       
c   -- var.elim.:  100/100          
c   -- var.elim.:  77/77          
c |     12384 |   19447    70853 |      --    9373       --      -- |     --   | -23/-20
c |     12384 |   19447    70853 |    7778    9373  1260283   134.5 |  9.824 % |
c |     12484 |   19447    70853 |    8556    6349   720632   113.5 |  9.845 % |
c |     12634 |   19447    70853 |    9412    6499   731720   112.6 |  9.845 % |
c |     12860 |   19447    70853 |   10353    6725   769534   114.4 |  9.845 % |
c |     13197 |   19447    70853 |   11388    7062   806799   114.2 |  9.845 % |
c |     13703 |   19447    70853 |   12527    7568   892965   118.0 |  9.845 % |
c |     14462 |   19447    70853 |   13780    8327   980003   117.7 |  9.845 % |
c ==============================================================================
c (current CPU-time: 31.6182 s)
c ==============================================================================
c [1mFound solution: 520320[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 |     14655 |   19475    70949 |    5842    8520   982915   115.4 |  9.845 % |
c   -- subsuming                       
c   -- var.elim.:  66/66          
c   -- var.elim.:  48/48          
c |     14655 |   19462    71109 |      --    8520       --      -- |     --   | -13/161
c |     14655 |   19462    71109 |    7784    8520   982915   115.4 |  9.845 % |
c |     14757 |   19462    71109 |    8563    5782   573204    99.1 |  9.869 % |
c |     14907 |   19462    71109 |    9419    5932   575482    97.0 |  9.869 % |
c |     15132 |   19462    71109 |   10361    6157   612909    99.5 |  9.869 % |
c |     15470 |   19462    71109 |   11397    6495   655321   100.9 |  9.869 % |
c |     15977 |   19462    71109 |   12537    7002   691552    98.8 |  9.869 % |
c ==============================================================================
c (current CPU-time: 33.9578 s)
c ==============================================================================
c [1mFound solution: 79232[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     16276 |   19481    71182 |    5844    7301   699886    95.9 |  9.869 % |
c   -- subsuming                       
c   -- var.elim.:  90/90          
c   -- var.elim.:  96/96          
c   -- var.elim.:  35/35          
c   -- var.elim.:  122/122          
c   -- var.elim.:  134/134          
c   -- var.elim.:  62/62          
c   -- subsuming                       
c   -- var.elim.:  42/42          
c   -- var.elim.:  93/93          
c   -- var.elim.:  20/20          
c |     16276 |   19015    66677 |      --    7301       --      -- |     --   | -431/-4395
c |     16276 |   19015    66677 |    7606    5159   280772    54.4 |  9.869 % |
c |     16377 |   19015    66677 |    8366    5260   282515    53.7 | 10.315 % |
c |     16527 |   19015    66677 |    9203    5410   283633    52.4 | 10.315 % |
c |     16754 |   19015    66677 |   10123    5637   289736    51.4 | 10.315 % |
c |     17092 |   19015    66677 |   11135    5975   300153    50.2 | 10.315 % |
c |     17598 |   19015    66677 |   12249    6481   318903    49.2 | 10.315 % |
c |     18357 |   19015    66677 |   13474    7240   353579    48.8 | 10.315 % |
c |     19496 |   19015    66677 |   14821    8379   392273    46.8 | 10.315 % |
c ==============================================================================
c (current CPU-time: 37.6583 s)
c ==============================================================================
c [1mFound solution: 69248[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20586 |   19044    66787 |    5713    9469   453401    47.9 | 10.315 % |
c   -- subsuming                       
c   -- var.elim.:  105/105          
c   -- var.elim.:  63/63          
c |     20586 |   19027    66713 |      --    9469       --      -- |     --   | -17/-73
c |     20586 |   19027    66713 |    7610    9469   453401    47.9 | 10.315 % |
c |     20687 |   19027    66713 |    8371    6414   205475    32.0 | 10.335 % |
c |     20837 |   19027    66713 |    9209    6564   207588    31.6 | 10.335 % |
c |     21062 |   19027    66713 |   10129    6789   216061    31.8 | 10.335 % |
c |     21400 |   19027    66713 |   11142    7127   224432    31.5 | 10.335 % |
c |     21906 |   19027    66713 |   12257    7633   248939    32.6 | 10.335 % |
c |     22665 |   19027    66713 |   13482    8392   273347    32.6 | 10.335 % |
c |     23804 |   19027    66713 |   14831    9531   307531    32.3 | 10.335 % |
c |     25513 |   18999    66300 |   16290   11239   422171    37.6 | 10.396 % |
c |     28076 |   18973    66212 |   17894   13801   521065    37.8 | 10.487 % |
c |     31920 |   18959    66161 |   19669   17644   662885    37.6 | 10.547 % |
c |     37687 |   18951    66136 |   21627   15227   654030    43.0 | 10.607 % |
c |     46338 |   18951    66136 |   23790   14410   759934    52.7 | 10.607 % |
c |     59313 |   18951    66136 |   26169   14858   622138    41.9 | 10.607 % |
c |     78774 |   18951    66136 |   28786   19617  1353212    69.0 | 10.607 % |
c |    107967 |   18862    65843 |   31516   15328   749407    48.9 | 11.061 % |
c |    151757 |   18862    65843 |   34668   21228  1163056    54.8 | 11.061 % |
c |    217444 |   18848    65797 |   38106   20779  1335582    64.3 | 11.121 % |
c |    315970 |   18779    65572 |   41763   21104  1280497    60.7 | 11.484 % |
c |    463760 |   18764    65521 |   45903   16197  1050012    64.8 | 11.575 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -s01_bit_7 -s01_bit_6 -s01_bit_5 -s01_bit_4 -s01_bit_3 -s01_bit_2 -s01_bit_1 -s01_bit0 s01_bit1 -s01_bit2 s01_bit3 -s01_bit4 -s01_bit5 s01_bit6 s01_bit7 -s01_bit8 -s01_bit9 -s01_bit10 -s01_bit11 -s01_bit12 -s11_bit_7 -s11_bit_6 -s11_bit_5 -s11_bit_4 -s11_bit_3 -s11_bit_2 -s11_bit_1 -s11_bit0 s11_bit1 s11_bit2 -s11_bit3 s11_bit4 -s11_bit5 s11_bit6 -s11_bit7 -s11_bit8 -s11_bit9 -s11_bit10 -s11_bit11 -s11_bit12 -s21_bit_7 -s21_bit_6 -s21_bit_5 -s21_bit_4 -s21_bit_3 -s21_bit_2 -s21_bit_1 s21_bit0 -s21_bit1 s21_bit2 s21_bit3 -s21_bit4 s21_bit5 -s21_bit6 -s21_bit7 -s21_bit8 -s21_bit9 -s21_bit10 -s21_bit11 -s21_bit12 -s31_bit_7 -s31_bit_6 -s31_bit_5 -s31_bit_4 -s31_bit_3 -s31_bit_2 -s31_bit_1 s31_bit0 s31_bit1 s31_bit2 s31_bit3 -s31_bit4 s31_bit5 -s31_bit6 -s31_bit7 -s31_bit8 -s31_bit9 -s31_bit10 -s31_bit11 -s31_bit12 -s41_bit_7 -s41_bit_6 -s41_bit_5 -s41_bit_4 -s41_bit_3 -s41_bit_2 -s41_bit_1 -s41_bit0 -s41_bit1 -s41_bit2 -s41_bit3 s41_bit4 s41_bit5 -s41_bit6 -s41_bit7 -s41_bit8 -s41_bit9 -s41_bit10 -s41_bit11 -s41_bit12 -s51_bit_7 -s51_bit_6 -s51_bit_5 -s51_bit_4 -s51_bit_3 -s51_bit_2 -s51_bit_1 -s51_bit0 -s51_bit1 s51_bit2 -s51_bit3 -s51_bit4 -s51_bit5 s51_bit6 -s51_bit7 -s51_bit8 -s51_bit9 -s51_bit10 -s51_bit11 -s51_bit12 -s61_bit_7 -s61_bit_6 -s61_bit_5 -s61_bit_4 -s61_bit_3 -s61_bit_2 -s61_bit_1 s61_bit0 -s61_bit1 s61_bit2 s61_bit3 -s61_bit4 s61_bit5 -s61_bit6 -s61_bit7 -s61_bit8 -s61_bit9 -s61_bit10 -s61_bit11 -s61_bit12 -x0_bit0 x1_bit0 x2_bit0 x3_bit0 x4_bit0 -x5_bit0 -x6_bit0 -x7_bit0 -x8_bit0 x9_bit0 -x10_bit0 -x11_bit0 -x12_bit0 -x13_bit0 x14_bit0 -x15_bit0 x16_bit0 x17_bit0 -x18_bit0 -x19_bit0 -x20_bit0 x21_bit0 -x22_bit0 x23_bit0 x24_bit0 -x25_bit0 x26_bit0 x27_bit0 -x28_bit0 x29_bit0 -x30_bit0 x#### 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.58 0.82 0.89 2/54 32403
Raw data (stat): 32403 (runsolver) R 32402 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545481398 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.0005 s]
Raw data (loadavg): 0.64 0.82 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 3077 0 0 0 990 8 0 0 25 0 1 0 545481398 9822208 1922 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2398 1922 603 41 0 2357 0
vsize: 9592
[startup+20.0012 s]
Raw data (loadavg): 0.70 0.83 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 4581 0 0 0 1985 13 0 0 25 0 1 0 545481398 12853248 2675 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3138 2675 603 41 0 3097 0
vsize: 12552
[startup+30.0019 s]
Raw data (loadavg): 0.74 0.83 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 4699 0 0 0 2983 14 0 0 25 0 1 0 545481398 12648448 2625 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3088 2625 603 41 0 3047 0
vsize: 12352
[startup+40.0022 s]
Raw data (loadavg): 0.78 0.84 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 5208 0 0 0 3981 16 0 0 25 0 1 0 545481398 12648448 2627 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3088 2627 603 41 0 3047 0
vsize: 12352
[startup+50.0028 s]
Raw data (loadavg): 0.81 0.84 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 5208 0 0 0 4981 16 0 0 25 0 1 0 545481398 12648448 2627 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3088 2627 603 41 0 3047 0
vsize: 12352
[startup+60.0022 s]
Raw data (loadavg): 0.84 0.85 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 5229 0 0 0 5981 16 0 0 25 0 1 0 545481398 12779520 2648 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3120 2648 603 41 0 3079 0
vsize: 12480
[startup+70.0033 s]
Raw data (loadavg): 0.87 0.85 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 5230 0 0 0 6981 16 0 0 25 0 1 0 545481398 12779520 2649 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3120 2649 603 41 0 3079 0
vsize: 12480
[startup+80.0041 s]
Raw data (loadavg): 0.89 0.86 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 5423 0 0 0 7981 16 0 0 25 0 1 0 545481398 13557760 2842 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3310 2842 603 41 0 3269 0
vsize: 13240
[startup+90.0036 s]
Raw data (loadavg): 0.90 0.86 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 5423 0 0 0 8981 16 0 0 25 0 1 0 545481398 13557760 2842 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3310 2842 603 41 0 3269 0
vsize: 13240
[startup+100.004 s]
Raw data (loadavg): 0.92 0.86 0.90 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 5541 0 0 0 9981 17 0 0 25 0 1 0 545481398 14082048 2960 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3438 2960 603 41 0 3397 0
vsize: 13752
[startup+110.003 s]
Raw data (loadavg): 0.93 0.87 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 5745 0 0 0 10980 18 0 0 25 0 1 0 545481398 14864384 3164 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3629 3164 603 41 0 3588 0
vsize: 14516
[startup+120.004 s]
Raw data (loadavg): 0.94 0.87 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 5745 0 0 0 11980 18 0 0 25 0 1 0 545481398 14864384 3164 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3629 3164 603 41 0 3588 0
vsize: 14516
[startup+130.004 s]
Raw data (loadavg): 0.95 0.88 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6090 0 0 0 12978 19 0 0 25 0 1 0 545481398 16314368 3509 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3983 3509 603 41 0 3942 0
vsize: 15932
[startup+140.005 s]
Raw data (loadavg): 0.96 0.88 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6178 0 0 0 13978 20 0 0 25 0 1 0 545481398 16822272 3597 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4107 3597 603 41 0 4066 0
vsize: 16428
[startup+150.004 s]
Raw data (loadavg): 0.96 0.88 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6178 0 0 0 14978 20 0 0 25 0 1 0 545481398 16822272 3597 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4107 3597 603 41 0 4066 0
vsize: 16428
[startup+160.004 s]
Raw data (loadavg): 0.97 0.89 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6179 0 0 0 15978 20 0 0 25 0 1 0 545481398 16822272 3598 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4107 3598 603 41 0 4066 0
vsize: 16428
[startup+170.005 s]
Raw data (loadavg): 0.97 0.89 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6179 0 0 0 16979 20 0 0 25 0 1 0 545481398 16822272 3598 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4107 3598 603 41 0 4066 0
vsize: 16428
[startup+180.005 s]
Raw data (loadavg): 0.98 0.89 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6179 0 0 0 17979 20 0 0 25 0 1 0 545481398 16822272 3598 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4107 3598 603 41 0 4066 0
vsize: 16428
[startup+190.005 s]
Raw data (loadavg): 0.98 0.90 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6343 0 0 0 18978 20 0 0 25 0 1 0 545481398 17346560 3762 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4235 3762 603 41 0 4194 0
vsize: 16940
[startup+200.006 s]
Raw data (loadavg): 1.06 0.91 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6343 0 0 0 19978 20 0 0 25 0 1 0 545481398 17346560 3762 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4235 3762 603 41 0 4194 0
vsize: 16940
[startup+210.005 s]
Raw data (loadavg): 1.05 0.92 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6343 0 0 0 20979 20 0 0 25 0 1 0 545481398 17346560 3762 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4235 3762 603 41 0 4194 0
vsize: 16940
[startup+220.005 s]
Raw data (loadavg): 1.04 0.92 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6534 0 0 0 21978 21 0 0 25 0 1 0 545481398 18128896 3953 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4426 3953 603 41 0 4385 0
vsize: 17704
[startup+230.006 s]
Raw data (loadavg): 1.03 0.92 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6534 0 0 0 22979 21 0 0 25 0 1 0 545481398 18128896 3953 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4426 3953 603 41 0 4385 0
vsize: 17704
[startup+240.005 s]
Raw data (loadavg): 1.03 0.92 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6534 0 0 0 23979 21 0 0 25 0 1 0 545481398 18128896 3953 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4426 3953 603 41 0 4385 0
vsize: 17704
[startup+250.006 s]
Raw data (loadavg): 1.02 0.92 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6607 0 0 0 24979 21 0 0 25 0 1 0 545481398 18391040 3991 4294967295 134512640 134672761 3221224544 3221223696 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+260.006 s]
Raw data (loadavg): 1.02 0.93 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6607 0 0 0 25979 21 0 0 25 0 1 0 545481398 18391040 3991 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+270.007 s]
Raw data (loadavg): 1.02 0.93 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6607 0 0 0 26979 21 0 0 25 0 1 0 545481398 18391040 3991 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+280.007 s]
Raw data (loadavg): 1.01 0.93 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6607 0 0 0 27979 21 0 0 25 0 1 0 545481398 18391040 3991 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+290.007 s]
Raw data (loadavg): 1.01 0.93 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6642 0 0 0 28979 21 0 0 25 0 1 0 545481398 18391040 3991 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+300.007 s]
Raw data (loadavg): 1.01 0.93 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6642 0 0 0 29980 21 0 0 25 0 1 0 545481398 18391040 3991 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+310.007 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6642 0 0 0 30980 21 0 0 25 0 1 0 545481398 18391040 3991 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+320.008 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6661 0 0 0 31980 21 0 0 25 0 1 0 545481398 18436096 4002 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4501 4002 603 41 0 4460 0
vsize: 18004
[startup+330.007 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6661 0 0 0 32980 21 0 0 25 0 1 0 545481398 18436096 4002 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4501 4002 603 41 0 4460 0
vsize: 18004
[startup+340.007 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6661 0 0 0 33980 21 0 0 25 0 1 0 545481398 18436096 4002 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4501 4002 603 41 0 4460 0
vsize: 18004
[startup+350.008 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 6661 0 0 0 34980 21 0 0 25 0 1 0 545481398 18436096 4002 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4501 4002 603 41 0 4460 0
vsize: 18004
[startup+360.008 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 7062 0 0 0 35979 22 0 0 25 0 1 0 545481398 20148224 4403 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4403 603 41 0 4878 0
vsize: 19676
[startup+370.009 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 7436 0 0 0 36978 24 0 0 25 0 1 0 545481398 21598208 4777 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5273 4777 603 41 0 5232 0
vsize: 21092
[startup+380.009 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 7495 0 0 0 37978 24 0 0 25 0 1 0 545481398 21794816 4828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5321 4828 603 41 0 5280 0
vsize: 21284
[startup+390.009 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 7495 0 0 0 38978 24 0 0 25 0 1 0 545481398 21794816 4828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5321 4828 603 41 0 5280 0
vsize: 21284
[startup+400.01 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 7495 0 0 0 39979 24 0 0 25 0 1 0 545481398 21794816 4828 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5321 4828 603 41 0 5280 0
vsize: 21284
[startup+410.01 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 7495 0 0 0 40979 24 0 0 25 0 1 0 545481398 21794816 4828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5321 4828 603 41 0 5280 0
vsize: 21284
[startup+420.01 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 7517 0 0 0 41979 24 0 0 25 0 1 0 545481398 21925888 4850 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5353 4850 603 41 0 5312 0
vsize: 21412
[startup+430.011 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 7831 0 0 0 42978 25 0 0 25 0 1 0 545481398 23248896 5164 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5676 5164 603 41 0 5635 0
vsize: 22704
[startup+440.01 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8123 0 0 0 43977 26 0 0 25 0 1 0 545481398 24436736 5456 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5966 5456 603 41 0 5925 0
vsize: 23864
[startup+450.01 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8377 0 0 0 44977 26 0 0 25 0 1 0 545481398 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+460.011 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8377 0 0 0 45977 26 0 0 25 0 1 0 545481398 25387008 5702 4294967295 134512640 134672761 3221224544 3221223720 134553587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+470.011 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8377 0 0 0 46977 26 0 0 25 0 1 0 545481398 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+480.012 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8377 0 0 0 47978 26 0 0 25 0 1 0 545481398 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+490.012 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8377 0 0 0 48978 26 0 0 25 0 1 0 545481398 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+500.012 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8377 0 0 0 49978 26 0 0 25 0 1 0 545481398 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+510.012 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8416 0 0 0 50978 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+520.013 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8416 0 0 0 51978 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+530.013 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8416 0 0 0 52978 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+540.013 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8416 0 0 0 53979 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+550.014 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8416 0 0 0 54979 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+560.014 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8454 0 0 0 55979 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+570.016 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8454 0 0 0 56979 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+580.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8454 0 0 0 57979 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+590.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8454 0 0 0 58980 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+600.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8454 0 0 0 59980 27 0 0 25 0 1 0 545481398 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+610.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8456 0 0 0 60980 27 0 0 25 0 1 0 545481398 25378816 5702 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5702 603 41 0 6155 0
vsize: 24784
[startup+620.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8502 0 0 0 61980 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+630.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8502 0 0 0 62980 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+640.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8502 0 0 0 63981 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+650.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8502 0 0 0 64981 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+660.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8502 0 0 0 65981 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+670.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8544 0 0 0 66981 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+680.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8544 0 0 0 67981 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+690.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8544 0 0 0 68982 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+700.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8544 0 0 0 69982 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+710.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8544 0 0 0 70982 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+720.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8544 0 0 0 71982 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+730.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8544 0 0 0 72982 27 0 0 25 0 1 0 545481398 25321472 5692 4294967295 134512640 134672761 3221224544 3221223584 134612992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+740.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8787 0 0 0 73982 28 0 0 25 0 1 0 545481398 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+750.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8787 0 0 0 74982 28 0 0 25 0 1 0 545481398 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+760.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8787 0 0 0 75982 28 0 0 25 0 1 0 545481398 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+770.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8787 0 0 0 76982 28 0 0 25 0 1 0 545481398 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+780.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8787 0 0 0 77982 28 0 0 25 0 1 0 545481398 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+790.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8787 0 0 0 78982 28 0 0 25 0 1 0 545481398 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+800.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8787 0 0 0 79983 28 0 0 25 0 1 0 545481398 26267648 5923 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+810.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 8961 0 0 0 80982 28 0 0 25 0 1 0 545481398 27058176 6097 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6606 6097 603 41 0 6565 0
vsize: 26424
[startup+820.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9161 0 0 0 81981 29 0 0 25 0 1 0 545481398 27754496 6285 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+830.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9161 0 0 0 82981 29 0 0 25 0 1 0 545481398 27754496 6285 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+840.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9161 0 0 0 83982 29 0 0 25 0 1 0 545481398 27754496 6285 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+850.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9161 0 0 0 84982 29 0 0 25 0 1 0 545481398 27754496 6285 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+860.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9161 0 0 0 85982 29 0 0 25 0 1 0 545481398 27754496 6285 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+870.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9161 0 0 0 86982 29 0 0 25 0 1 0 545481398 27754496 6285 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+880.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9162 0 0 0 87982 29 0 0 25 0 1 0 545481398 27754496 6286 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6776 6286 603 41 0 6735 0
vsize: 27104
[startup+890.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9472 0 0 0 88982 30 0 0 25 0 1 0 545481398 29069312 6596 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7097 6596 603 41 0 7056 0
vsize: 28388
[startup+900.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9804 0 0 0 89980 32 0 0 25 0 1 0 545481398 30511104 6928 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7449 6928 603 41 0 7408 0
vsize: 29796
[startup+910.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9923 0 0 0 90980 32 0 0 25 0 1 0 545481398 30736384 7005 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7504 7005 603 41 0 7463 0
vsize: 30016
[startup+920.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9923 0 0 0 91980 32 0 0 25 0 1 0 545481398 30736384 7005 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7504 7005 603 41 0 7463 0
vsize: 30016
[startup+930.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9923 0 0 0 92980 32 0 0 25 0 1 0 545481398 30736384 7005 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7504 7005 603 41 0 7463 0
vsize: 30016
[startup+940.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9923 0 0 0 93981 32 0 0 25 0 1 0 545481398 30736384 7005 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7504 7005 603 41 0 7463 0
vsize: 30016
[startup+950.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9923 0 0 0 94981 32 0 0 25 0 1 0 545481398 30736384 7005 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7504 7005 603 41 0 7463 0
vsize: 30016
[startup+960.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9986 0 0 0 95981 33 0 0 25 0 1 0 545481398 30818304 7026 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7026 603 41 0 7483 0
vsize: 30096
[startup+970.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9986 0 0 0 96981 33 0 0 25 0 1 0 545481398 30818304 7026 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7026 603 41 0 7483 0
vsize: 30096
[startup+980.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9986 0 0 0 97981 33 0 0 25 0 1 0 545481398 30818304 7026 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7026 603 41 0 7483 0
vsize: 30096
[startup+990.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9986 0 0 0 98981 33 0 0 25 0 1 0 545481398 30818304 7026 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7026 603 41 0 7483 0
vsize: 30096
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9986 0 0 0 99982 33 0 0 25 0 1 0 545481398 30818304 7026 4294967295 134512640 134672761 3221224544 3221223584 134612659 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7026 603 41 0 7483 0
vsize: 30096
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 9989 0 0 0 100982 33 0 0 25 0 1 0 545481398 30818304 7029 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7029 603 41 0 7483 0
vsize: 30096
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10039 0 0 0 101982 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10039 0 0 0 102982 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10039 0 0 0 103982 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10039 0 0 0 104982 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10039 0 0 0 105983 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10039 0 0 0 106983 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10039 0 0 0 107983 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10085 0 0 0 108983 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10085 0 0 0 109983 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615541 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10085 0 0 0 110984 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10085 0 0 0 111984 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10085 0 0 0 112984 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10085 0 0 0 113984 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10131 0 0 0 114984 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10131 0 0 0 115984 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10131 0 0 0 116985 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10131 0 0 0 117985 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10131 0 0 0 118985 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32403
Raw data (stat): 32403 (minisat+) R 32402 27222 27221 0 -1 0 10131 0 0 0 119985 33 0 0 25 0 1 0 545481398 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 32403
Raw data (stat): 32403 (minisat+) Z 32402 27222 27221 0 -1 12 10132 0 0 0 119985 34 0 0 25 0 1 0 545481398 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.2
CPU user time (s): 1199.86
CPU system time (s): 0.345947
CPU usage (%): 100.013
Max. virtual memory (Kb): 30096
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####