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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.01784
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 21217

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 23:09:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13635 boxname=wulflinc10 idbench=1049 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  581d778a36086562107993896110e0a2  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-mod008.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-mod008.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-mod008.opb
IDLAUNCH: 13635
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        733020 kB
Buffers:         21240 kB
Cached:         259124 kB
SwapCached:          0 kB
Active:          43416 kB
Inactive:       239464 kB
HighTotal:      131008 kB
HighFree:          840 kB
LowTotal:       903652 kB
LowFree:        732180 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13144 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:29:04 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 13635 7 1200.3 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.5471 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.4222 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: 34.9187 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.0702 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: 47.4788 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: 49.8094 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: 52.887 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: 55.1396 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: 59.8909 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: 61.4637 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: 63.7283 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: 120.818 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: 132.414 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: 255.277 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: 297.282 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: 439.591 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: 679.431 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: 714.802 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.92 0.98 0.99 2/54 6376
Raw data (stat): 6376 (runsolver) R 6375 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490711883 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.001 s]
Raw data (loadavg): 0.93 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 6762 0 0 0 982 16 0 0 25 0 1 0 490711883 15093760 3008 4294967295 134512640 134672761 3221224544 3221223088 134621098 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.0019 s]
Raw data (loadavg): 0.94 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 14782 0 0 0 1957 41 0 0 25 0 1 0 490711883 46018560 10353 4294967295 134512640 134672761 3221224544 3221222992 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11235 10353 603 41 0 11194 0
vsize: 44940
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 15462 0 0 0 2952 46 0 0 25 0 1 0 490711883 45670400 10318 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.0015 s]
Raw data (loadavg): 0.96 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 23411 0 0 0 3924 73 0 0 25 0 1 0 490711883 52826112 10720 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12897 10720 603 41 0 12856 0
vsize: 51588
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 26481 0 0 0 4913 84 0 0 25 0 1 0 490711883 52719616 10719 4294967295 134512640 134672761 3221224544 3221223552 134565029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12871 10719 603 41 0 12830 0
vsize: 51484
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 34696 0 0 0 5884 113 0 0 25 0 1 0 490711883 52817920 10768 4294967295 134512640 134672761 3221224544 3221223584 134612987 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.0036 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 42677 0 0 0 6860 137 0 0 25 0 1 0 490711883 53178368 10860 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12983 10860 603 41 0 12942 0
vsize: 51932
[startup+80.0042 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 42677 0 0 0 7860 137 0 0 25 0 1 0 490711883 53178368 10860 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.0044 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 42752 0 0 0 8859 138 0 0 25 0 1 0 490711883 53575680 10935 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13080 10935 603 41 0 13039 0
vsize: 52320
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 42972 0 0 0 9859 139 0 0 25 0 1 0 490711883 54493184 11155 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13304 11155 603 41 0 13263 0
vsize: 53216
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 43334 0 0 0 10858 139 0 0 25 0 1 0 490711883 55910400 11517 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13650 11517 603 41 0 13609 0
vsize: 54600
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 43454 0 0 0 11858 140 0 0 25 0 1 0 490711883 56446976 11637 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13781 11637 603 41 0 13740 0
vsize: 55124
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 46865 0 0 0 12847 151 0 0 25 0 1 0 490711883 57204736 11842 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.005 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 49420 0 0 0 13837 161 0 0 25 0 1 0 490711883 57225216 11872 4294967295 134512640 134672761 3221224544 3221223744 134619616 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.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 49420 0 0 0 14837 161 0 0 25 0 1 0 490711883 57225216 11872 4294967295 134512640 134672761 3221224544 3221223680 134614551 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.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 49469 0 0 0 15837 161 0 0 25 0 1 0 490711883 57487360 11921 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14035 11921 603 41 0 13994 0
vsize: 56140
[startup+170.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 49664 0 0 0 16836 162 0 0 25 0 1 0 490711883 58277888 12116 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 12116 603 41 0 14187 0
vsize: 56912
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 50092 0 0 0 17834 164 0 0 25 0 1 0 490711883 60076032 12544 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14667 12544 603 41 0 14626 0
vsize: 58668
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 50451 0 0 0 18834 165 0 0 25 0 1 0 490711883 61493248 12903 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15013 12903 603 41 0 14972 0
vsize: 60052
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 51353 0 0 0 19832 167 0 0 25 0 1 0 490711883 65179648 13805 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15913 13805 603 41 0 15872 0
vsize: 63652
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 51759 0 0 0 20831 168 0 0 25 0 1 0 490711883 66883584 14211 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16329 14211 603 41 0 16288 0
vsize: 65316
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 52692 0 0 0 21829 170 0 0 25 0 1 0 490711883 70717440 15144 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17265 15144 603 41 0 17224 0
vsize: 69060
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 53534 0 0 0 22825 174 0 0 25 0 1 0 490711883 74182656 15986 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18111 15986 603 41 0 18070 0
vsize: 72444
[startup+240.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 54204 0 0 0 23823 176 0 0 25 0 1 0 490711883 76894208 16656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18773 16656 603 41 0 18732 0
vsize: 75092
[startup+250.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 55939 0 0 0 24820 179 0 0 25 0 1 0 490711883 83939328 18391 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20493 18391 603 41 0 20452 0
vsize: 81972
[startup+260.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 59596 0 0 0 25807 192 0 0 25 0 1 0 490711883 87326720 19230 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21320 19230 603 41 0 21279 0
vsize: 85280
[startup+270.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 59761 0 0 0 26807 193 0 0 25 0 1 0 490711883 88109056 19395 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21511 19395 603 41 0 21470 0
vsize: 86044
[startup+280.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 60437 0 0 0 27805 195 0 0 25 0 1 0 490711883 90816512 20071 4294967295 134512640 134672761 3221224544 3221223680 134614699 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22172 20071 603 41 0 22131 0
vsize: 88688
[startup+290.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 60681 0 0 0 28804 196 0 0 25 0 1 0 490711883 91852800 20315 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22425 20315 603 41 0 22384 0
vsize: 89700
[startup+300.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 63230 0 0 0 29797 203 0 0 25 0 1 0 490711883 100397056 21820 4294967295 134512640 134672761 3221224544 3221222916 134553648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24511 21820 603 41 0 24470 0
vsize: 98044
[startup+310.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 63746 0 0 0 30796 205 0 0 25 0 1 0 490711883 92950528 20587 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22693 20587 603 41 0 22652 0
vsize: 90772
[startup+320.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 63996 0 0 0 31796 206 0 0 25 0 1 0 490711883 94126080 20837 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22980 20837 603 41 0 22939 0
vsize: 91920
[startup+330.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 64502 0 0 0 32794 207 0 0 25 0 1 0 490711883 96210944 21343 4294967295 134512640 134672761 3221224544 3221223584 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23489 21343 603 41 0 23448 0
vsize: 93956
[startup+340.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 65212 0 0 0 33793 208 0 0 25 0 1 0 490711883 99045376 22053 4294967295 134512640 134672761 3221224544 3221223744 134610602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24181 22053 603 41 0 24140 0
vsize: 96724
[startup+350.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 65353 0 0 0 34793 209 0 0 25 0 1 0 490711883 99708928 22194 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24343 22194 603 41 0 24302 0
vsize: 97372
[startup+360.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 65540 0 0 0 35793 209 0 0 25 0 1 0 490711883 100364288 22381 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24503 22381 603 41 0 24462 0
vsize: 98012
[startup+370.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 66325 0 0 0 36791 212 0 0 25 0 1 0 490711883 103641088 23166 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25303 23166 603 41 0 25262 0
vsize: 101212
[startup+380.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 67097 0 0 0 37789 213 0 0 25 0 1 0 490711883 106762240 23938 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26065 23938 603 41 0 26024 0
vsize: 104260
[startup+390.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 67520 0 0 0 38788 215 0 0 25 0 1 0 490711883 108478464 24361 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26484 24361 603 41 0 26443 0
vsize: 105936
[startup+400.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 68328 0 0 0 39786 216 0 0 25 0 1 0 490711883 111845376 25169 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27306 25169 603 41 0 27265 0
vsize: 109224
[startup+410.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 68826 0 0 0 40785 217 0 0 25 0 1 0 490711883 113795072 25667 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27782 25667 603 41 0 27741 0
vsize: 111128
[startup+420.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 69423 0 0 0 41785 219 0 0 25 0 1 0 490711883 116326400 26264 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28400 26264 603 41 0 28359 0
vsize: 113600
[startup+430.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 69827 0 0 0 42784 219 0 0 25 0 1 0 490711883 117878784 26668 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28779 26668 603 41 0 28738 0
vsize: 115116
[startup+440.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 70172 0 0 0 43783 220 0 0 25 0 1 0 490711883 119332864 27013 4294967295 134512640 134672761 3221224544 3221223584 134612696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29134 27013 603 41 0 29093 0
vsize: 116536
[startup+450.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73563 0 0 0 44773 230 0 0 25 0 1 0 490711883 119689216 27112 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+460.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73563 0 0 0 45773 230 0 0 25 0 1 0 490711883 119689216 27112 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+470.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73563 0 0 0 46773 230 0 0 25 0 1 0 490711883 119689216 27112 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73563 0 0 0 47773 230 0 0 25 0 1 0 490711883 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.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73564 0 0 0 48773 230 0 0 25 0 1 0 490711883 119689216 27113 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27113 603 41 0 29180 0
vsize: 116884
[startup+500.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73566 0 0 0 49774 230 0 0 25 0 1 0 490711883 119689216 27115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27115 603 41 0 29180 0
vsize: 116884
[startup+510.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73567 0 0 0 50774 230 0 0 25 0 1 0 490711883 119689216 27116 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27116 603 41 0 29180 0
vsize: 116884
[startup+520.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73568 0 0 0 51774 230 0 0 25 0 1 0 490711883 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+530.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73569 0 0 0 52774 230 0 0 25 0 1 0 490711883 119689216 27118 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27118 603 41 0 29180 0
vsize: 116884
[startup+540.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73570 0 0 0 53774 230 0 0 25 0 1 0 490711883 119689216 27119 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27119 603 41 0 29180 0
vsize: 116884
[startup+550.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73571 0 0 0 54774 230 0 0 25 0 1 0 490711883 119689216 27120 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27120 603 41 0 29180 0
vsize: 116884
[startup+560.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 73573 0 0 0 55775 231 0 0 25 0 1 0 490711883 119689216 27122 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29221 27122 603 41 0 29180 0
vsize: 116884
[startup+570.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 74019 0 0 0 56774 232 0 0 25 0 1 0 490711883 121589760 27568 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29685 27568 603 41 0 29644 0
vsize: 118740
[startup+580.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 74662 0 0 0 57772 233 0 0 25 0 1 0 490711883 124145664 28211 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30309 28211 603 41 0 30268 0
vsize: 121236
[startup+590.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 75300 0 0 0 58771 235 0 0 25 0 1 0 490711883 126771200 28849 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30950 28849 603 41 0 30909 0
vsize: 123800
[startup+600.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 75623 0 0 0 59770 236 0 0 25 0 1 0 490711883 128090112 29172 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31272 29172 603 41 0 31231 0
vsize: 125088
[startup+610.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 75955 0 0 0 60770 236 0 0 25 0 1 0 490711883 129544192 29504 4294967295 134512640 134672761 3221224544 3221223416 1075353266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31627 29504 603 41 0 31586 0
vsize: 126508
[startup+620.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 76423 0 0 0 61769 237 0 0 25 0 1 0 490711883 131371008 29972 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32073 29972 603 41 0 32032 0
vsize: 128292
[startup+630.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 76787 0 0 0 62769 238 0 0 25 0 1 0 490711883 132927488 30336 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32453 30336 603 41 0 32412 0
vsize: 129812
[startup+640.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 77642 0 0 0 63767 240 0 0 25 0 1 0 490711883 136380416 31191 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33296 31191 603 41 0 33255 0
vsize: 133184
[startup+650.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 77997 0 0 0 64766 241 0 0 25 0 1 0 490711883 138084352 31546 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33712 31546 603 41 0 33671 0
vsize: 134848
[startup+660.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 78698 0 0 0 65764 243 0 0 25 0 1 0 490711883 140906496 32247 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34401 32247 603 41 0 34360 0
vsize: 137604
[startup+670.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 80649 0 0 0 66760 247 0 0 25 0 1 0 490711883 148979712 34198 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36372 34198 603 41 0 36331 0
vsize: 145488
[startup+680.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 81715 0 0 0 67758 250 0 0 25 0 1 0 490711883 153317376 35264 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37431 35264 603 41 0 37390 0
vsize: 149724
[startup+690.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 84593 0 0 0 68748 259 0 0 25 0 1 0 490711883 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+700.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 84594 0 0 0 69747 259 0 0 25 0 1 0 490711883 153923584 35427 4294967295 134512640 134672761 3221224544 3221223688 134616254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37579 35427 603 41 0 37538 0
vsize: 150316
[startup+710.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 84594 0 0 0 70748 259 0 0 25 0 1 0 490711883 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+720.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86722 0 0 0 71738 269 0 0 25 0 1 0 490711883 153636864 35359 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35359 603 41 0 37468 0
vsize: 150036
[startup+730.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86722 0 0 0 72738 269 0 0 25 0 1 0 490711883 153636864 35359 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35359 603 41 0 37468 0
vsize: 150036
[startup+740.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86724 0 0 0 73738 269 0 0 25 0 1 0 490711883 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+750.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86724 0 0 0 74738 269 0 0 25 0 1 0 490711883 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+760.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86724 0 0 0 75739 269 0 0 25 0 1 0 490711883 153636864 35361 4294967295 134512640 134672761 3221224544 3221223744 134610707 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): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86724 0 0 0 76739 269 0 0 25 0 1 0 490711883 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+780.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86724 0 0 0 77739 269 0 0 25 0 1 0 490711883 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615627 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): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86724 0 0 0 78739 269 0 0 25 0 1 0 490711883 153636864 35361 4294967295 134512640 134672761 3221224544 3221223584 134612987 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): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86724 0 0 0 79739 269 0 0 25 0 1 0 490711883 153636864 35361 4294967295 134512640 134672761 3221224544 3221223584 134612614 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): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86724 0 0 0 80740 269 0 0 25 0 1 0 490711883 153636864 35361 4294967295 134512640 134672761 3221224544 3221223688 134616350 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.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86725 0 0 0 81740 269 0 0 25 0 1 0 490711883 153636864 35362 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35362 603 41 0 37468 0
vsize: 150036
[startup+830.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86726 0 0 0 82740 269 0 0 25 0 1 0 490711883 153636864 35363 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35363 603 41 0 37468 0
vsize: 150036
[startup+840.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86727 0 0 0 83740 269 0 0 25 0 1 0 490711883 153636864 35364 4294967295 134512640 134672761 3221224544 3221223584 134613122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35364 603 41 0 37468 0
vsize: 150036
[startup+850.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86727 0 0 0 84740 269 0 0 25 0 1 0 490711883 153636864 35364 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35364 603 41 0 37468 0
vsize: 150036
[startup+860.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 86728 0 0 0 85741 269 0 0 25 0 1 0 490711883 153636864 35365 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35365 603 41 0 37468 0
vsize: 150036
[startup+870.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 87104 0 0 0 86740 270 0 0 25 0 1 0 490711883 155254784 35741 4294967295 134512640 134672761 3221224544 3221223680 134614750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37904 35741 603 41 0 37863 0
vsize: 151616
[startup+880.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 87931 0 0 0 87739 271 0 0 25 0 1 0 490711883 158629888 36568 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38728 36568 603 41 0 38687 0
vsize: 154912
[startup+890.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 88617 0 0 0 88737 273 0 0 25 0 1 0 490711883 161480704 37254 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39424 37254 603 41 0 39383 0
vsize: 157696
[startup+900.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 89279 0 0 0 89736 274 0 0 25 0 1 0 490711883 164188160 37916 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40085 37916 603 41 0 40044 0
vsize: 160340
[startup+910.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 90102 0 0 0 90735 276 0 0 25 0 1 0 490711883 167514112 38739 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40897 38739 603 41 0 40856 0
vsize: 163588
[startup+920.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 90754 0 0 0 91733 278 0 0 25 0 1 0 490711883 170233856 39391 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41561 39391 603 41 0 41520 0
vsize: 166244
[startup+930.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 91885 0 0 0 92731 280 0 0 25 0 1 0 490711883 174739456 40522 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42661 40522 603 41 0 42620 0
vsize: 170644
[startup+940.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 92781 0 0 0 93730 281 0 0 25 0 1 0 490711883 178475008 41418 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43573 41418 603 41 0 43532 0
vsize: 174292
[startup+950.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 93486 0 0 0 94729 282 0 0 25 0 1 0 490711883 181338112 42123 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44272 42123 603 41 0 44231 0
vsize: 177088
[startup+960.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 94568 0 0 0 95728 284 0 0 25 0 1 0 490711883 185761792 43205 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45352 43205 603 41 0 45311 0
vsize: 181408
[startup+970.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 94756 0 0 0 96727 285 0 0 25 0 1 0 490711883 186527744 43393 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45539 43393 603 41 0 45498 0
vsize: 182156
[startup+980.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 95264 0 0 0 97726 286 0 0 25 0 1 0 490711883 188690432 43901 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46067 43901 603 41 0 46026 0
vsize: 184268
[startup+990.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 96391 0 0 0 98725 288 0 0 25 0 1 0 490711883 193232896 45028 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47176 45028 603 41 0 47135 0
vsize: 188704
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 97394 0 0 0 99723 290 0 0 25 0 1 0 490711883 197320704 46031 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48174 46031 603 41 0 48133 0
vsize: 192696
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 97692 0 0 0 100722 291 0 0 25 0 1 0 490711883 198615040 46329 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48490 46329 603 41 0 48449 0
vsize: 193960
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 98058 0 0 0 101721 292 0 0 25 0 1 0 490711883 200040448 46695 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48838 46695 603 41 0 48797 0
vsize: 195352
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 98559 0 0 0 102720 293 0 0 25 0 1 0 490711883 202182656 47196 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49361 47196 603 41 0 49320 0
vsize: 197444
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 99043 0 0 0 103719 295 0 0 25 0 1 0 490711883 204115968 47680 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49833 47680 603 41 0 49792 0
vsize: 199332
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 99655 0 0 0 104717 297 0 0 25 0 1 0 490711883 206565376 48292 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50431 48292 603 41 0 50390 0
vsize: 201724
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 100337 0 0 0 105716 299 0 0 25 0 1 0 490711883 209436672 48974 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51132 48974 603 41 0 51091 0
vsize: 204528
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 101305 0 0 0 106713 301 0 0 25 0 1 0 490711883 213348352 49942 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52087 49942 603 41 0 52046 0
vsize: 208348
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 102199 0 0 0 107712 302 0 0 25 0 1 0 490711883 216981504 50836 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52974 50836 603 41 0 52933 0
vsize: 211896
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 103165 0 0 0 108710 305 0 0 25 0 1 0 490711883 220946432 51802 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53942 51802 603 41 0 53901 0
vsize: 215768
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 103877 0 0 0 109709 306 0 0 25 0 1 0 490711883 223883264 52514 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54659 52514 603 41 0 54618 0
vsize: 218636
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 104581 0 0 0 110707 308 0 0 25 0 1 0 490711883 226848768 53218 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55383 53218 603 41 0 55342 0
vsize: 221532
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 105073 0 0 0 111706 309 0 0 25 0 1 0 490711883 228818944 53710 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55864 53710 603 41 0 55823 0
vsize: 223456
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 106041 0 0 0 112704 311 0 0 25 0 1 0 490711883 232759296 54678 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56826 54678 603 41 0 56785 0
vsize: 227304
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 107227 0 0 0 113702 313 0 0 25 0 1 0 490711883 237580288 55864 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58003 55864 603 41 0 57962 0
vsize: 232012
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 108657 0 0 0 114700 316 0 0 25 0 1 0 490711883 243445760 57294 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59435 57294 603 41 0 59394 0
vsize: 237740
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 109893 0 0 0 115697 319 0 0 25 0 1 0 490711883 248549376 58530 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60681 58530 603 41 0 60640 0
vsize: 242724
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 110583 0 0 0 116696 321 0 0 25 0 1 0 490711883 251351040 59220 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61365 59220 603 41 0 61324 0
vsize: 245460
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 111566 0 0 0 117693 323 0 0 25 0 1 0 490711883 255373312 60203 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62347 60203 603 41 0 62306 0
vsize: 249388
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 112626 0 0 0 118691 326 0 0 25 0 1 0 490711883 259756032 61263 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63417 61263 603 41 0 63376 0
vsize: 253668
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 6376
Raw data (stat): 6376 (minisat+) R 6375 25347 25346 0 -1 0 113854 0 0 0 119689 328 0 0 25 0 1 0 490711883 264728576 62491 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64631 62491 603 41 0 64590 0
vsize: 258524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.98 0.99 1/54 6376
Raw data (stat): 6376 (minisat+) Z 6375 25347 25346 0 -1 12 113855 0 0 0 119689 340 0 0 25 0 1 0 490711883 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.15
CPU time (s): 1200.3
CPU user time (s): 1196.9
CPU system time (s): 3.40848
CPU usage (%): 100.013
Max. virtual memory (Kb): 258524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####