PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.01684
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 15637

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        804092 kB
Buffers:         20656 kB
Cached:         189820 kB
SwapCached:        732 kB
Active:          39572 kB
Inactive:       172904 kB
HighTotal:      131008 kB
HighFree:          308 kB
LowTotal:       903652 kB
LowFree:        803784 kB
SwapTotal:     2097892 kB
SwapFree:      2096248 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            12400 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:39:36 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 17028 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss
c ---[   8]---> Adder-cost: 2481   maxlim: 21999   bits: 16/15
c ---[   5]---> Adder-cost: 2052   maxlim: 4999   bits: 14/13
c ---[   4]---> Adder-cost: 2306   maxlim: 11999   bits: 15/14
c ---[   2]---> BDD-cost:  478
c ---[   1]---> BDD-cost: 2553
c ---[   0]---> Adder-cost: 1803   maxlim: 3999   bits: 13/12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   62010   221290 |   18602       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10281          
c   -- var.elim.:  2000/10281          
c   -- var.elim.:  3000/10281          
c   -- var.elim.:  4000/10281          
c   -- var.elim.:  5000/10281          
c   -- var.elim.:  6000/10281          
c   -- var.elim.:  7000/10281          
c   -- var.elim.:  8000/10281          
c   -- var.elim.:  9000/10281          
c   -- var.elim.:  10000/10281          
c   -- var.elim.:  10281/10281          
c   -- var.elim.:  1000/1496          
c   -- var.elim.:  1496/1496          
c   -- var.elim.:  439/439          
c   -- subsuming                       
c   -- var.elim.:  353/353          
c   -- var.elim.:  126/126          
c |         0 |   60992   316610 |      --       0       --      -- |     --   | -1018/95348
c |         0 |   60992   316610 |   24396       0        0     nan |  0.000 % |
c |       100 |   60992   316610 |   26836     100      355     3.5 |  0.295 % |
c |       251 |   60992   316610 |   29520     251      947     3.8 |  0.295 % |
c |       476 |   60992   316610 |   32472     476     2140     4.5 |  0.295 % |
c |       813 |   60992   316610 |   35719     813     5035     6.2 |  0.295 % |
c |      1319 |   60992   316610 |   39291    1319    23867    18.1 |  0.295 % |
c |      2078 |   60992   316610 |   43220    2078    34107    16.4 |  0.295 % |
c ==============================================================================
c (current CPU-time: 12.7651 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.7482 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.2486 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.4512 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.8817 s)
c ==============================================================================
c [1mFound solution: 713[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5839 |  196578   764111 |   58973    5839   254144    43.5 |  0.083 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2696          
c   -- var.elim.:  2000/2696          
c   -- var.elim.:  2696/2696          
c   -- var.elim.:  1000/1422          
c   -- var.elim.:  1422/1422          
c   -- subsuming                       
c   -- var.elim.:  94/94          
c |      5839 |  195617   765564 |      --    5839       --      -- |     --   | -961/1454
c |      5839 |  195617   765564 |   78246    5839   254144    43.5 |  0.083 % |
c ==============================================================================
c (current CPU-time: 50.2104 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: 53.2999 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.5546 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: 60.2658 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.8336 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: 64.0953 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.487 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: 131.991 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: 253.312 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: 295.06 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: 437.48 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: 677.498 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: 712.902 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_0#### 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.60 0.90 0.92 2/54 29832
Raw data (stat): 29832 (runsolver) D 29831 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542517928 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.66 0.90 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 6762 0 0 0 980 18 0 0 25 0 1 0 542517928 15093760 3008 4294967295 134512640 134672761 3221224544 3221223088 134620997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3685 3008 603 41 0 3644 0
vsize: 14740
[startup+19.9998 s]
Raw data (loadavg): 0.71 0.91 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 14781 0 0 0 1954 43 0 0 25 0 1 0 542517928 46018560 10352 4294967295 134512640 134672761 3221224544 3221222992 134606971 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11235 10352 603 41 0 11194 0
vsize: 44940
[startup+30.0003 s]
Raw data (loadavg): 0.75 0.91 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 15462 0 0 0 2948 49 0 0 25 0 1 0 542517928 45670400 10318 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11150 10318 603 41 0 11109 0
vsize: 44600
[startup+39.9999 s]
Raw data (loadavg): 0.79 0.91 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 23000 0 0 0 3924 73 0 0 25 0 1 0 542517928 52826112 10718 4294967295 134512640 134672761 3221224544 3221222672 134522981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12897 10718 603 41 0 12856 0
vsize: 51588
[startup+49.9995 s]
Raw data (loadavg): 0.82 0.91 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 26481 0 0 0 4911 86 0 0 25 0 1 0 542517928 54677504 11162 4294967295 134512640 134672761 3221224544 3221223088 134621235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13349 11162 603 41 0 13308 0
vsize: 53396
[startup+59.9991 s]
Raw data (loadavg): 0.85 0.92 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 34696 0 0 0 5882 114 0 0 25 0 1 0 542517928 52817920 10768 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12895 10768 603 41 0 12854 0
vsize: 51580
[startup+69.9988 s]
Raw data (loadavg): 0.87 0.92 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 42677 0 0 0 6856 139 0 0 25 0 1 0 542517928 53178368 10860 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12983 10860 603 41 0 12942 0
vsize: 51932
[startup+79.9993 s]
Raw data (loadavg): 0.89 0.92 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 42677 0 0 0 7856 139 0 0 25 0 1 0 542517928 53178368 10860 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12983 10860 603 41 0 12942 0
vsize: 51932
[startup+89.9988 s]
Raw data (loadavg): 0.91 0.92 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 42752 0 0 0 8856 140 0 0 25 0 1 0 542517928 53575680 10935 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13080 10935 603 41 0 13039 0
vsize: 52320
[startup+99.9984 s]
Raw data (loadavg): 0.92 0.92 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 42972 0 0 0 9856 140 0 0 25 0 1 0 542517928 54493184 11155 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13304 11155 603 41 0 13263 0
vsize: 53216
[startup+109.999 s]
Raw data (loadavg): 0.93 0.93 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 43334 0 0 0 10855 141 0 0 25 0 1 0 542517928 55910400 11517 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13650 11517 603 41 0 13609 0
vsize: 54600
[startup+119.999 s]
Raw data (loadavg): 0.94 0.93 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 43457 0 0 0 11855 141 0 0 25 0 1 0 542517928 56446976 11640 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13781 11640 603 41 0 13740 0
vsize: 55124
[startup+129.999 s]
Raw data (loadavg): 0.95 0.93 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 46865 0 0 0 12844 152 0 0 25 0 1 0 542517928 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+139.999 s]
Raw data (loadavg): 0.96 0.93 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 49420 0 0 0 13833 162 0 0 25 0 1 0 542517928 57225216 11872 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13971 11872 603 41 0 13930 0
vsize: 55884
[startup+149.999 s]
Raw data (loadavg): 0.96 0.93 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 49420 0 0 0 14834 162 0 0 25 0 1 0 542517928 57225216 11872 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13971 11872 603 41 0 13930 0
vsize: 55884
[startup+159.999 s]
Raw data (loadavg): 0.97 0.94 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 49478 0 0 0 15833 162 0 0 25 0 1 0 542517928 57487360 11930 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14035 11930 603 41 0 13994 0
vsize: 56140
[startup+169.999 s]
Raw data (loadavg): 0.97 0.94 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 49691 0 0 0 16833 163 0 0 25 0 1 0 542517928 58417152 12143 4294967295 134512640 134672761 3221224544 3221223648 134604309 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14262 12143 603 41 0 14221 0
vsize: 57048
[startup+179.999 s]
Raw data (loadavg): 0.98 0.94 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 50186 0 0 0 17833 164 0 0 25 0 1 0 542517928 60473344 12638 4294967295 134512640 134672761 3221224544 3221223692 134614482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14764 12638 603 41 0 14723 0
vsize: 59056
[startup+190 s]
Raw data (loadavg): 0.98 0.94 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 50559 0 0 0 18832 164 0 0 25 0 1 0 542517928 61890560 13011 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15110 13011 603 41 0 15069 0
vsize: 60440
[startup+199.999 s]
Raw data (loadavg): 0.98 0.94 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 51380 0 0 0 19830 166 0 0 25 0 1 0 542517928 65310720 13832 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15945 13832 603 41 0 15904 0
vsize: 63780
[startup+210 s]
Raw data (loadavg): 0.98 0.94 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 51844 0 0 0 20829 168 0 0 25 0 1 0 542517928 67149824 14296 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16394 14296 603 41 0 16353 0
vsize: 65576
[startup+220 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 52840 0 0 0 21828 169 0 0 25 0 1 0 542517928 71331840 15292 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17415 15292 603 41 0 17374 0
vsize: 69660
[startup+230 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 53572 0 0 0 22826 172 0 0 25 0 1 0 542517928 74317824 16024 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18144 16024 603 41 0 18103 0
vsize: 72576
[startup+240 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 54589 0 0 0 23823 174 0 0 25 0 1 0 542517928 78512128 17041 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19168 17041 603 41 0 19127 0
vsize: 76672
[startup+249.999 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 56164 0 0 0 24820 177 0 0 25 0 1 0 542517928 84955136 18616 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20741 18616 603 41 0 20700 0
vsize: 82964
[startup+260 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 59596 0 0 0 25811 186 0 0 25 0 1 0 542517928 87326720 19230 4294967295 134512640 134672761 3221224544 3221223680 134614800 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 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 59929 0 0 0 26810 187 0 0 25 0 1 0 542517928 88748032 19563 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21667 19563 603 41 0 21626 0
vsize: 86668
[startup+280 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 60614 0 0 0 27809 188 0 0 25 0 1 0 542517928 91598848 20248 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22363 20248 603 41 0 22322 0
vsize: 89452
[startup+290.001 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 60708 0 0 0 28809 189 0 0 25 0 1 0 542517928 91983872 20342 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22457 20342 603 41 0 22416 0
vsize: 89828
[startup+300 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 63697 0 0 0 29800 197 0 0 25 0 1 0 542517928 92684288 20538 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22628 20538 603 41 0 22587 0
vsize: 90512
[startup+310 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 63838 0 0 0 30800 198 0 0 25 0 1 0 542517928 93347840 20679 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22790 20679 603 41 0 22749 0
vsize: 91160
[startup+320 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 64018 0 0 0 31800 198 0 0 25 0 1 0 542517928 94126080 20859 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22980 20859 603 41 0 22939 0
vsize: 91920
[startup+330.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 64693 0 0 0 32799 199 0 0 25 0 1 0 542517928 96976896 21534 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23676 21534 603 41 0 23635 0
vsize: 94704
[startup+340.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 65241 0 0 0 33799 200 0 0 25 0 1 0 542517928 99180544 22082 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24214 22082 603 41 0 24173 0
vsize: 96856
[startup+350 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 65401 0 0 0 34798 200 0 0 25 0 1 0 542517928 99840000 22242 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24375 22242 603 41 0 24334 0
vsize: 97500
[startup+360.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 65627 0 0 0 35798 201 0 0 25 0 1 0 542517928 100765696 22468 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24601 22468 603 41 0 24560 0
vsize: 98404
[startup+370.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 66578 0 0 0 36796 203 0 0 25 0 1 0 542517928 104660992 23419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25552 23419 603 41 0 25511 0
vsize: 102208
[startup+380.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 67162 0 0 0 37795 204 0 0 25 0 1 0 542517928 107032576 24003 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26131 24003 603 41 0 26090 0
vsize: 104524
[startup+390.002 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 67630 0 0 0 38794 205 0 0 25 0 1 0 542517928 109006848 24471 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26613 24471 603 41 0 26572 0
vsize: 106452
[startup+400.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 68451 0 0 0 39792 208 0 0 25 0 1 0 542517928 112369664 25292 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27434 25292 603 41 0 27393 0
vsize: 109736
[startup+410.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 68905 0 0 0 40791 209 0 0 25 0 1 0 542517928 114188288 25746 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27878 25746 603 41 0 27837 0
vsize: 111512
[startup+420.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 69532 0 0 0 41791 210 0 0 25 0 1 0 542517928 116707328 26373 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28493 26373 603 41 0 28452 0
vsize: 113972
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 69886 0 0 0 42790 211 0 0 25 0 1 0 542517928 118140928 26727 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28843 26727 603 41 0 28802 0
vsize: 115372
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 72377 0 0 0 43782 219 0 0 25 0 1 0 542517928 133541888 29060 4294967295 134512640 134672761 3221224544 3221222808 1075730078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32603 29060 603 41 0 32562 0
vsize: 130412
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73563 0 0 0 44776 224 0 0 25 0 1 0 542517928 119689216 27112 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73563 0 0 0 45777 224 0 0 25 0 1 0 542517928 119689216 27112 4294967295 134512640 134672761 3221224544 3221223744 134610622 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73563 0 0 0 46777 224 0 0 25 0 1 0 542517928 119689216 27112 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73563 0 0 0 47777 224 0 0 25 0 1 0 542517928 119689216 27112 4294967295 134512640 134672761 3221224544 3221223728 134615739 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73564 0 0 0 48777 224 0 0 25 0 1 0 542517928 119689216 27113 4294967295 134512640 134672761 3221224544 3221223584 134612972 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73566 0 0 0 49777 224 0 0 25 0 1 0 542517928 119689216 27115 4294967295 134512640 134672761 3221224544 3221223680 134614701 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73567 0 0 0 50777 224 0 0 25 0 1 0 542517928 119689216 27116 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73568 0 0 0 51778 224 0 0 25 0 1 0 542517928 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73569 0 0 0 52778 224 0 0 25 0 1 0 542517928 119689216 27118 4294967295 134512640 134672761 3221224544 3221223584 134612684 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73570 0 0 0 53778 224 0 0 25 0 1 0 542517928 119689216 27119 4294967295 134512640 134672761 3221224544 3221223728 134615916 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73571 0 0 0 54778 224 0 0 25 0 1 0 542517928 119689216 27120 4294967295 134512640 134672761 3221224544 3221223680 134614753 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 73573 0 0 0 55778 224 0 0 25 0 1 0 542517928 119689216 27122 4294967295 134512640 134672761 3221224544 3221223728 134615833 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 74161 0 0 0 56777 226 0 0 25 0 1 0 542517928 122093568 27710 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29808 27710 603 41 0 29767 0
vsize: 119232
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 74782 0 0 0 57776 227 0 0 25 0 1 0 542517928 124678144 28331 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30439 28331 603 41 0 30398 0
vsize: 121756
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 75426 0 0 0 58775 228 0 0 25 0 1 0 542517928 127295488 28975 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31078 28975 603 41 0 31037 0
vsize: 124312
[startup+600.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 75678 0 0 0 59774 228 0 0 25 0 1 0 542517928 128344064 29227 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31334 29227 603 41 0 31293 0
vsize: 125336
[startup+610.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 75997 0 0 0 60774 229 0 0 25 0 1 0 542517928 129679360 29546 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31660 29546 603 41 0 31619 0
vsize: 126640
[startup+620.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 76464 0 0 0 61772 231 0 0 25 0 1 0 542517928 131637248 30013 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32138 30013 603 41 0 32097 0
vsize: 128552
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 77042 0 0 0 62771 232 0 0 25 0 1 0 542517928 133943296 30591 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32701 30591 603 41 0 32660 0
vsize: 130804
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 77699 0 0 0 63770 233 0 0 25 0 1 0 542517928 136642560 31248 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33360 31248 603 41 0 33319 0
vsize: 133440
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 78187 0 0 0 64769 235 0 0 25 0 1 0 542517928 138854400 31736 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33900 31736 603 41 0 33859 0
vsize: 135600
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 79032 0 0 0 65767 237 0 0 25 0 1 0 542517928 142389248 32581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34763 32581 603 41 0 34722 0
vsize: 139052
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 81027 0 0 0 66763 241 0 0 25 0 1 0 542517928 150450176 34576 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36731 34576 603 41 0 36690 0
vsize: 146924
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 83125 0 0 0 67759 246 0 0 25 0 1 0 542517928 161067008 36674 4294967295 134512640 134672761 3221224544 3221222960 134609159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39323 36674 603 41 0 39282 0
vsize: 157292
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 84593 0 0 0 68752 251 0 0 25 0 1 0 542517928 153923584 35426 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37579 35426 603 41 0 37538 0
vsize: 150316
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 84594 0 0 0 69752 251 0 0 25 0 1 0 542517928 153923584 35427 4294967295 134512640 134672761 3221224544 3221223728 134615948 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 84594 0 0 0 70753 251 0 0 25 0 1 0 542517928 153923584 35427 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86722 0 0 0 71745 259 0 0 25 0 1 0 542517928 153636864 35359 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35359 603 41 0 37468 0
vsize: 150036
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86722 0 0 0 72745 259 0 0 25 0 1 0 542517928 153636864 35359 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 35359 603 41 0 37468 0
vsize: 150036
[startup+740.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86724 0 0 0 73745 259 0 0 25 0 1 0 542517928 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+750.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86724 0 0 0 74745 259 0 0 25 0 1 0 542517928 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615755 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86724 0 0 0 75746 259 0 0 25 0 1 0 542517928 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615807 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86724 0 0 0 76746 259 0 0 25 0 1 0 542517928 153636864 35361 4294967295 134512640 134672761 3221224544 3221223584 134614228 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86724 0 0 0 77746 259 0 0 25 0 1 0 542517928 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86724 0 0 0 78746 259 0 0 25 0 1 0 542517928 153636864 35361 4294967295 134512640 134672761 3221224544 3221223728 134615828 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86724 0 0 0 79746 259 0 0 25 0 1 0 542517928 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+810.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86724 0 0 0 80747 259 0 0 25 0 1 0 542517928 153636864 35361 4294967295 134512640 134672761 3221224544 3221223688 134616108 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86725 0 0 0 81747 259 0 0 25 0 1 0 542517928 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86726 0 0 0 82747 259 0 0 25 0 1 0 542517928 153636864 35363 4294967295 134512640 134672761 3221224544 3221223728 134615665 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86727 0 0 0 83747 259 0 0 25 0 1 0 542517928 153636864 35364 4294967295 134512640 134672761 3221224544 3221223728 134615619 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86727 0 0 0 84747 259 0 0 25 0 1 0 542517928 153636864 35364 4294967295 134512640 134672761 3221224544 3221223744 134610707 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 86728 0 0 0 85747 259 0 0 25 0 1 0 542517928 153636864 35365 4294967295 134512640 134672761 3221224544 3221223728 134615732 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 87202 0 0 0 86746 260 0 0 25 0 1 0 542517928 155652096 35839 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38001 35839 603 41 0 37960 0
vsize: 152004
[startup+880.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 88085 0 0 0 87745 262 0 0 25 0 1 0 542517928 159256576 36722 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38881 36722 603 41 0 38840 0
vsize: 155524
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 88704 0 0 0 88743 264 0 0 25 0 1 0 542517928 161742848 37341 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39488 37341 603 41 0 39447 0
vsize: 157952
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 89454 0 0 0 89742 265 0 0 25 0 1 0 542517928 164818944 38091 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40239 38091 603 41 0 40198 0
vsize: 160956
[startup+910.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 90220 0 0 0 90741 267 0 0 25 0 1 0 542517928 168042496 38857 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41026 38857 603 41 0 40985 0
vsize: 164104
[startup+920.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 90882 0 0 0 91739 269 0 0 25 0 1 0 542517928 170721280 39519 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41680 39519 603 41 0 41639 0
vsize: 166720
[startup+930.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 92058 0 0 0 92737 271 0 0 25 0 1 0 542517928 175480832 40695 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42842 40695 603 41 0 42801 0
vsize: 171368
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 92889 0 0 0 93736 272 0 0 25 0 1 0 542517928 178847744 41526 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43664 41526 603 41 0 43623 0
vsize: 174656
[startup+950.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 93669 0 0 0 94734 274 0 0 25 0 1 0 542517928 182091776 42306 4294967295 134512640 134672761 3221224544 3221223584 134603545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44456 42306 603 41 0 44415 0
vsize: 177824
[startup+960.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 94600 0 0 0 95733 276 0 0 25 0 1 0 542517928 185888768 43237 4294967295 134512640 134672761 3221224544 3221223688 134616339 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45383 43237 603 41 0 45342 0
vsize: 181532
[startup+970.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 94777 0 0 0 96733 276 0 0 25 0 1 0 542517928 186646528 43414 4294967295 134512640 134672761 3221224544 3221223680 134614513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45568 43414 603 41 0 45527 0
vsize: 182272
[startup+980.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 95424 0 0 0 97731 278 0 0 25 0 1 0 542517928 189345792 44061 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46227 44061 603 41 0 46186 0
vsize: 184908
[startup+990.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 96623 0 0 0 98729 280 0 0 25 0 1 0 542517928 194215936 45260 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47416 45260 603 41 0 47375 0
vsize: 189664
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 97484 0 0 0 99727 282 0 0 25 0 1 0 542517928 197705728 46121 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48268 46121 603 41 0 48227 0
vsize: 193072
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 97755 0 0 0 100727 283 0 0 25 0 1 0 542517928 198868992 46392 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48552 46392 603 41 0 48511 0
vsize: 194208
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 98141 0 0 0 101726 283 0 0 25 0 1 0 542517928 200421376 46778 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48931 46778 603 41 0 48890 0
vsize: 195724
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 98641 0 0 0 102725 285 0 0 25 0 1 0 542517928 202440704 47278 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49424 47278 603 41 0 49383 0
vsize: 197696
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 99193 0 0 0 103724 286 0 0 25 0 1 0 542517928 204767232 47830 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49992 47830 603 41 0 49951 0
vsize: 199968
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 99799 0 0 0 104723 287 0 0 25 0 1 0 542517928 207187968 48436 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50583 48436 603 41 0 50542 0
vsize: 202332
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 100520 0 0 0 105722 289 0 0 25 0 1 0 542517928 210202624 49157 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51319 49157 603 41 0 51278 0
vsize: 205276
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 101410 0 0 0 106721 290 0 0 25 0 1 0 542517928 213864448 50047 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52213 50047 603 41 0 52172 0
vsize: 208852
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 102320 0 0 0 107719 292 0 0 25 0 1 0 542517928 217481216 50957 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53096 50957 603 41 0 53055 0
vsize: 212384
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 103360 0 0 0 108717 294 0 0 25 0 1 0 542517928 221818880 51997 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54155 51997 603 41 0 54114 0
vsize: 216620
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 104027 0 0 0 109716 295 0 0 25 0 1 0 542517928 224530432 52664 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54817 52664 603 41 0 54776 0
vsize: 219268
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 104696 0 0 0 110714 297 0 0 25 0 1 0 542517928 227237888 53333 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55478 53333 603 41 0 55437 0
vsize: 221912
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 105197 0 0 0 111714 298 0 0 25 0 1 0 542517928 229339136 53834 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55991 53834 603 41 0 55950 0
vsize: 223964
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 106157 0 0 0 112712 300 0 0 25 0 1 0 542517928 233291776 54794 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56956 54794 603 41 0 56915 0
vsize: 227824
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 107505 0 0 0 113710 302 0 0 25 0 1 0 542517928 238714880 56142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58280 56142 603 41 0 58239 0
vsize: 233120
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 108880 0 0 0 114706 306 0 0 25 0 1 0 542517928 244453376 57517 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59681 57517 603 41 0 59640 0
vsize: 238724
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 109928 0 0 0 115704 309 0 0 25 0 1 0 542517928 248680448 58565 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60713 58565 603 41 0 60672 0
vsize: 242852
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 110742 0 0 0 116701 311 0 0 25 0 1 0 542517928 252010496 59379 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61526 59379 603 41 0 61485 0
vsize: 246104
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 111763 0 0 0 117699 314 0 0 25 0 1 0 542517928 256245760 60400 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62560 60400 603 41 0 62519 0
vsize: 250240
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 112876 0 0 0 118696 316 0 0 25 0 1 0 542517928 260751360 61513 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63660 61513 603 41 0 63619 0
vsize: 254640
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29832
Raw data (stat): 29832 (minisat+) R 29831 28099 28098 0 -1 0 113959 0 0 0 119694 319 0 0 25 0 1 0 542517928 265248768 62596 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64758 62596 603 41 0 64717 0
vsize: 259032
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 29832
Raw data (stat): 29832 (minisat+) Z 29831 28099 28098 0 -1 12 113960 0 0 0 119694 332 0 0 25 0 1 0 542517928 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.13
CPU time (s): 1200.27
CPU user time (s): 1196.94
CPU system time (s): 3.32349
CPU usage (%): 100.011
Max. virtual memory (Kb): 259032
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####