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-mod008.opb
MD5SUM	581d778a36086562107993896110e0a2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	307
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	22000
Number of bits of the biggest number in a constraint	15
Biggest sum of numbers in a constraint	1027256
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02084
Number of variables	319
Total number of constraints	325
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	319
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	231
Trace number 15050

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 02:43:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18627 boxname=wulflinc22 idbench=1433 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  581d778a36086562107993896110e0a2  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-mod008.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-mod008.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-mod008.opb
IDLAUNCH: 18627
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        807516 kB
Buffers:         21804 kB
Cached:         175236 kB
SwapCached:         24 kB
Active:          26024 kB
Inactive:       173712 kB
HighTotal:      131008 kB
HighFree:        54936 kB
LowTotal:       903652 kB
LowFree:        752580 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            21936 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:03:54 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 18627 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss
c ---[   8]---> Adder-cost: 2481   maxlim: 21999   bits: 16/15
c ---[   5]---> Adder-cost: 2052   maxlim: 4999   bits: 14/13
c ---[   4]---> Adder-cost: 2306   maxlim: 11999   bits: 15/14
c ---[   2]---> BDD-cost:  478
c ---[   1]---> BDD-cost: 2553
c ---[   0]---> Adder-cost: 1803   maxlim: 3999   bits: 13/12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   62010   221290 |   18602       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10281          
c   -- var.elim.:  2000/10281          
c   -- var.elim.:  3000/10281          
c   -- var.elim.:  4000/10281          
c   -- var.elim.:  5000/10281          
c   -- var.elim.:  6000/10281          
c   -- var.elim.:  7000/10281          
c   -- var.elim.:  8000/10281          
c   -- var.elim.:  9000/10281          
c   -- var.elim.:  10000/10281          
c   -- var.elim.:  10281/10281          
c   -- var.elim.:  1000/1496          
c   -- var.elim.:  1496/1496          
c   -- var.elim.:  439/439          
c   -- subsuming                       
c   -- var.elim.:  353/353          
c   -- var.elim.:  126/126          
c |         0 |   60992   316610 |      --       0       --      -- |     --   | -1018/95348
c |         0 |   60992   316610 |   24396       0        0     nan |  0.000 % |
c |       100 |   60992   316610 |   26836     100      355     3.5 |  0.295 % |
c |       251 |   60992   316610 |   29520     251      947     3.8 |  0.295 % |
c |       476 |   60992   316610 |   32472     476     2140     4.5 |  0.295 % |
c |       813 |   60992   316610 |   35719     813     5035     6.2 |  0.295 % |
c |      1319 |   60992   316610 |   39291    1319    23867    18.1 |  0.295 % |
c |      2078 |   60992   316610 |   43220    2078    34107    16.4 |  0.295 % |
c ==============================================================================
c (current CPU-time: 12.7521 s)
c ==============================================================================
c [1mFound solution: 1105[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:61663     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3012 |  209063   662548 |   62718    3012    87015    28.9 |  0.295 % |
c   -- subsuming                       
c   -- var.elim.:  1000/54320          
c   -- var.elim.:  2000/54320          
c   -- var.elim.:  3000/54320          
c   -- var.elim.:  4000/54320          
c   -- var.elim.:  5000/54320          
c   -- var.elim.:  6000/54320          
c   -- var.elim.:  7000/54320          
c   -- var.elim.:  8000/54320          
c   -- var.elim.:  9000/54320          
c   -- var.elim.:  10000/54320          
c   -- var.elim.:  11000/54320          
c   -- var.elim.:  12000/54320          
c   -- var.elim.:  13000/54320          
c   -- var.elim.:  14000/54320          
c   -- var.elim.:  15000/54320          
c   -- var.elim.:  16000/54320          
c   -- var.elim.:  17000/54320          
c   -- var.elim.:  18000/54320          
c   -- var.elim.:  19000/54320          
c   -- var.elim.:  20000/54320          
c   -- var.elim.:  21000/54320          
c   -- var.elim.:  22000/54320          
c   -- var.elim.:  23000/54320          
c   -- var.elim.:  24000/54320          
c   -- var.elim.:  25000/54320          
c   -- var.elim.:  26000/54320          
c   -- var.elim.:  27000/54320          
c   -- var.elim.:  28000/54320          
c   -- var.elim.:  29000/54320          
c   -- var.elim.:  30000/54320          
c   -- var.elim.:  31000/54320          
c   -- var.elim.:  32000/54320          
c   -- var.elim.:  33000/54320          
c   -- var.elim.:  34000/54320          
c   -- var.elim.:  35000/54320          
c   -- var.elim.:  36000/54320          
c   -- var.elim.:  37000/54320          
c   -- var.elim.:  38000/54320          
c   -- var.elim.:  39000/54320          
c   -- var.elim.:  40000/54320          
c   -- var.elim.:  41000/54320          
c   -- var.elim.:  42000/54320          
c   -- var.elim.:  43000/54320          
c   -- var.elim.:  44000/54320          
c   -- var.elim.:  45000/54320          
c   -- var.elim.:  46000/54320          
c   -- var.elim.:  47000/54320          
c   -- var.elim.:  48000/54320          
c   -- var.elim.:  49000/54320          
c   -- var.elim.:  50000/54320          
c   -- var.elim.:  51000/54320          
c   -- var.elim.:  52000/54320          
c   -- var.elim.:  53000/54320          
c   -- var.elim.:  54000/54320          
c   -- var.elim.:  54320/54320          
c   -- var.elim.:  1000/29120          
c   -- var.elim.:  2000/29120          
c   -- var.elim.:  3000/29120          
c   -- var.elim.:  4000/29120          
c   -- var.elim.:  5000/29120          
c   -- var.elim.:  6000/29120          
c   -- var.elim.:  7000/29120          
c   -- var.elim.:  8000/29120          
c   -- var.elim.:  9000/29120          
c   -- var.elim.:  10000/29120          
c   -- var.elim.:  11000/29120          
c   -- var.elim.:  12000/29120          
c   -- var.elim.:  13000/29120          
c   -- var.elim.:  14000/29120          
c   -- var.elim.:  15000/29120          
c   -- var.elim.:  16000/29120          
c   -- var.elim.:  17000/29120          
c   -- var.elim.:  18000/29120          
c   -- var.elim.:  19000/29120          
c   -- var.elim.:  20000/29120          
c   -- var.elim.:  21000/29120          
c   -- var.elim.:  22000/29120          
c   -- var.elim.:  23000/29120          
c   -- var.elim.:  24000/29120          
c   -- var.elim.:  25000/29120          
c   -- var.elim.:  26000/29120          
c   -- var.elim.:  27000/29120          
c   -- var.elim.:  28000/29120          
c   -- var.elim.:  29000/29120          
c   -- var.elim.:  29120/29120          
c   -- var.elim.:  360/360          
c   -- subsuming                       
c   -- var.elim.:  1000/4845          
c   -- var.elim.:  2000/4845          
c   -- var.elim.:  3000/4845          
c   -- var.elim.:  4000/4845          
c   -- var.elim.:  4845/4845          
c   -- var.elim.:  220/220          
c   -- subsuming                       
c   -- var.elim.:  79/79          
c   -- var.elim.:  7/7          
c |      3012 |  192716   748536 |      --    3012       --      -- |     --   | -16347/85989
c |      3012 |  192716   748536 |   77086    3012    87015    28.9 |  0.295 % |
c |      3114 |  192716   748536 |   84795    3114    89430    28.7 |  0.076 % |
c |      3264 |  192716   748536 |   93274    3264    91158    27.9 |  0.076 % |
c |      3490 |  192716   748536 |  102601    3490    94966    27.2 |  0.076 % |
c |      3827 |  192716   748536 |  112862    3827    96903    25.3 |  0.076 % |
c ==============================================================================
c (current CPU-time: 31.8422 s)
c ==============================================================================
c [1mFound solution: 1095[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4103 |  193698   751029 |   58109    4103   105975    25.8 |  0.076 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1271          
c   -- var.elim.:  1271/1271          
c   -- var.elim.:  695/695          
c   -- subsuming                       
c   -- var.elim.:  176/176          
c |      4103 |  193168   750853 |      --    4103       --      -- |     --   | -530/-175
c |      4103 |  193168   750853 |   77267    4103   105975    25.8 |  0.076 % |
c |      4203 |  193168   750853 |   84993    4203   136619    32.5 |  0.078 % |
c |      4355 |  193168   750853 |   93493    4355   151099    34.7 |  0.078 % |
c ==============================================================================
c (current CPU-time: 35.4416 s)
c ==============================================================================
c [1mFound solution: 1006[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4384 |  196149   758423 |   58844    4384   158080    36.1 |  0.078 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3831          
c   -- var.elim.:  2000/3831          
c   -- var.elim.:  3000/3831          
c   -- var.elim.:  3831/3831          
c   -- var.elim.:  1000/1972          
c   -- var.elim.:  1972/1972          
c   -- subsuming                       
c   -- var.elim.:  89/89          
c |      4384 |  194639   758454 |      --    4384       --      -- |     --   | -1510/32
c |      4384 |  194639   758454 |   77855    4384   158080    36.1 |  0.078 % |
c |      4484 |  194639   758454 |   85641    4484   159394    35.5 |  0.080 % |
c |      4634 |  194639   758454 |   94205    4634   162548    35.1 |  0.080 % |
c ==============================================================================
c (current CPU-time: 38.7191 s)
c ==============================================================================
c [1mFound solution: 765[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4696 |  194802   759075 |   58440    4696   171127    36.4 |  0.080 % |
c   -- subsuming                       
c   -- var.elim.:  440/440          
c   -- var.elim.:  324/324          
c |      4696 |  194691   759111 |      --    4696       --      -- |     --   | -111/37
c |      4696 |  194691   759111 |   77876    4696   171127    36.4 |  0.080 % |
c |      4796 |  194691   759111 |   85664    4796   173192    36.1 |  0.083 % |
c |      4946 |  194691   759111 |   94230    4946   174889    35.4 |  0.083 % |
c |      5174 |  194691   759111 |  103653    5174   180379    34.9 |  0.083 % |
c |      5512 |  194691   759111 |  114018    5512   207829    37.7 |  0.083 % |
c ==============================================================================
c (current CPU-time: 48.5896 s)
c ==============================================================================
c [1mFound solution: 713[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5839 |  196578   764111 |   58973    5839   254144    43.5 |  0.083 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2696          
c   -- var.elim.:  2000/2696          
c   -- var.elim.:  2696/2696          
c   -- var.elim.:  1000/1422          
c   -- var.elim.:  1422/1422          
c   -- subsuming                       
c   -- var.elim.:  94/94          
c |      5839 |  195617   765564 |      --    5839       --      -- |     --   | -961/1454
c |      5839 |  195617   765564 |   78246    5839   254144    43.5 |  0.083 % |
c ==============================================================================
c (current CPU-time: 50.9683 s)
c ==============================================================================
c [1mFound solution: 681[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5903 |  195689   766175 |   58706    5903   261402    44.3 |  0.083 % |
c   -- subsuming                       
c   -- var.elim.:  537/537          
c   -- var.elim.:  487/487          
c |      5903 |  195643   766688 |      --    5903       --      -- |     --   | -46/514
c |      5903 |  195643   766688 |   78257    5903   261402    44.3 |  0.083 % |
c |      6003 |  195643   766688 |   86082    6003   266889    44.5 |  0.087 % |
c ==============================================================================
c (current CPU-time: 54.1448 s)
c ==============================================================================
c [1mFound solution: 660[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6042 |  195674   767173 |   58702    6042   269203    44.6 |  0.087 % |
c   -- subsuming                       
c   -- var.elim.:  454/454          
c   -- var.elim.:  434/434          
c |      6042 |  195654   767333 |      --    6042       --      -- |     --   | -20/161
c |      6042 |  195654   767333 |   78261    6042   269203    44.6 |  0.087 % |
c |      6143 |  195654   767333 |   86087    6143   275026    44.8 |  0.090 % |
c ==============================================================================
c (current CPU-time: 56.4564 s)
c ==============================================================================
c [1mFound solution: 597[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6191 |  197231   771681 |   59169    6191   277209    44.8 |  0.090 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2497          
c   -- var.elim.:  2000/2497          
c   -- var.elim.:  2497/2497          
c   -- var.elim.:  1000/1384          
c   -- var.elim.:  1384/1384          
c   -- subsuming                       
c   -- var.elim.:  107/107          
c |      6191 |  196377   772024 |      --    6191       --      -- |     --   | -854/344
c |      6191 |  196377   772024 |   78550    6191   277209    44.8 |  0.090 % |
c |      6293 |  196377   772024 |   86405    6293   281581    44.7 |  0.092 % |
c |      6443 |  196377   772024 |   95046    6443   289108    44.9 |  0.092 % |
c |      6668 |  196377   772024 |  104551    6668   292647    43.9 |  0.092 % |
c ==============================================================================
c (current CPU-time: 61.3487 s)
c ==============================================================================
c [1mFound solution: 587[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6676 |  196414   772539 |   58924    6676   292897    43.9 |  0.092 % |
c   -- subsuming                       
c   -- var.elim.:  476/476          
c   -- var.elim.:  452/452          
c |      6676 |  196396   774457 |      --    6676       --      -- |     --   | -18/1919
c |      6676 |  196396   774457 |   78558    6676   292897    43.9 |  0.092 % |
c ==============================================================================
c (current CPU-time: 62.9584 s)
c ==============================================================================
c [1mFound solution: 585[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6717 |  196422   774713 |   58926    6717   294748    43.9 |  0.092 % |
c   -- subsuming                       
c   -- var.elim.:  229/229          
c   -- var.elim.:  211/211          
c |      6717 |  196404   774872 |      --    6717       --      -- |     --   | -18/160
c |      6717 |  196404   774872 |   78561    6717   294748    43.9 |  0.092 % |
c |      6821 |  196404   774872 |   86417    6821   300621    44.1 |  0.097 % |
c ==============================================================================
c (current CPU-time: 65.2721 s)
c ==============================================================================
c [1mFound solution: 516[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6850 |  196507   775570 |   58952    6850   301545    44.0 |  0.097 % |
c   -- subsuming                       
c   -- var.elim.:  592/592          
c   -- var.elim.:  514/514          
c |      6850 |  196431   775743 |      --    6850       --      -- |     --   | -76/174
c |      6850 |  196431   775743 |   78572    6850   301545    44.0 |  0.097 % |
c |      6950 |  196431   775743 |   86429    6950   318170    45.8 |  0.100 % |
c |      7100 |  196431   775743 |   95072    7100   330479    46.5 |  0.100 % |
c |      7327 |  196431   775743 |  104579    7327   337614    46.1 |  0.100 % |
c |      7665 |  196431   775743 |  115037    7665   341695    44.6 |  0.100 % |
c |      8171 |  196431   775743 |  126541    8171   380840    46.6 |  0.100 % |
c |      8930 |  196326   775322 |  139121    8880   411669    46.4 |  0.128 % |
c |     10069 |  196326   775322 |  153033   10019   499575    49.9 |  0.128 % |
c |     11781 |  196326   775322 |  168336   11731   802332    68.4 |  0.128 % |
c |     14344 |  196326   775322 |  185170   14294  1061850    74.3 |  0.128 % |
c ==============================================================================
c (current CPU-time: 124.422 s)
c ==============================================================================
c [1mFound solution: 514[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15042 |  197490   776183 |   59246   14958  1293993    86.5 |  0.128 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3480          
c   -- var.elim.:  2000/3480          
c   -- var.elim.:  3000/3480          
c   -- var.elim.:  3480/3480          
c   -- var.elim.:  1000/2637          
c   -- var.elim.:  2000/2637          
c   -- var.elim.:  2637/2637          
c   -- var.elim.:  1000/1016          
c   -- var.elim.:  1016/1016          
c   -- var.elim.:  8/8          
c   -- subsuming                       
c   -- var.elim.:  660/660          
c   -- var.elim.:  104/104          
c |     15042 |  196304   776819 |      --   14958       --      -- |     --   | -1186/637
c |     15042 |  196304   776819 |   78521   13535   760526    56.2 |  0.128 % |
c |     15142 |  196304   776819 |   86373   13635   792624    58.1 |  0.296 % |
c |     15293 |  196304   776819 |   95011   13786   804114    58.3 |  0.296 % |
c |     15518 |  196304   776819 |  104512   14011   812067    58.0 |  0.296 % |
c ==============================================================================
c (current CPU-time: 136.368 s)
c ==============================================================================
c [1mFound solution: 420[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15672 |  196331   776969 |   58899   14165   860242    60.7 |  0.296 % |
c   -- subsuming                       
c   -- var.elim.:  360/360          
c   -- var.elim.:  104/104          
c |     15672 |  196316   777006 |      --   14165       --      -- |     --   | -15/38
c |     15672 |  196316   777006 |   78526   14165   860242    60.7 |  0.296 % |
c |     15772 |  196316   777006 |   86379   14265   880185    61.7 |  0.298 % |
c |     15922 |  196316   777006 |   95016   14415   965570    67.0 |  0.298 % |
c |     16147 |  196316   777006 |  104518   14640  1022726    69.9 |  0.298 % |
c |     16484 |  196316   777006 |  114970   14977  1040760    69.5 |  0.298 % |
c |     16990 |  196316   777006 |  126467   15483  1063959    68.7 |  0.298 % |
c |     17749 |  196316   777006 |  139114   16242  1283070    79.0 |  0.298 % |
c |     18892 |  196316   777006 |  153025   17385  1481766    85.2 |  0.298 % |
c |     20601 |  196316   777006 |  168328   19094  2233636   117.0 |  0.298 % |
c |     23164 |  196273   776097 |  185120   21656  3142018   145.1 |  0.311 % |
c |     27011 |  196273   776097 |  203632   25503  5410672   212.2 |  0.311 % |
c ==============================================================================
c (current CPU-time: 263.592 s)
c ==============================================================================
c [1mFound solution: 410[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     29694 |  196312   776516 |   58893   28186  8632800   306.3 |  0.311 % |
c   -- subsuming                       
c   -- var.elim.:  414/414          
c   -- var.elim.:  375/375          
c   -- var.elim.:  96/96          
c   -- var.elim.:  245/245          
c   -- var.elim.:  243/243          
c |     29694 |  196277   776935 |      --   28186       --      -- |     --   | -35/420
c |     29694 |  196277   776935 |   78510   28147  8617851   306.2 |  0.311 % |
c |     29794 |  196249   776844 |   86349   28246  8657110   306.5 |  0.324 % |
c |     29949 |  196249   776844 |   94984   28401  8675500   305.5 |  0.324 % |
c |     30178 |  196249   776844 |  104482   28630  8866741   309.7 |  0.324 % |
c |     30516 |  196249   776844 |  114931   28968  9134667   315.3 |  0.324 % |
c |     31024 |  196249   776844 |  126424   29476  9399348   318.9 |  0.324 % |
c |     31785 |  196249   776844 |  139066   30237  9685768   320.3 |  0.324 % |
c |     32924 |  196249   776844 |  152973   31376  9903480   315.6 |  0.324 % |
c ==============================================================================
c (current CPU-time: 307.124 s)
c ==============================================================================
c [1mFound solution: 408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     32967 |  196301   777397 |   58890   31419  9917514   315.7 |  0.324 % |
c   -- subsuming                       
c   -- var.elim.:  523/523          
c   -- var.elim.:  671/671          
c   -- var.elim.:  100/100          
c |     32967 |  196264   778749 |      --   31419       --      -- |     --   | -37/1353
c |     32967 |  196264   778749 |   78505   31220  9660353   309.4 |  0.324 % |
c |     33068 |  196236   778480 |   86343   31320  9665167   308.6 |  0.331 % |
c |     33220 |  195988   777437 |   94858   31469  9702748   308.3 |  0.403 % |
c |     33445 |  195988   777437 |  104344   31694  9831700   310.2 |  0.403 % |
c |     33784 |  195988   777437 |  114778   32033  9969196   311.2 |  0.403 % |
c |     34290 |  195988   777437 |  126256   32539 10133308   311.4 |  0.403 % |
c |     35049 |  195988   777437 |  138881   33298 10324131   310.1 |  0.403 % |
c |     36189 |  195988   777437 |  152770   34438 11424346   331.7 |  0.403 % |
c |     37899 |  195903   776618 |  167974   36067 11748862   325.8 |  0.431 % |
c |     40461 |  195442   774918 |  184336   38623 13204174   341.9 |  0.607 % |
c |     44305 |  195442   774918 |  202770   42467 14934158   351.7 |  0.607 % |
c ==============================================================================
c (current CPU-time: 454.342 s)
c ==============================================================================
c [1mFound solution: 402[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     47582 |  195496   775462 |   58648   45744 16389694   358.3 |  0.607 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1485          
c   -- var.elim.:  1485/1485          
c   -- var.elim.:  1000/1298          
c   -- var.elim.:  1298/1298          
c   -- var.elim.:  556/556          
c   -- var.elim.:  520/520          
c   -- subsuming                       
c   -- var.elim.:  385/385          
c |     47582 |  195309   775619 |      --   45744       --      -- |     --   | -186/160
c |     47582 |  195309   775619 |   78123   41751  9118465   218.4 |  0.607 % |
c |     47682 |  195309   775619 |   85935   41851  9126223   218.1 |  0.613 % |
c |     47834 |  195309   775619 |   94529   42003  9148063   217.8 |  0.613 % |
c |     48059 |  195309   775619 |  103982   42228  9183561   217.5 |  0.613 % |
c |     48399 |  195309   775619 |  114380   42568  9211535   216.4 |  0.613 % |
c |     48905 |  195253   775414 |  125782   43069  9316897   216.3 |  0.631 % |
c |     49664 |  195253   775414 |  138361   43828  9619138   219.5 |  0.631 % |
c |     50803 |  195253   775414 |  152197   44967  9858600   219.2 |  0.631 % |
c |     52512 |  195253   775414 |  167416   46676 10659905   228.4 |  0.631 % |
c |     55075 |  195253   775414 |  184158   49239 11691172   237.4 |  0.631 % |
c |     58919 |  195253   775414 |  202574   53083 14333607   270.0 |  0.631 % |
c |     64688 |  195253   775414 |  222831   58852 17848391   303.3 |  0.631 % |
c |     73337 |  195253   775414 |  245115   67501 23656798   350.5 |  0.631 % |
c ==============================================================================
c (current CPU-time: 700.514 s)
c ==============================================================================
c [1mFound solution: 379[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     74770 |  195295   775929 |   58588   68934 24450824   354.7 |  0.631 % |
c   -- subsuming                       
c   -- var.elim.:  520/520          
c   -- var.elim.:  590/590          
c   -- var.elim.:  10/10          
c   -- var.elim.:  189/189          
c |     74770 |  195263   776785 |      --   68934       --      -- |     --   | -31/859
c |     74770 |  195263   776785 |   78105   66547 19523863   293.4 |  0.631 % |
c |     74873 |  195263   776785 |   85915   66650 19556670   293.4 |  0.636 % |
c |     75025 |  195263   776785 |   94507   66802 19564303   292.9 |  0.636 % |
c |     75252 |  194842   775176 |  103733   66926 19619437   293.2 |  0.771 % |
c |     75590 |  194842   775176 |  114107   67264 19891273   295.7 |  0.771 % |
c |     76096 |  194774   774917 |  125474   67762 20166212   297.6 |  0.792 % |
c ==============================================================================
c (current CPU-time: 736.597 s)
c ==============================================================================
c [1mFound solution: 373[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     76583 |  194691   775034 |   58407   68240 20303122   297.5 |  0.792 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1303          
c   -- var.elim.:  1303/1303          
c   -- var.elim.:  1000/1122          
c   -- var.elim.:  1122/1122          
c   -- var.elim.:  38/38          
c   -- var.elim.:  424/424          
c   -- subsuming                       
c   -- var.elim.:  5/5          
c |     76583 |  194579   777089 |      --   68240       --      -- |     --   | -111/2058
c |     76583 |  194579   777089 |   77831   68240 20303122   297.5 |  0.792 % |
c |     76684 |  194579   777089 |   85614   68341 20330740   297.5 |  0.831 % |
c |     76834 |  194579   777089 |   94176   68491 20346638   297.1 |  0.831 % |
c |     77060 |  194579   777089 |  103593   68717 20483818   298.1 |  0.831 % |
c |     77397 |  194579   777089 |  113953   69054 20874094   302.3 |  0.831 % |
c |     77905 |  194579   777089 |  125348   69562 21170964   304.3 |  0.831 % |
c |     78665 |  194579   777089 |  137883   70322 21509979   305.9 |  0.831 % |
c |     79807 |  194500   776800 |  151610   65631 15689001   239.0 |  0.854 % |
c |     81516 |  194500   776800 |  166771   67340 17337378   257.5 |  0.854 % |
c |     84081 |  194500   776800 |  183448   69905 20384369   291.6 |  0.854 % |
c |     87925 |  194459   776667 |  201750   73746 23074864   312.9 |  0.870 % |
c |     93693 |  194459   776667 |  221925   79514 28020258   352.4 |  0.870 % |
c |    102348 |  194104   775426 |  243672   88088 36309002   412.2 |  0.998 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C2_0x2e__bit0 -C3_0x2e__bit0 -C4_0x2e__bit0 -C5_0x2e__bit0 -C6_0x2e__bit0 -C7_0x2e__bit0 -C8_0x2e__bit0 -C9_0x2e__bit0 -C10_0x2e__bit0 -C11_0x2e__bit0 -C12_0x2e__bit0 -C13_0x2e__bit0 -C14_0x2e__bit0 -C15_0x2e__bit0 -C16_0x2e__bit0 -C17_0x2e__bit0 -C18_0x2e__bit0 -C19_0x2e__bit0 -C20_0x2e__bit0 -C21_0x2e__bit0 -C22_0x2e__bit0 -C23_0x2e__bit0 -C24_0x2e__bit0 -C25_0x2e__bit0 -C26_0x2e__bit0 -C27_0x2e__bit0 -C28_0x2e__bit0 -C29_0x2e__bit0 -C30_0x2e__bit0 -C31_0x2e__bit0 -C32_0x2e__bit0 -C33_0x2e__bit0 -C34_0x2e__bit0 -C35_0x2e__bit0 -C36_0x2e__bit0 -C37_0x2e__bit0 -C38_0x2e__bit0 -C39_0x2e__bit0 -C40_0x2e__bit0 -C41_0x2e__bit0 -C42_0x2e__bit0 -C43_0x2e__bit0 -C44_0x2e__bit0 -C45_0x2e__bit0 -C46_0x2e__bit0 -C47_0x2e__bit0 -C48_0x2e__bit0 -C49_0x2e__bit0 -C50_0x2e__bit0 -C51_0x2e__bit0 -C52_0x2e__bit0 -C53_0x2e__bit0 -C54_0x2e__bit0 -C55_0x2e__bit0 -C56_0x2e__bit0 -C57_0x2e__bit0 -C58_0x2e__bit0 -C59_0x2e__bit0 -C60_0x2e__bit0 -C61_0x2e__bit0 -C62_0x2e__bit0 -C63_0x2e__bit0 -C64_0x2e__bit0 -C65_0x2e__bit0 -C66_0x2e__bit0 -C67_0x2e__bit0 -C68_0x2e__bit0 -C69_0x2e__bit0 -C70_0x2e__bit0 -C71_0x2e__bit0 -C72_0x2e__bit0 -C73_0x2e__bit0 -C74_0x2e__bit0 -C75_0x2e__bit0 -C76_0x2e__bit0 -C77_0x2e__bit0 -C78_0x2e__bit0 -C79_0x2e__bit0 -C80_0x2e__bit0 -C81_0x2e__bit0 -C82_0x2e__bit0 C83_0x2e__bit0 -C84_0x2e__bit0 -C85_0x2e__bit0 C86_0x2e__bit0 -C87_0x2e__bit0 -C88_0x2e__bit0 -C89_0x2e__bit0 -C90_0x2e__bit0 -C91_0x2e__bit0 -C92_0x2e__bit0 -C93_0x2e__bit0 -C94_0x2e__bit0 -C95_0x2e__bit0 -C96_0x2e__bit0 -C97_0x2e__bit0 -C98_0x2e__bit0 -C99_0x2e__bit0 -C100_0x2e__bit0 -C101_0x2e__bit0 -C102_0x2e__bit0 -C103_0x2e__bit0 -C104_0x2e__bit0 -C105_0x2e__bit0 -C106_0x2e__bit0 -C107_0x2e__bit0 -C108_0x2e__bit0 -C109_0x2e__bit0 -C110_0x2e__bit0 -C111_0x2e__bit0 -C112_0x2e__bit0 -C113_0x2e__bit0 -C114_0x2e__bit0 -C115_0x2e__bit0 -C116_0x2e__bit0 -C117_0x2e__bit0 -C118_0x2e__bit0 -C119_0x2e__bit0 -C120_0x2e__bit0 -C121_0x2e__bit0 C122_0x2e__bit0 -C123_0x2e__bit0 -C124_0x2e__bit0 -C125_0x2e__bit0 -C126_0x2e__bit0 -C127_0x2e__bit0 -C128_0x2e__bit0 -C129_0x2e__bit0 C130_0x2e__bit0 -C131_0x2e__bit0 -C132_0x2e__bit0 -C133_0x2e__bit0 -C134_0x2e__bit0 -C135_0x2e__bit0 -C136_0x2e__bit0 -C137_0x2e__bit0 -C138_0x2e__bit0 C139_0x2e__bit0 -C140_0x2e__bit0 -C141_0x2e__bit0 -C142_0x2e__bit0 -C143_0x2e__bit0 -C144_0x2e__bit0 -C145_0x2e__bit0 -C146_0x2e__bit0 -C147_0x2e__bit0 -C148_0x2e__bit0 -C149_0x2e__bit0 -C150_0x2e__bit0 -C151_0x2e__bit0 -C152_0x2e__bit0 -C153_0x2e__bit0 -C154_0x2e__bit0 -C155_0x2e__bit0 -C156_0x2e__bit0 -C157_0x2e__bit0 -C158_0x2e__bit0 -C159_0x2e__bit0 -C160_0x2e__bit0 -C161_0x2e__bit0 -C162_0x2e__bit0 -C163_0x2e__bit0 -C164_0x2e__bit0 -C165_0x2e__bit0 -C166_0x2e__bit0 -C167_0x2e__bit0 -C168_0x2e__bit0 -C169_0x2e__bit0 -C170_0x2e__bit0 -C171_0x2e__bit0 -C172#### 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.85 0.95 0.93 2/54 26376
Raw data (stat): 26376 (runsolver) R 26375 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541571483 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0004 s]
Raw data (loadavg): 0.87 0.95 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 6762 0 0 0 980 18 0 0 25 0 1 0 541571483 15093760 3008 4294967295 134512640 134672761 3221224544 3221223184 134622209 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3685 3008 603 41 0 3644 0
vsize: 14740
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 14781 0 0 0 1951 46 0 0 25 0 1 0 541571483 46018560 10352 4294967295 134512640 134672761 3221224544 3221222704 134566695 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11235 10352 603 41 0 11194 0
vsize: 44940
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 15462 0 0 0 2946 51 0 0 25 0 1 0 541571483 45670400 10318 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11150 10318 603 41 0 11109 0
vsize: 44600
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 22938 0 0 0 3920 77 0 0 25 0 1 0 541571483 66334720 12564 4294967295 134512640 134672761 3221224544 3221222924 1075326251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16195 12564 603 41 0 16154 0
vsize: 64780
[startup+50.003 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 25415 0 0 0 4908 88 0 0 25 0 1 0 541571483 66473984 12585 4294967295 134512640 134672761 3221224544 3221223020 1075278784 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16229 12585 603 41 0 16188 0
vsize: 64916
[startup+60.0028 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 34696 0 0 0 5874 123 0 0 25 0 1 0 541571483 52817920 10768 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12895 10768 603 41 0 12854 0
vsize: 51580
[startup+70.0039 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 42676 0 0 0 6845 152 0 0 25 0 1 0 541571483 53178368 10859 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12983 10859 603 41 0 12942 0
vsize: 51932
[startup+80.0042 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 42677 0 0 0 7845 152 0 0 25 0 1 0 541571483 53178368 10860 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12983 10860 603 41 0 12942 0
vsize: 51932
[startup+90.005 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 42723 0 0 0 8845 152 0 0 25 0 1 0 541571483 53444608 10906 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13048 10906 603 41 0 13007 0
vsize: 52192
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 42828 0 0 0 9845 153 0 0 25 0 1 0 541571483 53841920 11011 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13145 11011 603 41 0 13104 0
vsize: 52580
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 43172 0 0 0 10843 154 0 0 25 0 1 0 541571483 55259136 11355 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13491 11355 603 41 0 13450 0
vsize: 53964
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 43386 0 0 0 11842 156 0 0 25 0 1 0 541571483 56180736 11569 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 11569 603 41 0 13675 0
vsize: 54864
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 46865 0 0 0 12830 168 0 0 25 0 1 0 541571483 57204736 11842 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13966 11842 603 41 0 13925 0
vsize: 55864
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 49420 0 0 0 13819 179 0 0 25 0 1 0 541571483 57225216 11872 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13971 11872 603 41 0 13930 0
vsize: 55884
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 49420 0 0 0 14819 179 0 0 25 0 1 0 541571483 57225216 11872 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13971 11872 603 41 0 13930 0
vsize: 55884
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 49420 0 0 0 15819 180 0 0 25 0 1 0 541571483 57225216 11872 4294967295 134512640 134672761 3221224544 3221223696 134614481 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13971 11872 603 41 0 13930 0
vsize: 55884
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 49589 0 0 0 16818 180 0 0 25 0 1 0 541571483 58015744 12041 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 12041 603 41 0 14123 0
vsize: 56656
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 49787 0 0 0 17818 181 0 0 25 0 1 0 541571483 58789888 12239 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14353 12239 603 41 0 14312 0
vsize: 57412
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 50222 0 0 0 18816 183 0 0 25 0 1 0 541571483 60600320 12674 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14795 12674 603 41 0 14754 0
vsize: 59180
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 50807 0 0 0 19814 184 0 0 25 0 1 0 541571483 62951424 13259 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15369 13259 603 41 0 15328 0
vsize: 61476
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 51440 0 0 0 20813 186 0 0 25 0 1 0 541571483 65572864 13892 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16009 13892 603 41 0 15968 0
vsize: 64036
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 51950 0 0 0 21812 187 0 0 25 0 1 0 541571483 67657728 14402 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16518 14402 603 41 0 16477 0
vsize: 66072
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 52989 0 0 0 22809 190 0 0 25 0 1 0 541571483 71921664 15441 4294967295 134512640 134672761 3221224544 3221223556 134565154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17559 15441 603 41 0 17518 0
vsize: 70236
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 53594 0 0 0 23807 192 0 0 25 0 1 0 541571483 74444800 16046 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18175 16046 603 41 0 18134 0
vsize: 72700
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 54601 0 0 0 24805 194 0 0 25 0 1 0 541571483 78512128 17053 4294967295 134512640 134672761 3221224544 3221223584 134612608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19168 17053 603 41 0 19127 0
vsize: 76672
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 56146 0 0 0 25801 198 0 0 25 0 1 0 541571483 84828160 18598 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20710 18598 603 41 0 20669 0
vsize: 82840
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 59596 0 0 0 26792 208 0 0 25 0 1 0 541571483 87326720 19230 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21320 19230 603 41 0 21279 0
vsize: 85280
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 59817 0 0 0 27791 209 0 0 25 0 1 0 541571483 88236032 19451 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21542 19451 603 41 0 21501 0
vsize: 86168
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 60470 0 0 0 28790 211 0 0 25 0 1 0 541571483 90947584 20104 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22204 20104 603 41 0 22163 0
vsize: 88816
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 60682 0 0 0 29789 211 0 0 25 0 1 0 541571483 91852800 20316 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22425 20316 603 41 0 22384 0
vsize: 89700
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 63230 0 0 0 30779 221 0 0 25 0 1 0 541571483 103542784 22235 4294967295 134512640 134672761 3221224544 3221222912 134553654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25279 22235 603 41 0 25238 0
vsize: 101116
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 63745 0 0 0 31777 224 0 0 25 0 1 0 541571483 92950528 20586 4294967295 134512640 134672761 3221224544 3221223620 1074733027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22693 20586 603 41 0 22652 0
vsize: 90772
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 63996 0 0 0 32777 224 0 0 25 0 1 0 541571483 94126080 20837 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22980 20837 603 41 0 22939 0
vsize: 91920
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 64388 0 0 0 33776 225 0 0 25 0 1 0 541571483 95694848 21229 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23363 21229 603 41 0 23322 0
vsize: 93452
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 65068 0 0 0 34775 226 0 0 25 0 1 0 541571483 98541568 21909 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24058 21909 603 41 0 24017 0
vsize: 96232
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 65301 0 0 0 35774 227 0 0 25 0 1 0 541571483 99450880 22142 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24280 22142 603 41 0 24239 0
vsize: 97120
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 65506 0 0 0 36774 227 0 0 25 0 1 0 541571483 100233216 22347 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24471 22347 603 41 0 24430 0
vsize: 97884
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 66050 0 0 0 37773 228 0 0 25 0 1 0 541571483 102469632 22891 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25017 22891 603 41 0 24976 0
vsize: 100068
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 67004 0 0 0 38771 231 0 0 25 0 1 0 541571483 106352640 23845 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25965 23845 603 41 0 25924 0
vsize: 103860
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 67372 0 0 0 39769 232 0 0 25 0 1 0 541571483 107954176 24213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26356 24213 603 41 0 26315 0
vsize: 105424
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 68007 0 0 0 40767 235 0 0 25 0 1 0 541571483 110460928 24848 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26968 24848 603 41 0 26927 0
vsize: 107872
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 68729 0 0 0 41766 236 0 0 25 0 1 0 541571483 113414144 25570 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27689 25570 603 41 0 27648 0
vsize: 110756
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 69041 0 0 0 42765 237 0 0 25 0 1 0 541571483 114712576 25882 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28006 25882 603 41 0 27965 0
vsize: 112024
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 69710 0 0 0 43764 238 0 0 25 0 1 0 541571483 117485568 26551 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28683 26551 603 41 0 28642 0
vsize: 114732
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 70043 0 0 0 44763 239 0 0 25 0 1 0 541571483 118800384 26884 4294967295 134512640 134672761 3221224544 3221223744 134610711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29004 26884 603 41 0 28963 0
vsize: 116016
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73563 0 0 0 45752 251 0 0 25 0 1 0 541571483 119689216 27112 4294967295 134512640 134672761 3221224544 3221223800 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+470.013 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73563 0 0 0 46752 251 0 0 25 0 1 0 541571483 119689216 27112 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+480.013 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73563 0 0 0 47752 251 0 0 25 0 1 0 541571483 119689216 27112 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+490.013 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73563 0 0 0 48752 251 0 0 25 0 1 0 541571483 119689216 27112 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+500.013 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73563 0 0 0 49752 251 0 0 25 0 1 0 541571483 119689216 27112 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+510.013 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73565 0 0 0 50752 251 0 0 25 0 1 0 541571483 119689216 27114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27114 603 41 0 29180 0
vsize: 116884
[startup+520.013 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73567 0 0 0 51753 251 0 0 25 0 1 0 541571483 119689216 27116 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27116 603 41 0 29180 0
vsize: 116884
[startup+530.014 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73567 0 0 0 52753 251 0 0 25 0 1 0 541571483 119689216 27116 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27116 603 41 0 29180 0
vsize: 116884
[startup+540.013 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73568 0 0 0 53753 251 0 0 25 0 1 0 541571483 119689216 27117 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27117 603 41 0 29180 0
vsize: 116884
[startup+550.013 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73569 0 0 0 54753 251 0 0 25 0 1 0 541571483 119689216 27118 4294967295 134512640 134672761 3221224544 3221223584 134612885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27118 603 41 0 29180 0
vsize: 116884
[startup+560.013 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73570 0 0 0 55753 251 0 0 25 0 1 0 541571483 119689216 27119 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27119 603 41 0 29180 0
vsize: 116884
[startup+570.014 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73571 0 0 0 56753 251 0 0 25 0 1 0 541571483 119689216 27120 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27120 603 41 0 29180 0
vsize: 116884
[startup+580.014 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 73573 0 0 0 57753 251 0 0 25 0 1 0 541571483 119689216 27122 4294967295 134512640 134672761 3221224544 3221223584 134612572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27122 603 41 0 29180 0
vsize: 116884
[startup+590.013 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 74126 0 0 0 58752 252 0 0 25 0 1 0 541571483 121962496 27675 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29776 27675 603 41 0 29735 0
vsize: 119104
[startup+600.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 74724 0 0 0 59751 253 0 0 25 0 1 0 541571483 124411904 28273 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30374 28273 603 41 0 30333 0
vsize: 121496
[startup+610.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 75364 0 0 0 60750 254 0 0 25 0 1 0 541571483 127033344 28913 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31014 28913 603 41 0 30973 0
vsize: 124056
[startup+620.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 75630 0 0 0 61750 255 0 0 25 0 1 0 541571483 128217088 29179 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31303 29179 603 41 0 31262 0
vsize: 125212
[startup+630.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 75978 0 0 0 62749 256 0 0 25 0 1 0 541571483 129544192 29527 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31627 29527 603 41 0 31586 0
vsize: 126508
[startup+640.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 76428 0 0 0 63749 256 0 0 25 0 1 0 541571483 131371008 29977 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32073 29977 603 41 0 32032 0
vsize: 128292
[startup+650.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 76760 0 0 0 64748 257 0 0 25 0 1 0 541571483 132804608 30309 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32423 30309 603 41 0 32382 0
vsize: 129692
[startup+660.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 77624 0 0 0 65746 259 0 0 25 0 1 0 541571483 136380416 31173 4294967295 134512640 134672761 3221224544 3221223680 134614560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33296 31173 603 41 0 33255 0
vsize: 133184
[startup+670.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 77946 0 0 0 66746 260 0 0 25 0 1 0 541571483 137953280 31495 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33680 31495 603 41 0 33639 0
vsize: 134720
[startup+680.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 78589 0 0 0 67744 261 0 0 25 0 1 0 541571483 140533760 32138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34310 32138 603 41 0 34269 0
vsize: 137240
[startup+690.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 80437 0 0 0 68741 265 0 0 25 0 1 0 541571483 148119552 33986 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36162 33986 603 41 0 36121 0
vsize: 144648
[startup+700.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 81565 0 0 0 69739 267 0 0 25 0 1 0 541571483 152686592 35114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37277 35114 603 41 0 37236 0
vsize: 149108
[startup+710.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 84593 0 0 0 70727 278 0 0 25 0 1 0 541571483 153923584 35426 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37579 35426 603 41 0 37538 0
vsize: 150316
[startup+720.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 84594 0 0 0 71727 279 0 0 25 0 1 0 541571483 153923584 35427 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37579 35427 603 41 0 37538 0
vsize: 150316
[startup+730.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 84594 0 0 0 72727 279 0 0 25 0 1 0 541571483 153923584 35427 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37579 35427 603 41 0 37538 0
vsize: 150316
[startup+740.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 85842 0 0 0 73722 284 0 0 25 0 1 0 541571483 163647488 36675 4294967295 134512640 134672761 3221224544 3221222848 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39953 36675 603 41 0 39912 0
vsize: 159812
[startup+750.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86722 0 0 0 74719 287 0 0 25 0 1 0 541571483 153636864 35359 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35359 603 41 0 37468 0
vsize: 150036
[startup+760.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86724 0 0 0 75719 287 0 0 25 0 1 0 541571483 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+770.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86724 0 0 0 76719 287 0 0 25 0 1 0 541571483 153636864 35361 4294967295 134512640 134672761 3221224544 3221223584 134612771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+780.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86724 0 0 0 77719 287 0 0 25 0 1 0 541571483 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+790.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86724 0 0 0 78719 287 0 0 25 0 1 0 541571483 153636864 35361 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+800.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86724 0 0 0 79720 287 0 0 25 0 1 0 541571483 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+810.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86724 0 0 0 80720 287 0 0 25 0 1 0 541571483 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+820.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86724 0 0 0 81720 287 0 0 25 0 1 0 541571483 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+830.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86724 0 0 0 82720 287 0 0 25 0 1 0 541571483 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+840.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86724 0 0 0 83720 287 0 0 25 0 1 0 541571483 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+850.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86725 0 0 0 84720 287 0 0 25 0 1 0 541571483 153636864 35362 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35362 603 41 0 37468 0
vsize: 150036
[startup+860.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86726 0 0 0 85721 287 0 0 25 0 1 0 541571483 153636864 35363 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35363 603 41 0 37468 0
vsize: 150036
[startup+870.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86727 0 0 0 86721 287 0 0 25 0 1 0 541571483 153636864 35364 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35364 603 41 0 37468 0
vsize: 150036
[startup+880.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86728 0 0 0 87721 287 0 0 25 0 1 0 541571483 153636864 35365 4294967295 134512640 134672761 3221224544 3221223584 134612860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35365 603 41 0 37468 0
vsize: 150036
[startup+890.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 86729 0 0 0 88721 287 0 0 25 0 1 0 541571483 153636864 35366 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35366 603 41 0 37468 0
vsize: 150036
[startup+900.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 87475 0 0 0 89720 289 0 0 25 0 1 0 541571483 156803072 36112 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38282 36112 603 41 0 38241 0
vsize: 153128
[startup+910.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 88259 0 0 0 90718 291 0 0 25 0 1 0 541571483 159911936 36896 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39041 36896 603 41 0 39000 0
vsize: 156164
[startup+920.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 88818 0 0 0 91716 293 0 0 25 0 1 0 541571483 162250752 37455 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39612 37455 603 41 0 39571 0
vsize: 158448
[startup+930.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 89630 0 0 0 92716 294 0 0 25 0 1 0 541571483 165625856 38267 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40436 38267 603 41 0 40395 0
vsize: 161744
[startup+940.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 90363 0 0 0 93713 296 0 0 25 0 1 0 541571483 168550400 39000 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41150 39000 603 41 0 41109 0
vsize: 164600
[startup+950.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 91073 0 0 0 94712 297 0 0 25 0 1 0 541571483 171466752 39710 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41862 39710 603 41 0 41821 0
vsize: 167448
[startup+960.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 92179 0 0 0 95709 301 0 0 25 0 1 0 541571483 175984640 40816 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42965 40816 603 41 0 42924 0
vsize: 171860
[startup+970.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 26376
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 92953 0 0 0 96707 303 0 0 25 0 1 0 541571483 179224576 41590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43756 41590 603 41 0 43715 0
vsize: 175024
[startup+980.015 s]
Raw data (loadavg): 1.23 1.04 0.95 2/54 26429
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 93773 0 0 0 97705 305 0 0 25 0 1 0 541571483 182476800 42410 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44550 42410 603 41 0 44509 0
vsize: 178200
[startup+990.015 s]
Raw data (loadavg): 1.20 1.03 0.95 2/54 26429
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 94600 0 0 0 98703 307 0 0 25 0 1 0 541571483 185888768 43237 4294967295 134512640 134672761 3221224544 3221223688 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45383 43237 603 41 0 45342 0
vsize: 181532
[startup+1000.02 s]
Raw data (loadavg): 1.17 1.03 0.95 2/54 26429
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 94792 0 0 0 99703 307 0 0 25 0 1 0 541571483 186646528 43429 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45568 43429 603 41 0 45527 0
vsize: 182272
[startup+1010.02 s]
Raw data (loadavg): 1.14 1.03 0.95 2/54 26429
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 95441 0 0 0 100701 309 0 0 25 0 1 0 541571483 189345792 44078 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46227 44078 603 41 0 46186 0
vsize: 184908
[startup+1020.02 s]
Raw data (loadavg): 1.12 1.03 0.95 2/54 26429
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 96615 0 0 0 101698 312 0 0 25 0 1 0 541571483 194215936 45252 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47416 45252 603 41 0 47375 0
vsize: 189664
[startup+1030.02 s]
Raw data (loadavg): 1.10 1.03 0.95 2/54 26429
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 97459 0 0 0 102695 315 0 0 25 0 1 0 541571483 197582848 46096 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48238 46096 603 41 0 48197 0
vsize: 192952
[startup+1040.01 s]
Raw data (loadavg): 1.08 1.03 0.95 2/54 26429
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 97737 0 0 0 103695 316 0 0 25 0 1 0 541571483 198746112 46374 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48522 46374 603 41 0 48481 0
vsize: 194088
[startup+1050.01 s]
Raw data (loadavg): 1.07 1.03 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 98105 0 0 0 104693 318 0 0 25 0 1 0 541571483 200290304 46742 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48899 46742 603 41 0 48858 0
vsize: 195596
[startup+1060.01 s]
Raw data (loadavg): 1.06 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 98610 0 0 0 105692 319 0 0 25 0 1 0 541571483 202309632 47247 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49392 47247 603 41 0 49351 0
vsize: 197568
[startup+1070.02 s]
Raw data (loadavg): 1.05 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 99095 0 0 0 106691 321 0 0 25 0 1 0 541571483 204361728 47732 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49893 47732 603 41 0 49852 0
vsize: 199572
[startup+1080.02 s]
Raw data (loadavg): 1.04 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 99706 0 0 0 107689 323 0 0 25 0 1 0 541571483 206811136 48343 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50491 48343 603 41 0 50450 0
vsize: 201964
[startup+1090.02 s]
Raw data (loadavg): 1.04 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 100381 0 0 0 108687 325 0 0 25 0 1 0 541571483 209559552 49018 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51162 49018 603 41 0 51121 0
vsize: 204648
[startup+1100.02 s]
Raw data (loadavg): 1.03 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 101310 0 0 0 109685 327 0 0 25 0 1 0 541571483 213348352 49947 4294967295 134512640 134672761 3221224544 3221223584 134612595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52087 49947 603 41 0 52046 0
vsize: 208348
[startup+1110.02 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 102199 0 0 0 110683 329 0 0 25 0 1 0 541571483 216981504 50836 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52974 50836 603 41 0 52933 0
vsize: 211896
[startup+1120.02 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 103147 0 0 0 111681 331 0 0 25 0 1 0 541571483 220946432 51784 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53942 51784 603 41 0 53901 0
vsize: 215768
[startup+1130.02 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 103858 0 0 0 112679 333 0 0 25 0 1 0 541571483 223883264 52495 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54659 52495 603 41 0 54618 0
vsize: 218636
[startup+1140.02 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 104570 0 0 0 113678 335 0 0 25 0 1 0 541571483 226721792 53207 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55352 53207 603 41 0 55311 0
vsize: 221408
[startup+1150.02 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 105049 0 0 0 114677 336 0 0 25 0 1 0 541571483 228691968 53686 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55833 53686 603 41 0 55792 0
vsize: 223332
[startup+1160.02 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 105878 0 0 0 115675 338 0 0 25 0 1 0 541571483 232144896 54515 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56676 54515 603 41 0 56635 0
vsize: 226704
[startup+1170.02 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 107102 0 0 0 116672 342 0 0 25 0 1 0 541571483 237068288 55739 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57878 55739 603 41 0 57837 0
vsize: 231512
[startup+1180.02 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 108481 0 0 0 117669 345 0 0 25 0 1 0 541571483 242810880 57118 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59280 57118 603 41 0 59239 0
vsize: 237120
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 109780 0 0 0 118665 348 0 0 25 0 1 0 541571483 248053760 58417 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60560 58417 603 41 0 60519 0
vsize: 242240
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26431
Raw data (stat): 26376 (minisat+) R 26375 26298 26297 0 -1 0 110463 0 0 0 119663 351 0 0 25 0 1 0 541571483 250834944 59100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61239 59100 603 41 0 61198 0
vsize: 244956
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.01 0.95 1/54 26431
Raw data (stat): 26376 (minisat+) Z 26375 26298 26297 0 -1 12 110464 0 0 0 119663 362 0 0 25 0 1 0 541571483 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.14
CPU time (s): 1200.27
CPU user time (s): 1196.64
CPU system time (s): 3.62845
CPU usage (%): 100.011
Max. virtual memory (Kb): 244956
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####