PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare2.opb
MD5SUM	3b5121187baf09367bd50bdc4d869d21
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	8448
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.43
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 18689

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        745436 kB
Buffers:          6304 kB
Cached:         257876 kB
SwapCached:          0 kB
Active:          55140 kB
Inactive:       212164 kB
HighTotal:      131008 kB
HighFree:        19768 kB
LowTotal:       903652 kB
LowFree:        725668 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              56 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16232 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 16:21:36 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 17652 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.492925 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.675897 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.939857 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.01085 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.25381 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.58376 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.92971 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.83357 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.91956 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.65429 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.49071 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.5601 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.148 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.331 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.8387 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.7215 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: 18.9981 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.7539 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.4342 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.7629 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.4473 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 -x1_bit_7 -x1_bit_6 -x1_bit_5 -x1_bit_4 -x1_bit_3 -x1_bit_2 -x1_bit_1 -x1_bit0 x1_bit1 -x1_bit2 x1_bit3 -x1_bit4 -x1_bit5 x1_bit6 x1_bit7 -x1_bit8 -x1_bit9 -x1_bit10 -x1_bit11 -x1_bit12 -x3_bit_7 -x3_bit_6 -x3_bit_5 -x3_bit_4 -x3_bit_3 -x3_bit_2 -x3_bit_1 -x3_bit0 x3_bit1 x3_bit2 -x3_bit3 x3_bit4 -x3_bit5 x3_bit6 -x3_bit7 -x3_bit8 -x3_bit9 -x3_bit10 -x3_bit11 -x3_bit12 -x5_bit_7 -x5_bit_6 -x5_bit_5 -x5_bit_4 -x5_bit_3 -x5_bit_2 -x5_bit_1 x5_bit0 -x5_bit1 x5_bit2 x5_bit3 -x5_bit4 x5_bit5 -x5_bit6 -x5_bit7 -x5_bit8 -x5_bit9 -x5_bit10 -x5_bit11 -x5_bit12 -x7_bit_7 -x7_bit_6 -x7_bit_5 -x7_bit_4 -x7_bit_3 -x7_bit_2 -x7_bit_1 x7_bit0 x7_bit1 x7_bit2 x7_bit3 -x7_bit4 x7_bit5 -x7_bit6 -x7_bit7 -x7_bit8 -x7_bit9 -x7_bit10 -x7_bit11 -x7_bit12 -x9_bit_7 -x9_bit_6 -x9_bit_5 -x9_bit_4 -x9_bit_3 -x9_bit_2 -x9_bit_1 -x9_bit0 -x9_bit1 -x9_bit2 -x9_bit3 x9_bit4 x9_bit5 -x9_bit6 -x9_bit7 -x9_bit8 -x9_bit9 -x9_bit10 -x9_bit11 -x9_bit12 -x11_bit_7 -x11_bit_6 -x11_bit_5 -x11_bit_4 -x11_bit_3 -x11_bit_2 -x11_bit_1 -x11_bit0 -x11_bit1 x11_bit2 -x11_bit3 -x11_bit4 -x11_bit5 x11_bit6 -x11_bit7 -x11_bit8 -x11_bit9 -x11_bit10 -x11_bit11 -x11_bit12 -x13_bit_7 -x13_bit_6 -x13_bit_5 -x13_bit_4 -x13_bit_3 -x13_bit_2 -x13_bit_1 x13_bit0 -x13_bit1 x13_bit2 x13_bit3 -x13_bit4 x13_bit5 -x13_bit6 -x13_bit7 -x13_bit8 -x13_bit9 -x13_bit10 -x13_bit11 -x13_bit12 -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 x31_bit0 x32_bit0 -x33_bit0 -x34_bit0 -x35_bit0 x36_bit0 -x37_bit0 x38_bit0 x39_bit0 -x40_bit0 x41_bit0 x42_bit0 -x43_bit0 x44_bit0 -x45_bit0 x46_bit0 x47_bit0 -x48_bit0 x49_bit0 -x50_bit0 x51_bit0 -x52_bit0 x53_bit0 x54_bit0 -x55#### 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.48 0.84 0.87 2/56 29959
Raw data (stat): 29959 (runsolver) R 29958 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 431283541 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 s]
Raw data (loadavg): 0.56 0.84 0.87 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 3079 0 0 0 989 9 0 0 25 0 1 0 431283541 9822208 1924 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2398 1924 603 41 0 2357 0
vsize: 9592
[startup+19.9998 s]
Raw data (loadavg): 0.63 0.85 0.87 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 4581 0 0 0 1985 14 0 0 25 0 1 0 431283541 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.0006 s]
Raw data (loadavg): 0.68 0.85 0.87 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 4699 0 0 0 2985 14 0 0 25 0 1 0 431283541 12648448 2625 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3088 2625 603 41 0 3047 0
vsize: 12352
[startup+40.0004 s]
Raw data (loadavg): 0.73 0.86 0.87 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 5208 0 0 0 3982 17 0 0 25 0 1 0 431283541 12648448 2627 4294967295 134512640 134672761 3221224544 3221223584 134612987 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.0015 s]
Raw data (loadavg): 0.77 0.86 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 5208 0 0 0 4982 17 0 0 25 0 1 0 431283541 12648448 2627 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3088 2627 603 41 0 3047 0
vsize: 12352
[startup+60.0017 s]
Raw data (loadavg): 0.81 0.86 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 5229 0 0 0 5982 17 0 0 25 0 1 0 431283541 12779520 2648 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2648 603 41 0 3079 0
vsize: 12480
[startup+70.0015 s]
Raw data (loadavg): 0.84 0.87 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 5230 0 0 0 6982 17 0 0 25 0 1 0 431283541 12779520 2649 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2649 603 41 0 3079 0
vsize: 12480
[startup+80.0023 s]
Raw data (loadavg): 0.86 0.87 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 5423 0 0 0 7981 18 0 0 25 0 1 0 431283541 13557760 2842 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3310 2842 603 41 0 3269 0
vsize: 13240
[startup+90.0021 s]
Raw data (loadavg): 0.88 0.87 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 5423 0 0 0 8981 18 0 0 25 0 1 0 431283541 13557760 2842 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3310 2842 603 41 0 3269 0
vsize: 13240
[startup+100.002 s]
Raw data (loadavg): 0.90 0.88 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 5593 0 0 0 9981 19 0 0 25 0 1 0 431283541 14344192 3012 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3502 3012 603 41 0 3461 0
vsize: 14008
[startup+110.002 s]
Raw data (loadavg): 0.91 0.88 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 5745 0 0 0 10981 19 0 0 25 0 1 0 431283541 14864384 3164 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3629 3164 603 41 0 3588 0
vsize: 14516
[startup+120.002 s]
Raw data (loadavg): 0.93 0.89 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 5745 0 0 0 11981 19 0 0 25 0 1 0 431283541 14864384 3164 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3629 3164 603 41 0 3588 0
vsize: 14516
[startup+130.001 s]
Raw data (loadavg): 0.94 0.89 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6178 0 0 0 12980 20 0 0 25 0 1 0 431283541 16822272 3597 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4107 3597 603 41 0 4066 0
vsize: 16428
[startup+140.002 s]
Raw data (loadavg): 0.95 0.89 0.88 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6178 0 0 0 13980 20 0 0 25 0 1 0 431283541 16822272 3597 4294967295 134512640 134672761 3221224544 3221223508 1075347063 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.003 s]
Raw data (loadavg): 0.95 0.89 0.89 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6178 0 0 0 14981 20 0 0 25 0 1 0 431283541 16822272 3597 4294967295 134512640 134672761 3221224544 3221223728 134615830 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.003 s]
Raw data (loadavg): 0.96 0.90 0.89 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6179 0 0 0 15981 20 0 0 25 0 1 0 431283541 16822272 3598 4294967295 134512640 134672761 3221224544 3221223584 134614228 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.003 s]
Raw data (loadavg): 0.97 0.90 0.89 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6179 0 0 0 16981 20 0 0 25 0 1 0 431283541 16822272 3598 4294967295 134512640 134672761 3221224544 3221223728 134615632 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.003 s]
Raw data (loadavg): 0.97 0.90 0.89 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6179 0 0 0 17981 20 0 0 25 0 1 0 431283541 16822272 3598 4294967295 134512640 134672761 3221224544 3221223728 134615749 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.003 s]
Raw data (loadavg): 0.98 0.91 0.89 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6343 0 0 0 18981 20 0 0 25 0 1 0 431283541 17346560 3762 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.003 s]
Raw data (loadavg): 0.98 0.91 0.89 2/56 29959
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6343 0 0 0 19981 20 0 0 25 0 1 0 431283541 17346560 3762 4294967295 134512640 134672761 3221224544 3221223728 134615632 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.003 s]
Raw data (loadavg): 0.98 0.91 0.89 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6343 0 0 0 20981 20 0 0 25 0 1 0 431283541 17346560 3762 4294967295 134512640 134672761 3221224544 3221223728 134615652 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.002 s]
Raw data (loadavg): 0.98 0.91 0.89 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6534 0 0 0 21981 21 0 0 25 0 1 0 431283541 18128896 3953 4294967295 134512640 134672761 3221224544 3221223728 134615741 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.003 s]
Raw data (loadavg): 0.99 0.92 0.89 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6534 0 0 0 22981 21 0 0 25 0 1 0 431283541 18128896 3953 4294967295 134512640 134672761 3221224544 3221223728 134615749 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.002 s]
Raw data (loadavg): 0.99 0.92 0.89 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6534 0 0 0 23981 21 0 0 25 0 1 0 431283541 18128896 3953 4294967295 134512640 134672761 3221224544 3221223668 134566073 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.003 s]
Raw data (loadavg): 0.99 0.92 0.89 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6607 0 0 0 24981 21 0 0 25 0 1 0 431283541 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+260.002 s]
Raw data (loadavg): 0.99 0.92 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6607 0 0 0 25981 21 0 0 25 0 1 0 431283541 18391040 3991 4294967295 134512640 134672761 3221224544 3221223728 134615571 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.002 s]
Raw data (loadavg): 0.99 0.92 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6607 0 0 0 26981 21 0 0 25 0 1 0 431283541 18391040 3991 4294967295 134512640 134672761 3221224544 3221223584 134614330 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.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6642 0 0 0 27981 21 0 0 25 0 1 0 431283541 18391040 3991 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+290.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6642 0 0 0 28981 21 0 0 25 0 1 0 431283541 18391040 3991 4294967295 134512640 134672761 3221224544 3221223680 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+300.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6642 0 0 0 29982 21 0 0 25 0 1 0 431283541 18391040 3991 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+310.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6642 0 0 0 30981 22 0 0 25 0 1 0 431283541 18391040 3991 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4490 3991 603 41 0 4449 0
vsize: 17960
[startup+320.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6661 0 0 0 31981 22 0 0 25 0 1 0 431283541 18436096 4002 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4501 4002 603 41 0 4460 0
vsize: 18004
[startup+330.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6661 0 0 0 32982 22 0 0 25 0 1 0 431283541 18436096 4002 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4501 4002 603 41 0 4460 0
vsize: 18004
[startup+340.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6661 0 0 0 33982 22 0 0 25 0 1 0 431283541 18436096 4002 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4501 4002 603 41 0 4460 0
vsize: 18004
[startup+350.004 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 6789 0 0 0 34981 23 0 0 25 0 1 0 431283541 18960384 4130 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4629 4130 603 41 0 4588 0
vsize: 18516
[startup+360.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 7178 0 0 0 35980 24 0 0 25 0 1 0 431283541 20676608 4519 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5048 4519 603 41 0 5007 0
vsize: 20192
[startup+370.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 7495 0 0 0 36979 25 0 0 25 0 1 0 431283541 21794816 4828 4294967295 134512640 134672761 3221224544 3221223540 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5321 4828 603 41 0 5280 0
vsize: 21284
[startup+380.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 7495 0 0 0 37979 25 0 0 25 0 1 0 431283541 21794816 4828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5321 4828 603 41 0 5280 0
vsize: 21284
[startup+390.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 7495 0 0 0 38979 25 0 0 25 0 1 0 431283541 21794816 4828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5321 4828 603 41 0 5280 0
vsize: 21284
[startup+400.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 7495 0 0 0 39979 25 0 0 25 0 1 0 431283541 21794816 4828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5321 4828 603 41 0 5280 0
vsize: 21284
[startup+410.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 7495 0 0 0 40979 25 0 0 25 0 1 0 431283541 21794816 4828 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5321 4828 603 41 0 5280 0
vsize: 21284
[startup+420.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 7637 0 0 0 41979 26 0 0 25 0 1 0 431283541 22454272 4970 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5482 4970 603 41 0 5441 0
vsize: 21928
[startup+430.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 7943 0 0 0 42978 26 0 0 25 0 1 0 431283541 23642112 5276 4294967295 134512640 134672761 3221224544 3221223680 134614560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5772 5276 603 41 0 5731 0
vsize: 23088
[startup+440.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8242 0 0 0 43978 27 0 0 25 0 1 0 431283541 24965120 5575 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6095 5575 603 41 0 6054 0
vsize: 24380
[startup+450.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8377 0 0 0 44978 28 0 0 25 0 1 0 431283541 25387008 5702 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+460.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8377 0 0 0 45978 28 0 0 25 0 1 0 431283541 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+470.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8377 0 0 0 46978 28 0 0 25 0 1 0 431283541 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+480.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8377 0 0 0 47978 28 0 0 25 0 1 0 431283541 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+490.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8377 0 0 0 48978 28 0 0 25 0 1 0 431283541 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+500.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 29961
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8377 0 0 0 49978 29 0 0 25 0 1 0 431283541 25387008 5702 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6198 5702 603 41 0 6157 0
vsize: 24792
[startup+510.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8416 0 0 0 50977 29 0 0 25 0 1 0 431283541 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+520.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8416 0 0 0 51977 29 0 0 25 0 1 0 431283541 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+530.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8416 0 0 0 52978 29 0 0 25 0 1 0 431283541 25378816 5700 4294967295 134512640 134672761 3221224544 3221223712 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+540.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8416 0 0 0 53978 29 0 0 25 0 1 0 431283541 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+550.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8416 0 0 0 54978 29 0 0 25 0 1 0 431283541 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+560.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8454 0 0 0 55978 30 0 0 25 0 1 0 431283541 25378816 5700 4294967295 134512640 134672761 3221224544 3221223536 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+570.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8454 0 0 0 56978 30 0 0 25 0 1 0 431283541 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+580.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8454 0 0 0 57978 30 0 0 25 0 1 0 431283541 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+590.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8454 0 0 0 58978 30 0 0 25 0 1 0 431283541 25378816 5700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5700 603 41 0 6155 0
vsize: 24784
[startup+600.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8455 0 0 0 59978 30 0 0 25 0 1 0 431283541 25378816 5701 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6196 5701 603 41 0 6155 0
vsize: 24784
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8502 0 0 0 60978 30 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8502 0 0 0 61978 31 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8502 0 0 0 62978 31 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223584 134612777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8502 0 0 0 63978 31 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8502 0 0 0 64978 31 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8502 0 0 0 65978 31 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8544 0 0 0 66978 31 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8544 0 0 0 67978 31 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8544 0 0 0 68978 32 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8544 0 0 0 69978 32 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223376 1075349739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8544 0 0 0 70978 32 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8544 0 0 0 71978 32 0 0 25 0 1 0 431283541 25321472 5692 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5692 603 41 0 6141 0
vsize: 24728
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8787 0 0 0 72977 33 0 0 25 0 1 0 431283541 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8787 0 0 0 73977 33 0 0 25 0 1 0 431283541 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8787 0 0 0 74977 33 0 0 25 0 1 0 431283541 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8787 0 0 0 75977 33 0 0 25 0 1 0 431283541 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8787 0 0 0 76977 33 0 0 25 0 1 0 431283541 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8787 0 0 0 77977 33 0 0 25 0 1 0 431283541 26267648 5923 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8787 0 0 0 78977 33 0 0 25 0 1 0 431283541 26267648 5923 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6413 5923 603 41 0 6372 0
vsize: 25652
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29963
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 8962 0 0 0 79977 34 0 0 25 0 1 0 431283541 27058176 6098 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6606 6098 603 41 0 6565 0
vsize: 26424
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9161 0 0 0 80977 34 0 0 25 0 1 0 431283541 27754496 6285 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9161 0 0 0 81977 35 0 0 25 0 1 0 431283541 27754496 6285 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9161 0 0 0 82977 35 0 0 25 0 1 0 431283541 27754496 6285 4294967295 134512640 134672761 3221224544 3221223584 134612665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9161 0 0 0 83977 35 0 0 25 0 1 0 431283541 27754496 6285 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9161 0 0 0 84977 35 0 0 25 0 1 0 431283541 27754496 6285 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6776 6285 603 41 0 6735 0
vsize: 27104
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9162 0 0 0 85977 35 0 0 25 0 1 0 431283541 27754496 6286 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6776 6286 603 41 0 6735 0
vsize: 27104
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9162 0 0 0 86977 35 0 0 25 0 1 0 431283541 27754496 6286 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6776 6286 603 41 0 6735 0
vsize: 27104
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9530 0 0 0 87976 36 0 0 25 0 1 0 431283541 29331456 6654 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6654 603 41 0 7120 0
vsize: 28644
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9840 0 0 0 88976 37 0 0 25 0 1 0 431283541 30642176 6964 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7481 6964 603 41 0 7440 0
vsize: 29924
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9923 0 0 0 89976 37 0 0 25 0 1 0 431283541 30736384 7005 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7504 7005 603 41 0 7463 0
vsize: 30016
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9923 0 0 0 90976 37 0 0 25 0 1 0 431283541 30736384 7005 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7504 7005 603 41 0 7463 0
vsize: 30016
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9923 0 0 0 91976 37 0 0 25 0 1 0 431283541 30736384 7005 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7504 7005 603 41 0 7463 0
vsize: 30016
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9923 0 0 0 92976 37 0 0 25 0 1 0 431283541 30736384 7005 4294967295 134512640 134672761 3221224544 3221223728 134615579 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.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9924 0 0 0 93976 37 0 0 25 0 1 0 431283541 30736384 7006 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7504 7006 603 41 0 7463 0
vsize: 30016
[startup+950.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9986 0 0 0 94976 37 0 0 25 0 1 0 431283541 30818304 7026 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7524 7026 603 41 0 7483 0
vsize: 30096
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9986 0 0 0 95977 37 0 0 25 0 1 0 431283541 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+970.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9986 0 0 0 96977 37 0 0 25 0 1 0 431283541 30818304 7026 4294967295 134512640 134672761 3221224544 3221223728 134615660 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9986 0 0 0 97977 37 0 0 25 0 1 0 431283541 30818304 7026 4294967295 134512640 134672761 3221224544 3221223728 134615773 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 9986 0 0 0 98977 37 0 0 25 0 1 0 431283541 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): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10036 0 0 0 99977 37 0 0 25 0 1 0 431283541 31080448 7076 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7588 7076 603 41 0 7547 0
vsize: 30352
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10039 0 0 0 100977 37 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10039 0 0 0 101977 37 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10039 0 0 0 102977 37 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10039 0 0 0 103977 38 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10039 0 0 0 104977 38 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10039 0 0 0 105977 38 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10085 0 0 0 106977 38 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7524 7033 603 41 0 7483 0
vsize: 30096
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10085 0 0 0 107977 38 0 0 25 0 1 0 431283541 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+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10085 0 0 0 108977 38 0 0 25 0 1 0 431283541 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+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29965
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10085 0 0 0 109978 38 0 0 25 0 1 0 431283541 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+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10085 0 0 0 110978 38 0 0 25 0 1 0 431283541 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10085 0 0 0 111978 38 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10085 0 0 0 112978 38 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615608 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10131 0 0 0 113978 38 0 0 25 0 1 0 431283541 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+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10131 0 0 0 114978 38 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10131 0 0 0 115978 38 0 0 25 0 1 0 431283541 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10131 0 0 0 116979 38 0 0 25 0 1 0 431283541 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+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10131 0 0 0 117979 38 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10131 0 0 0 118979 38 0 0 25 0 1 0 431283541 30818304 7033 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 29967
Raw data (stat): 29959 (minisat+) R 29958 12452 12451 0 -1 0 10177 0 0 0 119979 38 0 0 25 0 1 0 431283541 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 29967
Raw data (stat): 29959 (minisat+) Z 29958 12452 12451 0 -1 12 10178 0 0 0 119979 40 0 0 25 0 1 0 431283541 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.04
CPU time (s): 1200.2
CPU user time (s): 1199.8
CPU system time (s): 0.400939
CPU usage (%): 100.013
Max. virtual memory (Kb): 30352
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####