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/miplib/normalized-mps-v2-20-10-mod008.opb
MD5SUM	fbdb3cf321a85412feefcaac30780520
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.01584
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 17036

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 09:23:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12036 boxname=wulflinc23 idbench=926 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fbdb3cf321a85412feefcaac30780520  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-mod008.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-mod008.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-mod008.opb
IDLAUNCH: 12036
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        401944 kB
Buffers:         25288 kB
Cached:         579420 kB
SwapCached:        492 kB
Active:         375848 kB
Inactive:       230916 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        401692 kB
SwapTotal:     2097136 kB
SwapFree:      2095852 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            20256 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:43:40 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 12036 7 1200.24 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.929 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: 32.2471 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.8755 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: 39.156 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: 49.0185 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: 51.3962 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.5787 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.8684 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.7876 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: 63.3834 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.688 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.721 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.687 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.302 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: 306.797 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: 455.075 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: 704.847 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: 741.503 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_0x#### 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.84 0.97 0.98 2/54 1137
Raw data (stat): 1137 (runsolver) R 1136 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543971563 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 6762 0 0 0 980 18 0 0 25 0 1 0 543971563 15093760 3008 4294967295 134512640 134672761 3221224544 3221223088 134621110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3685 3008 603 41 0 3644 0
vsize: 14740
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 14780 0 0 0 1954 42 0 0 25 0 1 0 543971563 46018560 10351 4294967295 134512640 134672761 3221224544 3221222992 134643580 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10351 603 41 0 11194 0
vsize: 44940
[startup+30.0012 s]
Raw data (loadavg): 0.90 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 15462 0 0 0 2950 47 0 0 25 0 1 0 543971563 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.0016 s]
Raw data (loadavg): 0.92 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 22485 0 0 0 3926 70 0 0 25 0 1 0 543971563 60059648 12115 4294967295 134512640 134672761 3221224544 3221222664 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14663 12123 603 41 0 14622 0
vsize: 58652
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 25377 0 0 0 4917 80 0 0 25 0 1 0 543971563 66473984 12547 4294967295 134512640 134672761 3221224544 3221222984 1075331931 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16229 12547 603 41 0 16188 0
vsize: 64916
[startup+60.0017 s]
Raw data (loadavg): 0.94 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 34696 0 0 0 5880 115 0 0 25 0 1 0 543971563 52817920 10768 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12895 10768 603 41 0 12854 0
vsize: 51580
[startup+70.0026 s]
Raw data (loadavg): 0.95 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 42676 0 0 0 6852 143 0 0 25 0 1 0 543971563 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.0032 s]
Raw data (loadavg): 0.96 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 42677 0 0 0 7852 144 0 0 25 0 1 0 543971563 53178368 10860 4294967295 134512640 134672761 3221224544 3221223728 134615544 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.0035 s]
Raw data (loadavg): 0.96 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 42719 0 0 0 8852 144 0 0 25 0 1 0 543971563 53444608 10902 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13048 10902 603 41 0 13007 0
vsize: 52192
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 42816 0 0 0 9851 145 0 0 25 0 1 0 543971563 53841920 10999 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13145 10999 603 41 0 13104 0
vsize: 52580
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 43152 0 0 0 10851 145 0 0 25 0 1 0 543971563 55128064 11335 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13459 11335 603 41 0 13418 0
vsize: 53836
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 43383 0 0 0 11850 146 0 0 25 0 1 0 543971563 56180736 11566 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 11566 603 41 0 13675 0
vsize: 54864
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 46865 0 0 0 12839 158 0 0 25 0 1 0 543971563 57204736 11842 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13966 11842 603 41 0 13925 0
vsize: 55864
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 49420 0 0 0 13830 166 0 0 25 0 1 0 543971563 57225216 11872 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13971 11872 603 41 0 13930 0
vsize: 55884
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 49420 0 0 0 14829 166 0 0 25 0 1 0 543971563 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+160.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 49420 0 0 0 15829 166 0 0 25 0 1 0 543971563 57225216 11872 4294967295 134512640 134672761 3221224544 3221223728 134615551 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.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 49583 0 0 0 16829 167 0 0 25 0 1 0 543971563 58015744 12035 4294967295 134512640 134672761 3221224544 3221223724 134615849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 12035 603 41 0 14123 0
vsize: 56656
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 49787 0 0 0 17828 168 0 0 25 0 1 0 543971563 58789888 12239 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 50222 0 0 0 18828 168 0 0 25 0 1 0 543971563 60600320 12674 4294967295 134512640 134672761 3221224544 3221223728 134615526 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.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 50809 0 0 0 19826 170 0 0 25 0 1 0 543971563 62951424 13261 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15369 13261 603 41 0 15328 0
vsize: 61476
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 51443 0 0 0 20825 171 0 0 25 0 1 0 543971563 65572864 13895 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16009 13895 603 41 0 15968 0
vsize: 64036
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 51977 0 0 0 21824 172 0 0 25 0 1 0 543971563 67788800 14429 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16550 14429 603 41 0 16509 0
vsize: 66200
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 53038 0 0 0 22821 175 0 0 25 0 1 0 543971563 72101888 15490 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17603 15490 603 41 0 17562 0
vsize: 70412
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 53619 0 0 0 23820 177 0 0 25 0 1 0 543971563 74444800 16071 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18175 16071 603 41 0 18134 0
vsize: 72700
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 54657 0 0 0 24818 179 0 0 25 0 1 0 543971563 78733312 17109 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19222 17109 603 41 0 19181 0
vsize: 76888
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 56196 0 0 0 25816 181 0 0 25 0 1 0 543971563 85061632 18648 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20767 18648 603 41 0 20726 0
vsize: 83068
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 59596 0 0 0 26807 191 0 0 25 0 1 0 543971563 87326720 19230 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 59866 0 0 0 27806 191 0 0 25 0 1 0 543971563 88498176 19500 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21606 19500 603 41 0 21565 0
vsize: 86424
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 60514 0 0 0 28806 192 0 0 25 0 1 0 543971563 91209728 20148 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22268 20148 603 41 0 22227 0
vsize: 89072
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 60697 0 0 0 29805 192 0 0 25 0 1 0 543971563 91852800 20331 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22425 20331 603 41 0 22384 0
vsize: 89700
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 63697 0 0 0 30796 202 0 0 25 0 1 0 543971563 92684288 20538 4294967295 134512640 134672761 3221224544 3221223800 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22628 20538 603 41 0 22587 0
vsize: 90512
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 63746 0 0 0 31795 202 0 0 25 0 1 0 543971563 92950528 20587 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22693 20587 603 41 0 22652 0
vsize: 90772
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 63996 0 0 0 32795 203 0 0 25 0 1 0 543971563 94126080 20837 4294967295 134512640 134672761 3221224544 3221223728 134615671 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.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 64426 0 0 0 33794 204 0 0 25 0 1 0 543971563 95821824 21267 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23394 21267 603 41 0 23353 0
vsize: 93576
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 65143 0 0 0 34793 206 0 0 25 0 1 0 543971563 98787328 21984 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24118 21985 603 41 0 24077 0
vsize: 96472
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 65314 0 0 0 35792 206 0 0 25 0 1 0 543971563 99450880 22155 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24280 22155 603 41 0 24239 0
vsize: 97120
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 65517 0 0 0 36792 206 0 0 25 0 1 0 543971563 100364288 22358 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24503 22358 603 41 0 24462 0
vsize: 98012
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 66079 0 0 0 37791 208 0 0 25 0 1 0 543971563 102596608 22920 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25048 22920 603 41 0 25007 0
vsize: 100192
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 67011 0 0 0 38789 210 0 0 25 0 1 0 543971563 106496000 23852 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26000 23852 603 41 0 25959 0
vsize: 104000
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 67372 0 0 0 39788 211 0 0 25 0 1 0 543971563 107954176 24213 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26356 24213 603 41 0 26315 0
vsize: 105424
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 68007 0 0 0 40787 212 0 0 25 0 1 0 543971563 110460928 24848 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 24848 603 41 0 26927 0
vsize: 107872
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 68723 0 0 0 41786 214 0 0 25 0 1 0 543971563 113414144 25564 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27689 25564 603 41 0 27648 0
vsize: 110756
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 69025 0 0 0 42785 214 0 0 25 0 1 0 543971563 114712576 25866 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28006 25866 603 41 0 27965 0
vsize: 112024
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 69708 0 0 0 43784 216 0 0 25 0 1 0 543971563 117485568 26549 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28683 26549 603 41 0 28642 0
vsize: 114732
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 69998 0 0 0 44783 217 0 0 25 0 1 0 543971563 118665216 26839 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28971 26839 603 41 0 28930 0
vsize: 115884
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73563 0 0 0 45770 230 0 0 25 0 1 0 543971563 119689216 27112 4294967295 134512640 134672761 3221224544 3221223800 134616254 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.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73563 0 0 0 46769 230 0 0 25 0 1 0 543971563 119689216 27112 4294967295 134512640 134672761 3221224544 3221223688 134616320 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.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73563 0 0 0 47769 230 0 0 25 0 1 0 543971563 119689216 27112 4294967295 134512640 134672761 3221224544 3221223628 1074754731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73563 0 0 0 48769 230 0 0 25 0 1 0 543971563 119689216 27112 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73563 0 0 0 49769 230 0 0 25 0 1 0 543971563 119689216 27112 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27112 603 41 0 29180 0
vsize: 116884
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73564 0 0 0 50769 230 0 0 25 0 1 0 543971563 119689216 27113 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27113 603 41 0 29180 0
vsize: 116884
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73566 0 0 0 51769 231 0 0 25 0 1 0 543971563 119689216 27115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27115 603 41 0 29180 0
vsize: 116884
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73567 0 0 0 52770 231 0 0 25 0 1 0 543971563 119689216 27116 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27116 603 41 0 29180 0
vsize: 116884
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73568 0 0 0 53770 231 0 0 25 0 1 0 543971563 119689216 27117 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27117 603 41 0 29180 0
vsize: 116884
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73569 0 0 0 54770 231 0 0 25 0 1 0 543971563 119689216 27118 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27118 603 41 0 29180 0
vsize: 116884
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73570 0 0 0 55770 231 0 0 25 0 1 0 543971563 119689216 27119 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27119 603 41 0 29180 0
vsize: 116884
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73571 0 0 0 56770 231 0 0 25 0 1 0 543971563 119689216 27120 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27120 603 41 0 29180 0
vsize: 116884
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73573 0 0 0 57770 231 0 0 25 0 1 0 543971563 119689216 27122 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29221 27122 603 41 0 29180 0
vsize: 116884
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 73963 0 0 0 58769 232 0 0 25 0 1 0 543971563 121331712 27512 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29622 27512 603 41 0 29581 0
vsize: 118488
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 74650 0 0 0 59767 234 0 0 25 0 1 0 543971563 124145664 28199 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30309 28199 603 41 0 30268 0
vsize: 121236
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 75256 0 0 0 60766 235 0 0 25 0 1 0 543971563 126640128 28805 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30918 28805 603 41 0 30877 0
vsize: 123672
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 75582 0 0 0 61766 236 0 0 25 0 1 0 543971563 127959040 29131 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31240 29131 603 41 0 31199 0
vsize: 124960
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 75842 0 0 0 62765 236 0 0 25 0 1 0 543971563 129007616 29391 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31496 29391 603 41 0 31455 0
vsize: 125984
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 76302 0 0 0 63765 237 0 0 25 0 1 0 543971563 130859008 29851 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31948 29851 603 41 0 31907 0
vsize: 127792
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 76581 0 0 0 64764 238 0 0 25 0 1 0 543971563 132046848 30130 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32238 30130 603 41 0 32197 0
vsize: 128952
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 77387 0 0 0 65763 240 0 0 25 0 1 0 543971563 135364608 30936 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33048 30936 603 41 0 33007 0
vsize: 132192
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 77769 0 0 0 66762 241 0 0 25 0 1 0 543971563 136904704 31318 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33424 31318 603 41 0 33383 0
vsize: 133696
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 78329 0 0 0 67760 243 0 0 25 0 1 0 543971563 139497472 31878 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34057 31878 603 41 0 34016 0
vsize: 136228
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 79530 0 0 0 68757 246 0 0 25 0 1 0 543971563 144429056 33079 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35261 33079 603 41 0 35220 0
vsize: 141044
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 81213 0 0 0 69754 249 0 0 25 0 1 0 543971563 151232512 34762 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36922 34762 603 41 0 36881 0
vsize: 147688
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 84593 0 0 0 70742 260 0 0 25 0 1 0 543971563 153923584 35426 4294967295 134512640 134672761 3221224544 3221223800 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37579 35426 603 41 0 37538 0
vsize: 150316
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 84594 0 0 0 71742 261 0 0 25 0 1 0 543971563 153923584 35427 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37579 35427 603 41 0 37538 0
vsize: 150316
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 84594 0 0 0 72742 261 0 0 25 0 1 0 543971563 153923584 35427 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37579 35427 603 41 0 37538 0
vsize: 150316
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 84594 0 0 0 73742 261 0 0 25 0 1 0 543971563 153923584 35427 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37579 35427 603 41 0 37538 0
vsize: 150316
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86722 0 0 0 74734 268 0 0 25 0 1 0 543971563 153636864 35359 4294967295 134512640 134672761 3221224544 3221223584 134614228 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.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86722 0 0 0 75734 268 0 0 25 0 1 0 543971563 153636864 35359 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35359 603 41 0 37468 0
vsize: 150036
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86724 0 0 0 76734 268 0 0 25 0 1 0 543971563 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86724 0 0 0 77734 269 0 0 25 0 1 0 543971563 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86724 0 0 0 78735 269 0 0 25 0 1 0 543971563 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86724 0 0 0 79735 269 0 0 25 0 1 0 543971563 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86724 0 0 0 80735 269 0 0 25 0 1 0 543971563 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86724 0 0 0 81735 269 0 0 25 0 1 0 543971563 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86724 0 0 0 82736 269 0 0 25 0 1 0 543971563 153636864 35361 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86724 0 0 0 83736 269 0 0 25 0 1 0 543971563 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+850.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86724 0 0 0 84736 269 0 0 25 0 1 0 543971563 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35361 603 41 0 37468 0
vsize: 150036
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86726 0 0 0 85736 269 0 0 25 0 1 0 543971563 153636864 35363 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35363 603 41 0 37468 0
vsize: 150036
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86726 0 0 0 86736 269 0 0 25 0 1 0 543971563 153636864 35363 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35363 603 41 0 37468 0
vsize: 150036
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86727 0 0 0 87737 269 0 0 25 0 1 0 543971563 153636864 35364 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35364 603 41 0 37468 0
vsize: 150036
[startup+890.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86728 0 0 0 88737 269 0 0 25 0 1 0 543971563 153636864 35365 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37509 35365 603 41 0 37468 0
vsize: 150036
[startup+900.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 86810 0 0 0 89737 269 0 0 25 0 1 0 543971563 154009600 35447 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37600 35447 603 41 0 37559 0
vsize: 150400
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 87672 0 0 0 90735 271 0 0 25 0 1 0 543971563 157589504 36309 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38474 36309 603 41 0 38433 0
vsize: 153896
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 88460 0 0 0 91733 273 0 0 25 0 1 0 543971563 160821248 37097 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39263 37097 603 41 0 39222 0
vsize: 157052
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 88949 0 0 0 92731 275 0 0 25 0 1 0 543971563 162783232 37586 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39742 37586 603 41 0 39701 0
vsize: 158968
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 89878 0 0 0 93729 277 0 0 25 0 1 0 543971563 166612992 38515 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40677 38515 603 41 0 40636 0
vsize: 162708
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 90455 0 0 0 94727 279 0 0 25 0 1 0 543971563 168943616 39092 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41246 39092 603 41 0 41205 0
vsize: 164984
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 91265 0 0 0 95726 281 0 0 25 0 1 0 543971563 172318720 39902 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42070 39902 603 41 0 42029 0
vsize: 168280
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 92307 0 0 0 96723 284 0 0 25 0 1 0 543971563 176578560 40944 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43110 40944 603 41 0 43069 0
vsize: 172440
[startup+980.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 93056 0 0 0 97721 286 0 0 25 0 1 0 543971563 179646464 41693 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43859 41693 603 41 0 43818 0
vsize: 175436
[startup+990.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 93878 0 0 0 98720 288 0 0 25 0 1 0 543971563 182964224 42515 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44669 42515 603 41 0 44628 0
vsize: 178676
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 94600 0 0 0 99718 289 0 0 25 0 1 0 543971563 185888768 43237 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45383 43237 603 41 0 45342 0
vsize: 181532
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 94912 0 0 0 100717 290 0 0 25 0 1 0 543971563 187150336 43549 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45691 43549 603 41 0 45650 0
vsize: 182764
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 95550 0 0 0 101717 291 0 0 25 0 1 0 543971563 189857792 44187 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46352 44187 603 41 0 46311 0
vsize: 185408
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 96758 0 0 0 102713 294 0 0 25 0 1 0 543971563 194703360 45395 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47535 45395 603 41 0 47494 0
vsize: 190140
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 97502 0 0 0 103712 296 0 0 25 0 1 0 543971563 197836800 46139 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48300 46139 603 41 0 48259 0
vsize: 193200
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 97755 0 0 0 104711 297 0 0 25 0 1 0 543971563 198868992 46392 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48552 46392 603 41 0 48511 0
vsize: 194208
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 98123 0 0 0 105709 299 0 0 25 0 1 0 543971563 200290304 46760 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48899 46760 603 41 0 48858 0
vsize: 195596
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 98617 0 0 0 106708 301 0 0 25 0 1 0 543971563 202309632 47254 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49392 47254 603 41 0 49351 0
vsize: 197568
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 99094 0 0 0 107707 302 0 0 25 0 1 0 543971563 204361728 47731 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49893 47731 603 41 0 49852 0
vsize: 199572
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 99700 0 0 0 108706 303 0 0 25 0 1 0 543971563 206811136 48337 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50491 48337 603 41 0 50450 0
vsize: 201964
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 100342 0 0 0 109704 305 0 0 25 0 1 0 543971563 209436672 48979 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51132 48979 603 41 0 51091 0
vsize: 204528
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 101284 0 0 0 110702 307 0 0 25 0 1 0 543971563 213348352 49921 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52087 49921 603 41 0 52046 0
vsize: 208348
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 102142 0 0 0 111701 309 0 0 25 0 1 0 543971563 216862720 50779 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52945 50779 603 41 0 52904 0
vsize: 211780
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 103105 0 0 0 112699 311 0 0 25 0 1 0 543971563 220704768 51742 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53883 51742 603 41 0 53842 0
vsize: 215532
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 103791 0 0 0 113697 313 0 0 25 0 1 0 543971563 223625216 52428 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54596 52428 603 41 0 54555 0
vsize: 218384
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 104499 0 0 0 114695 315 0 0 25 0 1 0 543971563 226467840 53136 4294967295 134512640 134672761 3221224544 3221223540 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55290 53136 603 41 0 55249 0
vsize: 221160
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 104993 0 0 0 115694 316 0 0 25 0 1 0 543971563 228429824 53630 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55769 53630 603 41 0 55728 0
vsize: 223076
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 105710 0 0 0 116693 318 0 0 25 0 1 0 543971563 231411712 54347 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56497 54347 603 41 0 56456 0
vsize: 225988
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 106800 0 0 0 117691 320 0 0 25 0 1 0 543971563 235851776 55437 4294967295 134512640 134672761 3221224544 3221223584 134614258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57581 55437 603 41 0 57540 0
vsize: 230324
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 108234 0 0 0 118688 323 0 0 25 0 1 0 543971563 241762304 56871 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59024 56871 603 41 0 58983 0
vsize: 236096
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 1137
Raw data (stat): 1137 (minisat+) R 1136 3260 3259 0 -1 0 109592 0 0 0 119685 326 0 0 25 0 1 0 543971563 247357440 58229 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60390 58229 603 41 0 60349 0
vsize: 241560
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.98 1/54 1137
Raw data (stat): 1137 (minisat+) Z 1136 3260 3259 0 -1 12 109593 0 0 0 119685 337 0 0 25 0 1 0 543971563 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.13
CPU time (s): 1200.24
CPU user time (s): 1196.86
CPU system time (s): 3.37849
CPU usage (%): 100.009
Max. virtual memory (Kb): 241560
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####