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/submitted/een/normalized-p0282.opb
MD5SUM	dd62132555621025f45a5a6099c90742
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	258411
Optimality of the best value was proved	NO
Number of terms in the objective function	282
Biggest coefficient in the objective function	160646
Number of bits for the biggest coefficient in the objective function	18
Sum of the numbers in the objective function	1302615
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	160646
Number of bits of the biggest number in a constraint	18
Biggest sum of numbers in a constraint	1302615
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	282
Total number of constraints	221
Number of constraints which are clauses	177
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	44
Minimum length of a constraint	2
Maximum length of a constraint	57
Trace number 6998

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 20:51:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5055 boxname=wulflinc24 idbench=389 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dd62132555621025f45a5a6099c90742  /oldhome/oroussel/tmp/wulflinc24/normalized-p0282.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc24/normalized-p0282.opb /oldhome/oroussel/tmp/wulflinc24/normalized-p0282.opb
IDLAUNCH: 5055
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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.080
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:        816204 kB
Buffers:         35740 kB
Cached:         140292 kB
SwapCached:       3828 kB
Active:          65116 kB
Inactive:       117564 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        815952 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30232 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:11:13 (client local time) WITH STATUS 10 IN 1200.09 SECONDS
stats: 5055 7 1200.09 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................sss
c ---[  46]---> BDD-cost:    4
c ---[  45]---> BDD-cost:    8
c ---[  44]---> BDD-cost:   10
c ---[  43]---> BDD-cost:   16
c ---[  42]---> Sorter-cost: 1109     Base: 2 5 3 3
c ---[  41]---> Sorter-cost:  898     Base: 2 5 3 2
c ---[  40]---> Sorter-cost: 1118     Base: 2 5 5
c ---[  38]---> Sorter-cost: 1011     Base: 2 5 5
c ---[  37]---> Sorter-cost:  910     Base: 2 5 5
c ---[  36]---> Sorter-cost:  998     Base: 2 5 3 2
c ---[  35]---> Sorter-cost:  852     Base: 2 5 3 3
c ---[  34]---> Sorter-cost:  843     Base: 5 2 3 3
c ---[  33]---> Sorter-cost:  713     Base: 5 2 3 3
c ---[  32]---> Sorter-cost:  948     Base: 2 5 3 3
c ---[  31]---> Sorter-cost:  843     Base: 2 5 3 3
c ---[  30]---> Sorter-cost:  911     Base: 2 5 5
c ---[  29]---> Sorter-cost:  935     Base: 2 5 3 2
c ---[  28]---> Sorter-cost:  998     Base: 2 5 3
c ---[  27]---> Sorter-cost:  763     Base: 5 2 3 3
c ---[  26]---> Sorter-cost:  909     Base: 2 5 5
c ---[  25]---> Sorter-cost:  907     Base: 2 5 5
c ---[  24]---> Sorter-cost:  714     Base: 5 2 3 3
c ---[  23]---> Sorter-cost:  909     Base: 2 5 5
c ---[  22]---> Sorter-cost:  909     Base: 2 5 5
c ---[  21]---> Sorter-cost: 1008     Base: 2 5 3
c ---[  20]---> Sorter-cost:  898     Base: 2 5 3 3
c ---[  19]---> Sorter-cost:  843     Base: 2 5 3 3
c ---[  18]---> Sorter-cost:  761     Base: 2 5 3 3
c ---[  17]---> Sorter-cost:  714     Base: 5 2 3 3
c ---[  16]---> Sorter-cost: 1071     Base: 2 5 3 3
c ---[  15]---> Sorter-cost:  949     Base: 2 5 3 3
c ---[  14]---> BDD-cost:   26
c ---[  13]---> Sorter-cost: 1108     Base: 2 5 3 3
c ---[  11]---> Sorter-cost: 1081     Base: 2 5 3 3
c ---[  10]---> Sorter-cost:  999     Base: 2 5 3 2
c ---[   9]---> Sorter-cost:  995     Base: 2 5 3 3
c ---[   8]---> Sorter-cost:  982     Base: 2 5 3 2
c ---[   7]---> Sorter-cost:  996     Base: 2 5 3 3
c ---[   5]---> BDD-cost:   56
c ---[   4]---> BDD-cost:   56
c ---[   3]---> BDD-cost:   56
c ---[   2]---> BDD-cost:   12
c ---[   1]---> Sorter-cost:  719     Base: 2 5 3
c ---[   0]---> Sorter-cost:  657     Base: 2 5 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   70313   165043 |   21093       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/25276          
c   -- var.elim.:  2000/25276          
c   -- var.elim.:  3000/25276          
c   -- var.elim.:  4000/25276          
c   -- var.elim.:  5000/25276          
c   -- var.elim.:  6000/25276          
c   -- var.elim.:  7000/25276          
c   -- var.elim.:  8000/25276          
c   -- var.elim.:  9000/25276          
c   -- var.elim.:  10000/25276          
c   -- var.elim.:  11000/25276          
c   -- var.elim.:  12000/25276          
c   -- var.elim.:  13000/25276          
c   -- var.elim.:  14000/25276          
c   -- var.elim.:  15000/25276          
c   -- var.elim.:  16000/25276          
c   -- var.elim.:  17000/25276          
c   -- var.elim.:  18000/25276          
c   -- var.elim.:  19000/25276          
c   -- var.elim.:  20000/25276          
c   -- var.elim.:  21000/25276          
c   -- var.elim.:  22000/25276          
c   -- var.elim.:  23000/25276          
c   -- var.elim.:  24000/25276          
c   -- var.elim.:  25000/25276          
c   -- var.elim.:  25276/25276          
c   -- var.elim.:  1000/13115          
c   -- var.elim.:  2000/13115          
c   -- var.elim.:  3000/13115          
c   -- var.elim.:  4000/13115          
c   -- var.elim.:  5000/13115          
c   -- var.elim.:  6000/13115          
c   -- var.elim.:  7000/13115          
c   -- var.elim.:  8000/13115          
c   -- var.elim.:  9000/13115          
c   -- var.elim.:  10000/13115          
c   -- var.elim.:  11000/13115          
c   -- var.elim.:  12000/13115          
c   -- var.elim.:  13000/13115          
c   -- var.elim.:  13115/13115          
c   -- var.elim.:  860/860          
c   -- var.elim.:  41/41          
c   -- var.elim.:  30/30          
c   -- subsuming                       
c   -- var.elim.:  1000/4027          
c   -- var.elim.:  2000/4027          
c   -- var.elim.:  3000/4027          
c   -- var.elim.:  4000/4027          
c   -- var.elim.:  4027/4027          
c   -- var.elim.:  1000/1605          
c   -- var.elim.:  1605/1605          
c   -- var.elim.:  191/191          
c   -- var.elim.:  37/37          
c   -- subsuming                       
c   -- var.elim.:  544/544          
c   -- var.elim.:  161/161          
c |         0 |   57220   179867 |      --       0       --      -- |     --   | -13093/14868
c |         0 |   57220   179867 |   22888       0        0     nan |  0.000 % |
c |       101 |   57080   179268 |   25115      98      797     8.1 |  3.198 % |
c ==============================================================================
c (current CPU-time: 4.65329 s)
c ==============================================================================
c [1mFound solution: 639120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:77309     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       170 |  275356   689257 |   82606     167     1632     9.8 |  3.198 % |
c   -- subsuming                       
c   -- var.elim.:  1000/74100          
c   -- var.elim.:  2000/74100          
c   -- var.elim.:  3000/74100          
c   -- var.elim.:  4000/74100          
c   -- var.elim.:  5000/74100          
c   -- var.elim.:  6000/74100          
c   -- var.elim.:  7000/74100          
c   -- var.elim.:  8000/74100          
c   -- var.elim.:  9000/74100          
c   -- var.elim.:  10000/74100          
c   -- var.elim.:  11000/74100          
c   -- var.elim.:  12000/74100          
c   -- var.elim.:  13000/74100          
c   -- var.elim.:  14000/74100          
c   -- var.elim.:  15000/74100          
c   -- var.elim.:  16000/74100          
c   -- var.elim.:  17000/74100          
c   -- var.elim.:  18000/74100          
c   -- var.elim.:  19000/74100          
c   -- var.elim.:  20000/74100          
c   -- var.elim.:  21000/74100          
c   -- var.elim.:  22000/74100          
c   -- var.elim.:  23000/74100          
c   -- var.elim.:  24000/74100          
c   -- var.elim.:  25000/74100          
c   -- var.elim.:  26000/74100          
c   -- var.elim.:  27000/74100          
c   -- var.elim.:  28000/74100          
c   -- var.elim.:  29000/74100          
c   -- var.elim.:  30000/74100          
c   -- var.elim.:  31000/74100          
c   -- var.elim.:  32000/74100          
c   -- var.elim.:  33000/74100          
c   -- var.elim.:  34000/74100          
c   -- var.elim.:  35000/74100          
c   -- var.elim.:  36000/74100          
c   -- var.elim.:  37000/74100          
c   -- var.elim.:  38000/74100          
c   -- var.elim.:  39000/74100          
c   -- var.elim.:  40000/74100          
c   -- var.elim.:  41000/74100          
c   -- var.elim.:  42000/74100          
c   -- var.elim.:  43000/74100          
c   -- var.elim.:  44000/74100          
c   -- var.elim.:  45000/74100          
c   -- var.elim.:  46000/74100          
c   -- var.elim.:  47000/74100          
c   -- var.elim.:  48000/74100          
c   -- var.elim.:  49000/74100          
c   -- var.elim.:  50000/74100          
c   -- var.elim.:  51000/74100          
c   -- var.elim.:  52000/74100          
c   -- var.elim.:  53000/74100          
c   -- var.elim.:  54000/74100          
c   -- var.elim.:  55000/74100          
c   -- var.elim.:  56000/74100          
c   -- var.elim.:  57000/74100          
c   -- var.elim.:  58000/74100          
c   -- var.elim.:  59000/74100          
c   -- var.elim.:  60000/74100          
c   -- var.elim.:  61000/74100          
c   -- var.elim.:  62000/74100          
c   -- var.elim.:  63000/74100          
c   -- var.elim.:  64000/74100          
c   -- var.elim.:  65000/74100          
c   -- var.elim.:  66000/74100          
c   -- var.elim.:  67000/74100          
c   -- var.elim.:  68000/74100          
c   -- var.elim.:  69000/74100          
c   -- var.elim.:  70000/74100          
c   -- var.elim.:  71000/74100          
c   -- var.elim.:  72000/74100          
c   -- var.elim.:  73000/74100          
c   -- var.elim.:  74000/74100          
c   -- var.elim.:  74100/74100          
c   -- var.elim.:  1000/40523          
c   -- var.elim.:  2000/40523          
c   -- var.elim.:  3000/40523          
c   -- var.elim.:  4000/40523          
c   -- var.elim.:  5000/40523          
c   -- var.elim.:  6000/40523          
c   -- var.elim.:  7000/40523          
c   -- var.elim.:  8000/40523          
c   -- var.elim.:  9000/40523          
c   -- var.elim.:  10000/40523          
c   -- var.elim.:  11000/40523          
c   -- var.elim.:  12000/40523          
c   -- var.elim.:  13000/40523          
c   -- var.elim.:  14000/40523          
c   -- var.elim.:  15000/40523          
c   -- var.elim.:  16000/40523          
c   -- var.elim.:  17000/40523          
c   -- var.elim.:  18000/40523          
c   -- var.elim.:  19000/40523          
c   -- var.elim.:  20000/40523          
c   -- var.elim.:  21000/40523          
c   -- var.elim.:  22000/40523          
c   -- var.elim.:  23000/40523          
c   -- var.elim.:  24000/40523          
c   -- var.elim.:  25000/40523          
c   -- var.elim.:  26000/40523          
c   -- var.elim.:  27000/40523          
c   -- var.elim.:  28000/40523          
c   -- var.elim.:  29000/40523          
c   -- var.elim.:  30000/40523          
c   -- var.elim.:  31000/40523          
c   -- var.elim.:  32000/40523          
c   -- var.elim.:  33000/40523          
c   -- var.elim.:  34000/40523          
c   -- var.elim.:  35000/40523          
c   -- var.elim.:  36000/40523          
c   -- var.elim.:  37000/40523          
c   -- var.elim.:  38000/40523          
c   -- var.elim.:  39000/40523          
c   -- var.elim.:  40000/40523          
c   -- var.elim.:  40523/40523          
c   -- var.elim.:  98/98          
c   -- subsuming                       
c   -- var.elim.:  1000/1628          
c   -- var.elim.:  1628/1628          
c   -- var.elim.:  531/531          
c   -- var.elim.:  24/24          
c   -- var.elim.:  18/18          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  169/169          
c   -- var.elim.:  14/14          
c |       170 |  256665   794086 |      --     167       --      -- |     --   | -18691/104830
c |       170 |  256665   794086 |  102666     161     1539     9.6 |  3.198 % |
c ==============================================================================
c (current CPU-time: 18.5852 s)
c ==============================================================================
c [1mFound solution: 633392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       241 |  260868   804891 |   78260     231     3084    13.4 |  3.198 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5889          
c   -- var.elim.:  2000/5889          
c   -- var.elim.:  3000/5889          
c   -- var.elim.:  4000/5889          
c   -- var.elim.:  5000/5889          
c   -- var.elim.:  5889/5889          
c   -- var.elim.:  1000/3158          
c   -- var.elim.:  2000/3158          
c   -- var.elim.:  3000/3158          
c   -- var.elim.:  3158/3158          
c   -- subsuming                       
c   -- var.elim.:  23/23          
c |       241 |  258563   803532 |      --     231       --      -- |     --   | -2305/-1358
c |       241 |  258563   803532 |  103425     231     3084    13.4 |  3.198 % |
c |       341 |  258563   803532 |  113767     331     3781    11.4 |  0.781 % |
c |       491 |  258563   803532 |  125144     481     5075    10.6 |  0.781 % |
c ==============================================================================
c (current CPU-time: 22.6066 s)
c ==============================================================================
c [1mFound solution: 559905[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       556 |  259386   806547 |   77815     546     8689    15.9 |  0.781 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2052          
c   -- var.elim.:  2000/2052          
c   -- var.elim.:  2052/2052          
c   -- var.elim.:  1000/1507          
c   -- var.elim.:  1507/1507          
c   -- subsuming                       
c   -- var.elim.:  777/777          
c   -- var.elim.:  84/84          
c |       556 |  258919   810464 |      --     546       --      -- |     --   | -467/3918
c |       556 |  258919   810464 |  103567     546     8689    15.9 |  0.781 % |
c |       656 |  258919   810464 |  113924     646     9246    14.3 |  0.781 % |
c |       806 |  258919   810464 |  125316     796    12209    15.3 |  0.781 % |
c |      1031 |  258829   810079 |  137800     996    16638    16.7 |  0.800 % |
c |      1368 |  258829   810079 |  151580    1333    34783    26.1 |  0.800 % |
c |      1874 |  258829   810079 |  166738    1839    51277    27.9 |  0.800 % |
c ==============================================================================
c (current CPU-time: 32.0201 s)
c ==============================================================================
c [1mFound solution: 559359[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2185 |  259843   813461 |   77952    2150    85964    40.0 |  0.800 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2307          
c   -- var.elim.:  2000/2307          
c   -- var.elim.:  2307/2307          
c   -- var.elim.:  1000/1655          
c   -- var.elim.:  1655/1655          
c   -- var.elim.:  15/15          
c   -- subsuming                       
c   -- var.elim.:  888/888          
c   -- var.elim.:  193/193          
c |      2185 |  259251   816828 |      --    2150       --      -- |     --   | -592/3368
c |      2185 |  259251   816828 |  103700    2075    69918    33.7 |  0.800 % |
c |      2286 |  259251   816828 |  114070    2176    74346    34.2 |  0.800 % |
c |      2437 |  259251   816828 |  125477    2327    76283    32.8 |  0.800 % |
c |      2662 |  259251   816828 |  138025    2552    77985    30.6 |  0.800 % |
c |      3000 |  259251   816828 |  151827    2890   120441    41.7 |  0.800 % |
c |      3507 |  259251   816828 |  167010    3397   153863    45.3 |  0.800 % |
c |      4266 |  259210   816676 |  183682    4152   168080    40.5 |  0.810 % |
c |      5406 |  259210   816676 |  202050    5292   242386    45.8 |  0.810 % |
c |      7115 |  259210   816676 |  222255    7001   315842    45.1 |  0.810 % |
c |      9678 |  259140   816105 |  244415    9563   523130    54.7 |  0.823 % |
c |     13522 |  258984   815254 |  268695   13400   809326    60.4 |  0.858 % |
c ==============================================================================
c (current CPU-time: 62.0116 s)
c ==============================================================================
c [1mFound solution: 559358[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13762 |  258933   815616 |   77679   13635   836858    61.4 |  0.858 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1738          
c   -- var.elim.:  1738/1738          
c   -- var.elim.:  1000/1650          
c   -- var.elim.:  1650/1650          
c   -- var.elim.:  1000/1221          
c   -- var.elim.:  1221/1221          
c   -- var.elim.:  832/832          
c   -- subsuming                       
c   -- var.elim.:  215/215          
c   -- var.elim.:  83/83          
c |     13762 |  258504   813601 |      --   13635       --      -- |     --   | -429/-2014
c |     13762 |  258504   813601 |  103401   13175   654347    49.7 |  0.858 % |
c |     13862 |  258504   813601 |  113741   13275   656072    49.4 |  0.916 % |
c |     14012 |  258504   813601 |  125115   13425   656970    48.9 |  0.916 % |
c |     14237 |  258504   813601 |  137627   13650   658847    48.3 |  0.916 % |
c ==============================================================================
c (current CPU-time: 68.6946 s)
c ==============================================================================
c [1mFound solution: 548826[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14506 |  258887   814405 |   77666   13917   664597    47.8 |  0.916 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2579          
c   -- var.elim.:  2000/2579          
c   -- var.elim.:  2579/2579          
c   -- var.elim.:  1000/1684          
c   -- var.elim.:  1684/1684          
c   -- var.elim.:  642/642          
c   -- subsuming                       
c   -- var.elim.:  730/730          
c   -- var.elim.:  17/17          
c |     14506 |  258410   817503 |      --   13917       --      -- |     --   | -477/3099
c |     14506 |  258410   817503 |  103364   13894   660748    47.6 |  0.916 % |
c |     14609 |  258410   817503 |  113700   13997   661767    47.3 |  1.007 % |
c |     14760 |  258410   817503 |  125070   14148   662584    46.8 |  1.007 % |
c |     14985 |  258392   817446 |  137567   14372   665916    46.3 |  1.011 % |
c |     15322 |  258392   817446 |  151324   14709   713455    48.5 |  1.011 % |
c |     15829 |  258290   814878 |  166391   15212   720635    47.4 |  1.028 % |
c |     16588 |  258290   814878 |  183030   15971   737453    46.2 |  1.028 % |
c |     17727 |  258239   814700 |  201293   17106   790873    46.2 |  1.039 % |
c |     19436 |  258201   814561 |  221390   18812   863384    45.9 |  1.050 % |
c ==============================================================================
c (current CPU-time: 88.6435 s)
c ==============================================================================
c [1mFound solution: 547371[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19537 |  258289   815593 |   77486   18913   868626    45.9 |  1.050 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1259          
c   -- var.elim.:  1259/1259          
c   -- var.elim.:  1000/1059          
c   -- var.elim.:  1059/1059          
c   -- var.elim.:  782/782          
c   -- subsuming                       
c   -- var.elim.:  41/41          
c   -- var.elim.:  12/12          
c |     19537 |  258189   817136 |      --   18913       --      -- |     --   | -100/1544
c |     19537 |  258189   817136 |  103275   18699   785952    42.0 |  1.050 % |
c |     19638 |  258189   817136 |  113603   18800   787339    41.9 |  1.052 % |
c |     19788 |  258189   817136 |  124963   18950   789071    41.6 |  1.052 % |
c |     20013 |  257988   815794 |  137352   19171   793393    41.4 |  1.090 % |
c |     20351 |  257988   815794 |  151088   19509   797565    40.9 |  1.090 % |
c |     20857 |  257988   815794 |  166196   20015   803913    40.2 |  1.090 % |
c |     21616 |  257988   815794 |  182816   20774   811589    39.1 |  1.090 % |
c |     22757 |  257925   815534 |  201049   21911   842691    38.5 |  1.099 % |
c ==============================================================================
c (current CPU-time: 101.777 s)
c ==============================================================================
c [1mFound solution: 515214[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23465 |  257864   814175 |   77359   22605   863989    38.2 |  1.099 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1794          
c   -- var.elim.:  1794/1794          
c   -- var.elim.:  1000/1485          
c   -- var.elim.:  1485/1485          
c   -- var.elim.:  21/21          
c   -- var.elim.:  255/255          
c   -- subsuming                       
c   -- var.elim.:  41/41          
c   -- var.elim.:  8/8          
c |     23465 |  257752   816201 |      --   22605       --      -- |     --   | -109/2033
c |     23465 |  257752   816201 |  103100   22264   819801    36.8 |  1.099 % |
c |     23565 |  257752   816201 |  113410   22364   821567    36.7 |  1.137 % |
c |     23716 |  257447   814695 |  124604   22512   843330    37.5 |  1.214 % |
c |     23946 |  257447   814695 |  137064   22742   858112    37.7 |  1.214 % |
c |     24286 |  257299   814082 |  150684   23065   860979    37.3 |  1.253 % |
c |     24792 |  257299   814082 |  165753   23571   892605    37.9 |  1.253 % |
c |     25553 |  257227   813399 |  182277   24327   950497    39.1 |  1.268 % |
c |     26692 |  257227   813399 |  200505   25466  1035916    40.7 |  1.268 % |
c |     28400 |  257180   813228 |  220515   27173  1381089    50.8 |  1.283 % |
c |     30962 |  257139   813064 |  242528   29731  1556310    52.3 |  1.291 % |
c |     34807 |  257139   813064 |  266780   33576  1790792    53.3 |  1.291 % |
c ==============================================================================
c (current CPU-time: 177.643 s)
c ==============================================================================
c [1mFound solution: 508002[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     36412 |  257237   814035 |   77171   35181  1875444    53.3 |  1.291 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2008          
c   -- var.elim.:  2000/2008          
c   -- var.elim.:  2008/2008          
c   -- var.elim.:  1000/1681          
c   -- var.elim.:  1681/1681          
c   -- var.elim.:  683/683          
c   -- var.elim.:  622/622          
c   -- var.elim.:  628/628          
c   -- subsuming                       
c   -- var.elim.:  993/993          
c   -- var.elim.:  10/10          
c |     36412 |  257112   816439 |      --   35181       --      -- |     --   | -123/2409
c |     36412 |  257112   816439 |  102844   34619  1614172    46.6 |  1.291 % |
c |     36512 |  257112   816439 |  113129   34719  1614945    46.5 |  1.297 % |
c |     36662 |  257112   816439 |  124442   34869  1617639    46.4 |  1.297 % |
c |     36888 |  257112   816439 |  136886   35095  1619918    46.2 |  1.297 % |
c |     37225 |  257112   816439 |  150575   35432  1634693    46.1 |  1.297 % |
c |     37732 |  256966   815910 |  165538   35930  1648993    45.9 |  1.337 % |
c ==============================================================================
c (current CPU-time: 188.979 s)
c ==============================================================================
c [1mFound solution: 507997[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38272 |  257066   816888 |   77119   36470  1674704    45.9 |  1.337 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1017          
c   -- var.elim.:  1017/1017          
c   -- var.elim.:  855/855          
c   -- var.elim.:  680/680          
c |     38272 |  256974   817547 |      --   36470       --      -- |     --   | -92/660
c |     38272 |  256974   817547 |  102789   36187  1557567    43.0 |  1.337 % |
c |     38372 |  256974   817547 |  113068   36287  1558338    42.9 |  1.338 % |
c |     38522 |  256974   817547 |  124375   36437  1565628    43.0 |  1.338 % |
c |     38747 |  256974   817547 |  136812   36662  1593661    43.5 |  1.338 % |
c |     39084 |  256974   817547 |  150494   36999  1611164    43.5 |  1.338 % |
c |     39590 |  256917   817334 |  165506   37504  1632785    43.5 |  1.355 % |
c ==============================================================================
c (current CPU-time: 203.563 s)
c ==============================================================================
c [1mFound solution: 468617[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     39958 |  257058   818600 |   77117   37872  1688598    44.6 |  1.355 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1317          
c   -- var.elim.:  1317/1317          
c   -- var.elim.:  1000/1065          
c   -- var.elim.:  1065/1065          
c   -- var.elim.:  556/556          
c   -- var.elim.:  633/633          
c |     39958 |  256947   820686 |      --   37872       --      -- |     --   | -111/2087
c |     39958 |  256947   820686 |  102778   37743  1671016    44.3 |  1.355 % |
c |     40059 |  256947   820686 |  113056   37844  1674941    44.3 |  1.359 % |
c |     40210 |  256947   820686 |  124362   37995  1675645    44.1 |  1.359 % |
c |     40439 |  256925   820617 |  136786   38222  1692068    44.3 |  1.365 % |
c |     40779 |  256925   820617 |  150465   38562  1695091    44.0 |  1.365 % |
c |     41289 |  256925   820617 |  165512   39072  1703412    43.6 |  1.365 % |
c |     42049 |  256859   820376 |  182016   39822  1713474    43.0 |  1.380 % |
c |     43188 |  256746   819931 |  200130   40955  1740844    42.5 |  1.404 % |
c |     44897 |  256625   819456 |  220039   42654  1781498    41.8 |  1.430 % |
c ==============================================================================
c (current CPU-time: 225.768 s)
c ==============================================================================
c [1mFound solution: 428842[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     46228 |  257823   822969 |   77346   43985  2002713    45.5 |  1.430 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3220          
c   -- var.elim.:  2000/3220          
c   -- var.elim.:  3000/3220          
c   -- var.elim.:  3220/3220          
c   -- var.elim.:  1000/2018          
c   -- var.elim.:  2000/2018          
c   -- var.elim.:  2018/2018          
c   -- var.elim.:  355/355          
c   -- var.elim.:  303/303          
c   -- subsuming                       
c   -- var.elim.:  369/369          
c |     46228 |  257113   823037 |      --   43985       --      -- |     --   | -704/81
c |     46228 |  257113   823037 |  102845   43083  1766774    41.0 |  1.430 % |
c |     46330 |  257113   823037 |  113129   43185  1770224    41.0 |  1.439 % |
c |     46482 |  257113   823037 |  124442   43337  1772700    40.9 |  1.439 % |
c |     46707 |  257113   823037 |  136886   43562  1779694    40.9 |  1.439 % |
c |     47044 |  257113   823037 |  150575   43899  1785013    40.7 |  1.439 % |
c |     47550 |  257094   822971 |  165620   44399  1794553    40.4 |  1.445 % |
c |     48310 |  257094   822971 |  182183   45159  1805976    40.0 |  1.445 % |
c |     49450 |  256951   822419 |  200289   46291  1835520    39.7 |  1.482 % |
c |     51161 |  256927   822332 |  220298   48001  1981523    41.3 |  1.492 % |
c ==============================================================================
c (current CPU-time: 250.194 s)
c ==============================================================================
c [1mFound solution: 428786[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     51265 |  257030   823456 |   77108   48105  1994040    41.5 |  1.492 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1369          
c   -- var.elim.:  1369/1369          
c   -- var.elim.:  1000/1514          
c   -- var.elim.:  1514/1514          
c   -- var.elim.:  759/759          
c   -- var.elim.:  707/707          
c   -- subsuming                       
c   -- var.elim.:  985/985          
c |     51265 |  256929   825634 |      --   48105       --      -- |     --   | -98/2185
c |     51265 |  256929   825634 |  102771   47753  1861386    39.0 |  1.492 % |
c |     51365 |  256929   825634 |  113048   47853  1862530    38.9 |  1.497 % |
c |     51520 |  256929   825634 |  124353   48008  1863412    38.8 |  1.497 % |
c |     51745 |  256929   825634 |  136788   48233  1890116    39.2 |  1.497 % |
c |     52082 |  256929   825634 |  150467   48570  1934255    39.8 |  1.497 % |
c |     52588 |  256929   825634 |  165514   49076  2096387    42.7 |  1.497 % |
c |     53347 |  256862   825369 |  182018   49833  2174701    43.6 |  1.516 % |
c |     54487 |  256793   825156 |  200166   50971  2285220    44.8 |  1.535 % |
c ==============================================================================
c (current CPU-time: 288.275 s)
c ==============================================================================
c [1mFound solution: 428784[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     55756 |  256838   825999 |   77051   52239  2422329    46.4 |  1.535 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1187          
c   -- var.elim.:  1187/1187          
c   -- var.elim.:  1000/1043          
c   -- var.elim.:  1043/1043          
c   -- var.elim.:  673/673          
c   -- var.elim.:  622/622          
c   -- var.elim.:  620/620          
c   -- var.elim.:  626/626          
c   -- subsuming                       
c   -- var.elim.:  67/67          
c |     55756 |  256733   827365 |      --   52239       --      -- |     --   | -105/1367
c |     55756 |  256733   827365 |  102693   51691  2107428    40.8 |  1.535 % |
c |     55858 |  256733   827365 |  112962   51793  2108016    40.7 |  1.554 % |
c |     56008 |  256733   827365 |  124258   51943  2113940    40.7 |  1.554 % |
c |     56233 |  256726   827345 |  136680   52167  2123048    40.7 |  1.556 % |
c ==============================================================================
c (current CPU-time: 294.802 s)
c ==============================================================================
c [1mFound solution: 428775[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     56487 |  256835   828520 |   77050   52421  2141714    40.9 |  1.556 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1062          
c   -- var.elim.:  1062/1062          
c   -- var.elim.:  983/983          
c   -- var.elim.:  792/792          
c |     56487 |  256750   830333 |      --   52421       --      -- |     --   | -85/1814
c |     56487 |  256750   830333 |  102700   52421  2141714    40.9 |  1.556 % |
c |     56587 |  256750   830333 |  112970   52521  2142715    40.8 |  1.558 % |
c |     56737 |  256729   829667 |  124256   52670  2143685    40.7 |  1.565 % |
c |     56962 |  256638   825950 |  136634   52891  2149865    40.6 |  1.589 % |
c |     57301 |  256596   825806 |  150272   53229  2155023    40.5 |  1.599 % |
c |     57807 |  256557   825668 |  165275   53734  2160163    40.2 |  1.608 % |
c |     58567 |  256432   825166 |  181713   54465  2241866    41.2 |  1.642 % |
c |     59706 |  256432   825166 |  199885   55604  2278197    41.0 |  1.642 % |
c |     61416 |  256399   825059 |  219845   57311  2360316    41.2 |  1.651 % |
c |     63978 |  256381   824963 |  241813   59871  2442469    40.8 |  1.655 % |
c ==============================================================================
c (current CPU-time: 323.628 s)
c ==============================================================================
c [1mFound solution: 389399[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     64651 |  256467   825960 |   76940   60544  2509829    41.5 |  1.655 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1844          
c   -- var.elim.:  1844/1844          
c   -- var.elim.:  1000/1585          
c   -- var.elim.:  1585/1585          
c   -- var.elim.:  42/42          
c   -- subsuming                       
c   -- var.elim.:  725/725          
c   -- var.elim.:  10/10          
c |     64651 |  256364   829452 |      --   60544       --      -- |     --   | -101/3497
c |     64651 |  256364   829452 |  102545   58677  1981054    33.8 |  1.655 % |
c |     64751 |  256165   822482 |  112712   58774  1982424    33.7 |  1.712 % |
c |     64903 |  256165   822482 |  123983   58926  1990408    33.8 |  1.712 % |
c |     65128 |  256165   822482 |  136382   59151  2000707    33.8 |  1.712 % |
c |     65466 |  256165   822482 |  150020   59489  2009943    33.8 |  1.712 % |
c |     65972 |  256116   822299 |  164990   59972  2021323    33.7 |  1.723 % |
c |     66734 |  256116   822299 |  181490   60734  2135671    35.2 |  1.723 % |
c ==============================================================================
c (current CPU-time: 355.546 s)
c ==============================================================================
c [1mFound solution: 349894[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     67507 |  256205   822932 |   76861   61507  2268296    36.9 |  1.723 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1582          
c   -- var.elim.:  1582/1582          
c   -- var.elim.:  577/577          
c   -- var.elim.:  290/290          
c   -- var.elim.:  52/52          
c   -- subsuming                       
c   -- var.elim.:  309/309          
c |     67507 |  256110   823032 |      --   61507       --      -- |     --   | -95/101
c |     67507 |  256110   823032 |  102444   61120  2161801    35.4 |  1.723 % |
c |     67607 |  256110   823032 |  112688   61220  2162707    35.3 |  1.725 % |
c |     67757 |  256110   823032 |  123957   61370  2190464    35.7 |  1.725 % |
c |     67982 |  256062   822863 |  136327   61594  2246505    36.5 |  1.738 % |
c |     68320 |  255950   822450 |  149894   61931  2311331    37.3 |  1.770 % |
c |     68827 |  255950   822450 |  164884   62438  2335580    37.4 |  1.770 % |
c |     69586 |  255831   821999 |  181288   63194  2446021    38.7 |  1.804 % |
c |     70725 |  255811   821929 |  199401   64332  2606280    40.5 |  1.809 % |
c |     72436 |  255811   821929 |  219341   66043  2664337    40.3 |  1.809 % |
c |     74999 |  255769   821777 |  241235   68595  3409469    49.7 |  1.822 % |
c |     78844 |  255695   821512 |  265282   72438  4137839    57.1 |  1.841 % |
c |     84610 |  255695   821512 |  291811   78204  5821885    74.4 |  1.841 % |
c |     93259 |  255595   821155 |  320866   86850  7021785    80.8 |  1.867 % |
c ==============================================================================
c (current CPU-time: 528.021 s)
c ==============================================================================
c [1mFound solution: 349082[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     94029 |  255729   822253 |   76718   87620  7103956    81.1 |  1.867 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2014          
c   -- var.elim.:  2000/2014          
c   -- var.elim.:  2014/2014          
c   -- var.elim.:  1000/1208          
c   -- var.elim.:  1208/1208          
c   -- var.elim.:  791/791          
c   -- var.elim.:  737/737          
c   -- var.elim.:  743/743          
c   -- var.elim.:  744/744          
c   -- subsuming                       
c   -- var.elim.:  765/765          
c   -- var.elim.:  9/9          
c |     94029 |  255564   824350 |      --   87620       --      -- |     --   | -162/2104
c |     94029 |  255564   824350 |  102225   84111  4314161    51.3 |  1.867 % |
c |     94130 |  255564   824350 |  112448   84212  4315734    51.2 |  1.876 % |
c |     94280 |  255564   824350 |  123692   84362  4320896    51.2 |  1.876 % |
c |     94505 |  255564   824350 |  136062   84587  4331031    51.2 |  1.876 % |
c |     94843 |  255564   824350 |  149668   84925  4333607    51.0 |  1.876 % |
c |     95349 |  255564   824350 |  164635   85431  4365665    51.1 |  1.876 % |
c |     96108 |  255564   824350 |  181098   86190  4436825    51.5 |  1.876 % |
c |     97248 |  255564   824350 |  199208   87330  4471250    51.2 |  1.876 % |
c |     98957 |  255535   823960 |  219104   89028  4708719    52.9 |  1.883 % |
c |    101520 |  255535   823960 |  241015   91591  5683052    62.0 |  1.883 % |
c ==============================================================================
c (current CPU-time: 594.788 s)
c ==============================================================================
c [1mFound solution: 349080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    102697 |  255622   824859 |   76686   92768  5949303    64.1 |  1.883 % |
c   -- subsuming                       
c   -- var.elim.:  937/937          
c   -- var.elim.:  1000/1470          
c   -- var.elim.:  1470/1470          
c   -- var.elim.:  686/686          
c   -- var.elim.:  659/659          
c   -- var.elim.:  657/657          
c |    102697 |  255540   824722 |      --   92768       --      -- |     --   | -82/-136
c |    102697 |  255540   824722 |  102216   92755  5946804    64.1 |  1.883 % |
c |    102797 |  255478   824491 |  112410   92854  5947859    64.1 |  1.902 % |
c |    102947 |  255478   824491 |  123651   93004  5950676    64.0 |  1.902 % |
c ==============================================================================
c (current CPU-time: 600.491 s)
c ==============================================================================
c [1mFound solution: 349079[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    103062 |  255575   825416 |   76672   93119  5966401    64.1 |  1.902 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1189          
c   -- var.elim.:  1189/1189          
c   -- var.elim.:  891/891          
c   -- var.elim.:  693/693          
c   -- var.elim.:  658/658          
c   -- var.elim.:  656/656          
c |    103062 |  255483   825533 |      --   93119       --      -- |     --   | -92/118
c |    103062 |  255483   825533 |  102193   93091  5955667    64.0 |  1.902 % |
c |    103163 |  255483   825533 |  112412   93192  5957235    63.9 |  1.904 % |
c |    103313 |  255483   825533 |  123653   93342  5980145    64.1 |  1.904 % |
c |    103538 |  255483   825533 |  136019   93567  5996376    64.1 |  1.904 % |
c |    103875 |  255483   825533 |  149621   93904  6000323    63.9 |  1.904 % |
c |    104382 |  255483   825533 |  164583   94411  6166684    65.3 |  1.904 % |
c |    105141 |  255423   825321 |  180998   95169  6285444    66.0 |  1.919 % |
c |    106280 |  255403   825251 |  199083   96307  6511855    67.6 |  1.925 % |
c |    107989 |  255403   825251 |  218991   98016  7098403    72.4 |  1.925 % |
c |    110551 |  255403   825251 |  240890  100578  7665368    76.2 |  1.925 % |
c |    114399 |  255403   825251 |  264979  104426  7906062    75.7 |  1.925 % |
c |    120166 |  255382   825190 |  291453  110190 10339654    93.8 |  1.930 % |
c ==============================================================================
c (current CPU-time: 799.73 s)
c ==============================================================================
c [1mFound solution: 349078[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    122185 |  255428   825898 |   76628  112208 11060387    98.6 |  1.930 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1033          
c   -- var.elim.:  1033/1033          
c   -- var.elim.:  931/931          
c   -- var.elim.:  692/692          
c   -- var.elim.:  657/657          
c   -- var.elim.:  655/655          
c   -- subsuming                       
c   -- var.elim.:  34/34          
c |    122185 |  255320   825806 |      --  112208       --      -- |     --   | -108/-91
c |    122185 |  255320   825806 |  102128  107802  7466928    69.3 |  1.930 % |
c |    122286 |  255320   825806 |  112340   22065  1916812    86.9 |  1.946 % |
c |    122438 |  255320   825806 |  123574   22217  1929374    86.8 |  1.946 % |
c |    122663 |  255320   825806 |  135932   22442  2003774    89.3 |  1.946 % |
c |    123000 |  255320   825806 |  149525   22779  2061916    90.5 |  1.946 % |
c |    123508 |  255320   825806 |  164478   23287  2282379    98.0 |  1.946 % |
c |    124267 |  255320   825806 |  180925   24046  2516371   104.6 |  1.946 % |
c |    125406 |  255320   825806 |  199018   25185  2994024   118.9 |  1.946 % |
c ==============================================================================
c (current CPU-time: 847.127 s)
c ==============================================================================
c [1mFound solution: 349056[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    126163 |  255444   826987 |   76633   25942  3263665   125.8 |  1.946 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1033          
c   -- var.elim.:  1033/1033          
c   -- var.elim.:  963/963          
c   -- var.elim.:  571/571          
c   -- var.elim.:  540/540          
c   -- var.elim.:  113/113          
c |    126163 |  255337   827535 |      --   25942       --      -- |     --   | -107/549
c |    126163 |  255337   827535 |  102134   25942  3263665   125.8 |  1.946 % |
c |    126263 |  255337   827535 |  112348   26042  3265306   125.4 |  1.947 % |
c |    126413 |  255337   827535 |  123583   26192  3266150   124.7 |  1.947 % |
c |    126640 |  255337   827535 |  135941   26419  3267528   123.7 |  1.947 % |
c |    126977 |  255337   827535 |  149535   26756  3328760   124.4 |  1.947 % |
c |    127484 |  255315   827456 |  164474   27262  3478525   127.6 |  1.953 % |
c |    128243 |  255315   827456 |  180922   28021  3745251   133.7 |  1.953 % |
c |    129386 |  255315   827456 |  199014   29164  4213855   144.5 |  1.953 % |
c |    131094 |  255315   827456 |  218916   30872  4554402   147.5 |  1.953 % |
c |    133656 |  255315   827456 |  240807   33434  5622700   168.2 |  1.953 % |
c ==============================================================================
c (current CPU-time: 929.672 s)
c ==============================================================================
c [1mFound solution: 348989[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    134908 |  255418   828510 |   76625   34686  5849669   168.6 |  1.953 % |
c   -- subsuming                       
c   -- var.elim.:  963/963          
c   -- var.elim.:  884/884          
c   -- var.elim.:  473/473          
c   -- var.elim.:  777/777          
c   -- var.elim.:  670/670          
c |    134908 |  255323   828967 |      --   34686       --      -- |     --   | -95/458
c |    134908 |  255323   828967 |  102129   34686  5849669   168.6 |  1.953 % |
c |    135008 |  255293   828872 |  112328   34785  5850537   168.2 |  1.962 % |
c |    135158 |  255293   828872 |  123561   34935  5855502   167.6 |  1.962 % |
c |    135384 |  255293   828872 |  135917   35161  5915340   168.2 |  1.962 % |
c |    135722 |  255293   828872 |  149509   35499  6023475   169.7 |  1.962 % |
c |    136229 |  255293   828872 |  164460   36006  6130559   170.3 |  1.962 % |
c |    136988 |  255293   828872 |  180906   36765  6146892   167.2 |  1.962 % |
c |    138127 |  255293   828872 |  198997   37904  6242151   164.7 |  1.962 % |
c ==============================================================================
c (current CPU-time: 960.088 s)
c ==============================================================================
c [1mFound solution: 348597[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    139804 |  255403   829972 |   76620   39581  6469413   163.4 |  1.962 % |
c   -- subsuming                       
c   -- var.elim.:  998/998          
c   -- var.elim.:  928/928          
c   -- var.elim.:  775/775          
c   -- var.elim.:  809/809          
c   -- var.elim.:  739/739          
c   -- var.elim.:  741/741          
c   -- var.elim.:  739/739          
c |    139804 |  255300   830627 |      --   39581       --      -- |     --   | -103/656
c |    139804 |  255300   830627 |  102120   39309  6175323   157.1 |  1.962 % |
c |    139905 |  255300   830627 |  112332   39410  6176359   156.7 |  1.964 % |
c |    140055 |  255300   830627 |  123565   39560  6177174   156.1 |  1.964 % |
c |    140283 |  255300   830627 |  135921   39788  6239893   156.8 |  1.964 % |
c |    140620 |  255300   830627 |  149513   40125  6363622   158.6 |  1.964 % |
c |    141126 |  255300   830627 |  164465   40631  6490892   159.8 |  1.964 % |
c |    141885 |  255284   830575 |  180900   41389  6846879   165.4 |  1.968 % |
c |    143026 |  255284   830575 |  198990   42530  7083931   166.6 |  1.968 % |
c |    144739 |  255284   830575 |  218889   44243  7141098   161.4 |  1.968 % |
c ==============================================================================
c (current CPU-time: 1015.02 s)
c ==============================================================================
c [1mFound solution: 348462[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    146939 |  255342   831473 |   76602   46442  7565240   162.9 |  1.968 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1034          
c   -- var.elim.:  1034/1034          
c   -- var.elim.:  956/956          
c   -- var.elim.:  339/339          
c   -- var.elim.:  813/813          
c |    146939 |  255241   832652 |      --   46442       --      -- |     --   | -101/1180
c |    146939 |  255241   832652 |  102096   46418  7520305   162.0 |  1.968 % |
c |    147039 |  255241   832652 |  112306   46518  7520928   161.7 |  1.979 % |
c |    147192 |  255241   832652 |  123536   46671  7544410   161.7 |  1.979 % |
c |    147418 |  255241   832652 |  135890   46897  7560579   161.2 |  1.979 % |
c |    147756 |  255066   830274 |  149376   47152  7572398   160.6 |  2.015 % |
c ==============================================================================
c (current CPU-time: 1025.71 s)
c ==============================================================================
c [1mFound solution: 348434[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    147827 |  255182   831474 |   76554   47223  7576824   160.4 |  2.015 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1239          
c   -- var.elim.:  1239/1239          
c   -- var.elim.:  1000/1524          
c   -- var.elim.:  1524/1524          
c   -- var.elim.:  1000/1296          
c   -- var.elim.:  1296/1296          
c   -- var.elim.:  939/939          
c   -- var.elim.:  754/754          
c   -- var.elim.:  756/756          
c   -- subsuming                       
c   -- var.elim.:  10/10          
c |    147827 |  255029   834503 |      --   47223       --      -- |     --   | -153/3030
c |    147827 |  255029   834503 |  102011   40910  3702960    90.5 |  2.015 % |
c |    147927 |  255029   834503 |  112212   41010  3706023    90.4 |  2.018 % |
c |    148077 |  255029   834503 |  123434   41160  3707291    90.1 |  2.018 % |
c |    148302 |  255029   834503 |  135777   41385  3709448    89.6 |  2.018 % |
c |    148639 |  255029   834503 |  149355   41722  3729465    89.4 |  2.018 % |
c |    149145 |  255029   834503 |  164290   42228  3763633    89.1 |  2.018 % |
c |    149904 |  255029   834503 |  180719   42987  3828187    89.1 |  2.018 % |
c |    151043 |  254987   833809 |  198759   44122  4369506    99.0 |  2.031 % |
c |    152753 |  254987   833809 |  218634   45832  5081090   110.9 |  2.031 % |
c |    155317 |  254959   832935 |  240471   48395  5468130   113.0 |  2.039 % |
c ==============================================================================
c (current CPU-time: 1092.17 s)
c ==============================================================================
c [1mFound solution: 347552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    155644 |  255080   834034 |   76523   48722  5519046   113.3 |  2.039 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1636          
c   -- var.elim.:  1636/1636          
c   -- var.elim.:  1000/1527          
c   -- var.elim.:  1527/1527          
c   -- var.elim.:  461/461          
c   -- var.elim.:  794/794          
c   -- subsuming                       
c   -- var.elim.:  931/931          
c |    155644 |  254967   836201 |      --   48722       --      -- |     --   | -113/2168
c |    155644 |  254967   836201 |  101986   48115  4909720   102.0 |  2.039 % |
c |    155744 |  254967   836201 |  112185   48215  4910490   101.8 |  2.041 % |
c |    155895 |  254967   836201 |  123404   48366  4912016   101.6 |  2.041 % |
c |    156120 |  254967   836201 |  135744   48591  4942773   101.7 |  2.041 % |
c |    156457 |  254967   836201 |  149318   48928  5087293   104.0 |  2.041 % |
c |    156963 |  254967   836201 |  164250   49434  5240006   106.0 |  2.041 % |
c |    157724 |  254967   836201 |  180675   50195  5445730   108.5 |  2.041 % |
c |    158865 |  254967   836201 |  198743   51336  5612193   109.3 |  2.041 % |
c ==============================================================================
c (current CPU-time: 1133.02 s)
c ==============================================================================
c [1mFound solution: 347551[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    160259 |  255076   837306 |   76522   52730  5831072   110.6 |  2.041 % |
c   -- subsuming                       
c   -- var.elim.:  975/975          
c   -- var.elim.:  916/916          
c   -- var.elim.:  461/461          
c   -- var.elim.:  822/822          
c |    160259 |  254981   838141 |      --   52730       --      -- |     --   | -95/836
c |    160259 |  254981   838141 |  101992   52730  5831072   110.6 |  2.041 % |
c |    160359 |  254981   838141 |  112191   52830  5844319   110.6 |  2.042 % |
c#### 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.94 0.70 2/54 8891
Raw data (stat): 8891 (runsolver) R 8890 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487606123 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.87 0.94 0.71 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 15314 0 0 0 954 44 0 0 25 0 1 0 487606123 65712128 14062 4294967295 134512640 134672761 3221224576 3221222752 134604682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16043 14062 603 41 0 16002 0
vsize: 64172
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.94 0.71 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 19007 0 0 0 1933 64 0 0 25 0 1 0 487606123 79351808 16678 4294967295 134512640 134672761 3221224576 3221222864 134565194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19373 16678 603 41 0 19332 0
vsize: 77492
[startup+30.002 s]
Raw data (loadavg): 0.90 0.94 0.71 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 24655 0 0 0 2910 86 0 0 25 0 1 0 487606123 65855488 14226 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16078 14226 603 41 0 16037 0
vsize: 64312
[startup+40.002 s]
Raw data (loadavg): 0.92 0.94 0.72 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 28989 0 0 0 3895 102 0 0 25 0 1 0 487606123 66068480 14282 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16130 14282 603 41 0 16089 0
vsize: 64520
[startup+50.0023 s]
Raw data (loadavg): 0.93 0.94 0.72 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 29133 0 0 0 4894 102 0 0 25 0 1 0 487606123 66609152 14426 4294967295 134512640 134672761 3221224576 3221223616 134612978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16262 14426 603 41 0 16221 0
vsize: 65048
[startup+60.002 s]
Raw data (loadavg): 0.94 0.95 0.72 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 29613 0 0 0 5893 104 0 0 25 0 1 0 487606123 68608000 14906 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16750 14906 603 41 0 16709 0
vsize: 67000
[startup+70.0018 s]
Raw data (loadavg): 0.95 0.95 0.73 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 35156 0 0 0 6876 120 0 0 25 0 1 0 487606123 75993088 15973 4294967295 134512640 134672761 3221224576 3221222992 134609266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18553 15973 603 41 0 18512 0
vsize: 74212
[startup+80.0025 s]
Raw data (loadavg): 0.96 0.95 0.73 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 38785 0 0 0 7862 134 0 0 25 0 1 0 487606123 68927488 15009 4294967295 134512640 134672761 3221224576 3221223760 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16828 15009 603 41 0 16787 0
vsize: 67312
[startup+90.0021 s]
Raw data (loadavg): 0.96 0.95 0.73 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 38801 0 0 0 8862 134 0 0 25 0 1 0 487606123 69062656 15025 4294967295 134512640 134672761 3221224576 3221223700 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16861 15025 603 41 0 16820 0
vsize: 67444
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.73 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 43329 0 0 0 9846 150 0 0 25 0 1 0 487606123 69128192 15060 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16877 15060 603 41 0 16836 0
vsize: 67508
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.73 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 47938 0 0 0 10830 166 0 0 25 0 1 0 487606123 69648384 15126 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17004 15126 603 41 0 16963 0
vsize: 68016
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.74 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 48051 0 0 0 11830 166 0 0 25 0 1 0 487606123 70049792 15239 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17102 15239 603 41 0 17061 0
vsize: 68408
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.74 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 48265 0 0 0 12829 167 0 0 25 0 1 0 487606123 70959104 15453 4294967295 134512640 134672761 3221224576 3221223680 134604309 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17324 15453 603 41 0 17283 0
vsize: 69296
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.74 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 48440 0 0 0 13829 168 0 0 25 0 1 0 487606123 71614464 15628 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17484 15628 603 41 0 17443 0
vsize: 69936
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.74 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 48583 0 0 0 14829 168 0 0 25 0 1 0 487606123 72273920 15771 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17645 15771 603 41 0 17604 0
vsize: 70580
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 48741 0 0 0 15827 169 0 0 25 0 1 0 487606123 72929280 15929 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17805 15929 603 41 0 17764 0
vsize: 71220
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 48892 0 0 0 16827 170 0 0 25 0 1 0 487606123 73588736 16080 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17966 16080 603 41 0 17925 0
vsize: 71864
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 52048 0 0 0 17818 179 0 0 25 0 1 0 487606123 89554944 19165 4294967295 134512640 134672761 3221224576 3221222956 1075325891 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21864 19165 603 41 0 21823 0
vsize: 87456
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 53655 0 0 0 18812 185 0 0 25 0 1 0 487606123 74272768 16237 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18133 16237 603 41 0 18092 0
vsize: 72532
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 57491 0 0 0 19799 197 0 0 25 0 1 0 487606123 74272768 16265 4294967295 134512640 134672761 3221224576 3221223712 134614583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18133 16265 603 41 0 18092 0
vsize: 72532
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 61286 0 0 0 20786 211 0 0 25 0 1 0 487606123 74272768 16270 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18133 16270 603 41 0 18092 0
vsize: 72532
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.76 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 61290 0 0 0 21785 211 0 0 25 0 1 0 487606123 74272768 16274 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18133 16274 603 41 0 18092 0
vsize: 72532
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.76 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 65558 0 0 0 22772 224 0 0 25 0 1 0 487606123 78180352 17113 4294967295 134512640 134672761 3221224576 3221223120 134621095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19087 17113 603 41 0 19046 0
vsize: 76348
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.76 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 66164 0 0 0 23770 226 0 0 25 0 1 0 487606123 75399168 16543 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18408 16543 603 41 0 18367 0
vsize: 73632
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.76 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 66166 0 0 0 24770 226 0 0 25 0 1 0 487606123 75399168 16545 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18408 16545 603 41 0 18367 0
vsize: 73632
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 70751 0 0 0 25753 243 0 0 25 0 1 0 487606123 75563008 16584 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18448 16584 603 41 0 18407 0
vsize: 73792
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 70925 0 0 0 26751 244 0 0 25 0 1 0 487606123 76210176 16758 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18606 16758 603 41 0 18565 0
vsize: 74424
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 71035 0 0 0 27751 244 0 0 25 0 1 0 487606123 76611584 16868 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18704 16868 603 41 0 18663 0
vsize: 74816
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 71185 0 0 0 28751 244 0 0 25 0 1 0 487606123 77262848 17018 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18863 17018 603 41 0 18822 0
vsize: 75452
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 79515 0 0 0 29722 272 0 0 25 0 1 0 487606123 77484032 17089 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18917 17089 603 41 0 18876 0
vsize: 75668
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 79518 0 0 0 30721 273 0 0 25 0 1 0 487606123 77484032 17092 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18917 17092 603 41 0 18876 0
vsize: 75668
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 79520 0 0 0 31721 273 0 0 25 0 1 0 487606123 77484032 17094 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18917 17094 603 41 0 18876 0
vsize: 75668
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 83819 0 0 0 32707 287 0 0 25 0 1 0 487606123 82010112 17858 4294967295 134512640 134672761 3221224576 3221223120 134621071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20022 17858 603 41 0 19981 0
vsize: 80088
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 84425 0 0 0 33705 289 0 0 25 0 1 0 487606123 78307328 17284 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19118 17284 603 41 0 19077 0
vsize: 76472
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 84425 0 0 0 34705 289 0 0 25 0 1 0 487606123 78307328 17284 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19118 17284 603 41 0 19077 0
vsize: 76472
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 87696 0 0 0 35691 303 0 0 25 0 1 0 487606123 78368768 17317 4294967295 134512640 134672761 3221224576 3221222620 1075350014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19133 17317 603 41 0 19092 0
vsize: 76532
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 88871 0 0 0 36688 306 0 0 25 0 1 0 487606123 78368768 17317 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19133 17317 603 41 0 19092 0
vsize: 76532
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 88872 0 0 0 37688 306 0 0 25 0 1 0 487606123 78368768 17318 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19133 17318 603 41 0 19092 0
vsize: 76532
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 88966 0 0 0 38688 306 0 0 25 0 1 0 487606123 78766080 17412 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19230 17412 603 41 0 19189 0
vsize: 76920
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 89281 0 0 0 39686 308 0 0 25 0 1 0 487606123 80343040 17727 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19615 17727 603 41 0 19574 0
vsize: 78460
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 89540 0 0 0 40685 309 0 0 25 0 1 0 487606123 81379328 17986 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19868 17986 603 41 0 19827 0
vsize: 79472
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 89852 0 0 0 41685 310 0 0 25 0 1 0 487606123 82661376 18298 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20181 18298 603 41 0 20140 0
vsize: 80724
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 90131 0 0 0 42684 311 0 0 25 0 1 0 487606123 83845120 18577 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20470 18577 603 41 0 20429 0
vsize: 81880
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 90568 0 0 0 43682 313 0 0 25 0 1 0 487606123 85549056 19014 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20886 19014 603 41 0 20845 0
vsize: 83544
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 91002 0 0 0 44681 314 0 0 25 0 1 0 487606123 87367680 19448 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21330 19448 603 41 0 21289 0
vsize: 85320
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 91611 0 0 0 45678 317 0 0 25 0 1 0 487606123 89845760 20057 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21935 20057 603 41 0 21894 0
vsize: 87740
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 92078 0 0 0 46677 318 0 0 25 0 1 0 487606123 91783168 20524 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22408 20524 603 41 0 22367 0
vsize: 89632
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 92373 0 0 0 47676 319 0 0 25 0 1 0 487606123 92954624 20819 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22694 20819 603 41 0 22653 0
vsize: 90776
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 92613 0 0 0 48676 320 0 0 25 0 1 0 487606123 94007296 21059 4294967295 134512640 134672761 3221224576 3221223720 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22951 21059 603 41 0 22910 0
vsize: 91804
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 92873 0 0 0 49674 321 0 0 25 0 1 0 487606123 95051776 21319 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23206 21319 603 41 0 23165 0
vsize: 92824
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 93129 0 0 0 50674 322 0 0 25 0 1 0 487606123 96100352 21575 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23462 21575 603 41 0 23421 0
vsize: 93848
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 93408 0 0 0 51673 323 0 0 25 0 1 0 487606123 97177600 21854 4294967295 134512640 134672761 3221224576 3221223616 134612507 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23725 21854 603 41 0 23684 0
vsize: 94900
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 8891
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 93627 0 0 0 52672 324 0 0 25 0 1 0 487606123 98086912 22073 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23947 22073 603 41 0 23906 0
vsize: 95788
[startup+540.007 s]
Raw data (loadavg): 1.07 0.99 0.82 2/54 8944
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 98321 0 0 0 53655 340 0 0 25 0 1 0 487606123 98291712 22144 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23997 22144 603 41 0 23956 0
vsize: 95988
[startup+550.007 s]
Raw data (loadavg): 1.06 0.99 0.82 2/54 8944
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 98321 0 0 0 54655 340 0 0 25 0 1 0 487606123 98291712 22144 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23997 22144 603 41 0 23956 0
vsize: 95988
[startup+560.008 s]
Raw data (loadavg): 1.05 0.99 0.83 2/54 8944
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 98323 0 0 0 55656 340 0 0 25 0 1 0 487606123 98291712 22146 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23997 22146 603 41 0 23956 0
vsize: 95988
[startup+570.008 s]
Raw data (loadavg): 1.04 0.99 0.83 2/54 8944
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 98323 0 0 0 56656 341 0 0 25 0 1 0 487606123 98291712 22146 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23997 22146 603 41 0 23956 0
vsize: 95988
[startup+580.007 s]
Raw data (loadavg): 1.03 0.99 0.83 2/54 8944
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 98325 0 0 0 57655 341 0 0 25 0 1 0 487606123 98291712 22148 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23997 22148 603 41 0 23956 0
vsize: 95988
[startup+590.008 s]
Raw data (loadavg): 1.03 0.99 0.83 2/54 8944
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 98325 0 0 0 58655 341 0 0 25 0 1 0 487606123 98291712 22148 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23997 22148 603 41 0 23956 0
vsize: 95988
[startup+600.008 s]
Raw data (loadavg): 1.02 0.99 0.83 2/54 8944
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 101296 0 0 0 59644 352 0 0 25 0 1 0 487606123 98406400 22177 4294967295 134512640 134672761 3221224576 3221222648 134544511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24025 22177 603 41 0 23984 0
vsize: 96100
[startup+610.009 s]
Raw data (loadavg): 1.02 0.99 0.83 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 105352 0 0 0 60628 368 0 0 25 0 1 0 487606123 98406400 22186 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24025 22186 603 41 0 23984 0
vsize: 96100
[startup+620.009 s]
Raw data (loadavg): 1.02 0.99 0.83 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 105353 0 0 0 61627 368 0 0 25 0 1 0 487606123 98406400 22187 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24025 22187 603 41 0 23984 0
vsize: 96100
[startup+630.009 s]
Raw data (loadavg): 1.01 0.99 0.83 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 105354 0 0 0 62628 368 0 0 25 0 1 0 487606123 98406400 22188 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24025 22188 603 41 0 23984 0
vsize: 96100
[startup+640.009 s]
Raw data (loadavg): 1.01 0.99 0.83 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 105354 0 0 0 63628 368 0 0 25 0 1 0 487606123 98406400 22188 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24025 22188 603 41 0 23984 0
vsize: 96100
[startup+650.009 s]
Raw data (loadavg): 1.01 0.99 0.83 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 105355 0 0 0 64628 368 0 0 25 0 1 0 487606123 98406400 22189 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24025 22189 603 41 0 23984 0
vsize: 96100
[startup+660.01 s]
Raw data (loadavg): 1.01 0.99 0.83 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 105356 0 0 0 65628 368 0 0 25 0 1 0 487606123 98406400 22190 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24025 22190 603 41 0 23984 0
vsize: 96100
[startup+670.01 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 105535 0 0 0 66628 369 0 0 25 0 1 0 487606123 99184640 22369 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24215 22369 603 41 0 24174 0
vsize: 96860
[startup+680.01 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 105801 0 0 0 67627 369 0 0 25 0 1 0 487606123 100225024 22635 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24469 22635 603 41 0 24428 0
vsize: 97876
[startup+690.011 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 106031 0 0 0 68627 370 0 0 25 0 1 0 487606123 101261312 22865 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24722 22865 603 41 0 24681 0
vsize: 98888
[startup+700.011 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 106295 0 0 0 69626 371 0 0 25 0 1 0 487606123 102322176 23129 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24981 23129 603 41 0 24940 0
vsize: 99924
[startup+710.011 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 106575 0 0 0 70626 372 0 0 25 0 1 0 487606123 103485440 23409 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25265 23409 603 41 0 25224 0
vsize: 101060
[startup+720.012 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 106906 0 0 0 71625 373 0 0 25 0 1 0 487606123 104812544 23740 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25589 23740 603 41 0 25548 0
vsize: 102356
[startup+730.011 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 107278 0 0 0 72624 374 0 0 25 0 1 0 487606123 106242048 24112 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25938 24112 603 41 0 25897 0
vsize: 103752
[startup+740.011 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 107581 0 0 0 73623 375 0 0 25 0 1 0 487606123 107524096 24415 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26251 24415 603 41 0 26210 0
vsize: 105004
[startup+750.011 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 107900 0 0 0 74622 376 0 0 25 0 1 0 487606123 108818432 24734 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26567 24734 603 41 0 26526 0
vsize: 106268
[startup+760.011 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 108294 0 0 0 75622 376 0 0 25 0 1 0 487606123 110518272 25128 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26982 25128 603 41 0 26941 0
vsize: 107928
[startup+770.012 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 108648 0 0 0 76621 377 0 0 25 0 1 0 487606123 111955968 25482 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27333 25482 603 41 0 27292 0
vsize: 109332
[startup+780.011 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 108868 0 0 0 77621 378 0 0 25 0 1 0 487606123 112865280 25702 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27555 25702 603 41 0 27514 0
vsize: 110220
[startup+790.012 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 109087 0 0 0 78620 379 0 0 25 0 1 0 487606123 113774592 25921 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27777 25921 603 41 0 27736 0
vsize: 111108
[startup+800.012 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 109424 0 0 0 79619 380 0 0 25 0 1 0 487606123 115089408 26258 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28098 26258 603 41 0 28057 0
vsize: 112392
[startup+810.012 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 114593 0 0 0 80604 395 0 0 25 0 1 0 487606123 116207616 26508 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26508 603 41 0 28330 0
vsize: 113484
[startup+820.012 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 114593 0 0 0 81604 395 0 0 25 0 1 0 487606123 116207616 26508 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26508 603 41 0 28330 0
vsize: 113484
[startup+830.012 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 114593 0 0 0 82604 395 0 0 25 0 1 0 487606123 116207616 26508 4294967295 134512640 134672761 3221224576 3221223776 134610688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26508 603 41 0 28330 0
vsize: 113484
[startup+840.012 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 114593 0 0 0 83604 395 0 0 25 0 1 0 487606123 116207616 26508 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26508 603 41 0 28330 0
vsize: 113484
[startup+850.012 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 114593 0 0 0 84604 395 0 0 25 0 1 0 487606123 116207616 26508 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26508 603 41 0 28330 0
vsize: 113484
[startup+860.013 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 118085 0 0 0 85591 408 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+870.014 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 118085 0 0 0 86592 408 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+880.013 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 118085 0 0 0 87592 408 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+890.013 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 118085 0 0 0 88592 408 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+900.013 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8946
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 118085 0 0 0 89592 408 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+910.013 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 118085 0 0 0 90592 408 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+920.013 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 118085 0 0 0 91592 408 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+930.013 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 118085 0 0 0 92593 408 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+940.014 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 121577 0 0 0 93580 421 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+950.014 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 121577 0 0 0 94579 421 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+960.015 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 121577 0 0 0 95579 421 0 0 25 0 1 0 487606123 116207616 26510 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26510 603 41 0 28330 0
vsize: 113484
[startup+970.015 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 125071 0 0 0 96565 435 0 0 25 0 1 0 487606123 116207616 26512 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26512 603 41 0 28330 0
vsize: 113484
[startup+980.014 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 125071 0 0 0 97565 435 0 0 25 0 1 0 487606123 116207616 26512 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26512 603 41 0 28330 0
vsize: 113484
[startup+990.015 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 125071 0 0 0 98566 435 0 0 25 0 1 0 487606123 116207616 26512 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26512 603 41 0 28330 0
vsize: 113484
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 125071 0 0 0 99566 435 0 0 25 0 1 0 487606123 116207616 26512 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26512 603 41 0 28330 0
vsize: 113484
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 125071 0 0 0 100566 435 0 0 25 0 1 0 487606123 116207616 26512 4294967295 134512640 134672761 3221224576 3221223720 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26512 603 41 0 28330 0
vsize: 113484
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 127817 0 0 0 101559 442 0 0 25 0 1 0 487606123 130658304 29226 4294967295 134512640 134672761 3221224576 3221222912 134605456 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31899 29226 603 41 0 31858 0
vsize: 127596
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 128571 0 0 0 102554 448 0 0 25 0 1 0 487606123 116207616 26512 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28371 26512 603 41 0 28330 0
vsize: 113484
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 132671 0 0 0 103540 461 0 0 25 0 1 0 487606123 116158464 26504 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26504 603 41 0 28318 0
vsize: 113436
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 132671 0 0 0 104541 461 0 0 25 0 1 0 487606123 116158464 26504 4294967295 134512640 134672761 3221224576 3221223760 134616005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26504 603 41 0 28318 0
vsize: 113436
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 132671 0 0 0 105541 461 0 0 25 0 1 0 487606123 116158464 26504 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28359 26504 603 41 0 28318 0
vsize: 113436
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 132671 0 0 0 106540 461 0 0 25 0 1 0 487606123 116158464 26504 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26504 603 41 0 28318 0
vsize: 113436
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 132671 0 0 0 107541 461 0 0 25 0 1 0 487606123 116158464 26504 4294967295 134512640 134672761 3221224576 3221223616 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26504 603 41 0 28318 0
vsize: 113436
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 132671 0 0 0 108541 461 0 0 25 0 1 0 487606123 116158464 26504 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26504 603 41 0 28318 0
vsize: 113436
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 136180 0 0 0 109528 474 0 0 25 0 1 0 487606123 119074816 27092 4294967295 134512640 134672761 3221224576 3221223120 134621116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29071 27092 603 41 0 29030 0
vsize: 116284
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 136768 0 0 0 110525 477 0 0 25 0 1 0 487606123 116158464 26504 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26504 603 41 0 28318 0
vsize: 113436
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 136768 0 0 0 111525 477 0 0 25 0 1 0 487606123 116158464 26504 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26504 603 41 0 28318 0
vsize: 113436
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 136769 0 0 0 112526 477 0 0 25 0 1 0 487606123 116158464 26505 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26505 603 41 0 28318 0
vsize: 113436
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 140274 0 0 0 113511 491 0 0 25 0 1 0 487606123 116158464 26507 4294967295 134512640 134672761 3221224576 3221223832 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26507 603 41 0 28318 0
vsize: 113436
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 140274 0 0 0 114511 491 0 0 25 0 1 0 487606123 116158464 26507 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28359 26507 603 41 0 28318 0
vsize: 113436
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 140274 0 0 0 115510 491 0 0 25 0 1 0 487606123 116158464 26507 4294967295 134512640 134672761 3221224576 3221223824 134618422 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28359 26507 603 41 0 28318 0
vsize: 113436
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 140274 0 0 0 116510 492 0 0 25 0 1 0 487606123 116158464 26507 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26507 603 41 0 28318 0
vsize: 113436
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 140274 0 0 0 117509 492 0 0 25 0 1 0 487606123 116158464 26507 4294967295 134512640 134672761 3221224576 3221223712 134614721 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26507 603 41 0 28318 0
vsize: 113436
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 140274 0 0 0 118510 492 0 0 25 0 1 0 487606123 116158464 26507 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26507 603 41 0 28318 0
vsize: 113436
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 8948
Raw data (stat): 8891 (minisat+) R 8890 28546 28545 0 -1 0 140274 0 0 0 119510 492 0 0 25 0 1 0 487606123 116158464 26507 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28359 26507 603 41 0 28318 0
vsize: 113436
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.89 1/54 8948
Raw data (stat): 8891 (minisat+) Z 8890 28546 28545 0 -1 12 140275 0 0 0 119510 498 0 0 25 0 1 0 487606123 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.09
CPU time (s): 1200.09
CPU user time (s): 1195.1
CPU system time (s): 4.98424
CPU usage (%): 99.9999
Max. virtual memory (Kb): 127596
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####