PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	c8b965306fec2c21edee64824d12f378
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63488
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	230
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 16390

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-21 07:07:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13519 boxname=wulflinc24 idbench=1040 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c8b965306fec2c21edee64824d12f378  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare1.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare1.opb
IDLAUNCH: 13519
/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:        557456 kB
Buffers:         15136 kB
Cached:         434660 kB
SwapCached:        432 kB
Active:          50372 kB
Inactive:       401596 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        557204 kB
SwapTotal:     2097892 kB
SwapFree:      2096708 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5932 kB
Slab:            19512 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:27:16 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 13519 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> BDD-cost:23440
c ---[   8]---> BDD-cost:28410
c ---[   6]---> BDD-cost:25975
c ---[   4]---> BDD-cost:24801
c ---[   2]---> BDD-cost:25034
c ---[   0]---> BDD-cost:24120
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  436767  1274769 |  145589       0        0     nan |  0.000 % |
c |       101 |  436767  1274769 |  160147     101     7599    75.2 |  0.040 % |
c ==============================================================================
c [1mFound solution: 6404096[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       101 |  441175  1285058 |  147058     101     7599    75.2 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5898240[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       102 |  441198  1285135 |  147066     102     7622    74.7 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5855232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       125 |  441212  1285169 |  147070     125     9078    72.6 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5680128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       139 |  441234  1285220 |  147078     139     9626    69.3 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5663744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       186 |  441243  1285242 |  147081     186    11744    63.1 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5647360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       268 |  441251  1285261 |  147083     268    15602    58.2 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5596160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       307 |  441266  1285297 |  147088     307    17285    56.3 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5487616[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       382 |  441275  1285321 |  147091     382    20883    54.7 |  0.040 % |
c |       482 |  441275  1285321 |  161800     482    24693    51.2 |  0.044 % |
c |       632 |  441275  1285321 |  177980     632    30326    48.0 |  0.044 % |
c ==============================================================================
c [1mFound solution: 5464064[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       730 |  441287  1285350 |  147095     730    35225    48.3 |  0.044 % |
c |       830 |  441287  1285350 |  161804     830    39533    47.6 |  0.045 % |
c ==============================================================================
c [1mFound solution: 5440512[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       904 |  441297  1285373 |  147099     904    43500    48.1 |  0.045 % |
c ==============================================================================
c [1mFound solution: 5271552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       978 |  441308  1285399 |  147102     978    46652    47.7 |  0.045 % |
c |      1078 |  441308  1285399 |  161812    1078    50655    47.0 |  0.046 % |
c |      1229 |  441308  1285399 |  177993    1229    57259    46.6 |  0.046 % |
c |      1457 |  441308  1285399 |  195792    1457    68298    46.9 |  0.046 % |
c |      1796 |  441308  1285399 |  215372    1796    83053    46.2 |  0.046 % |
c |      2303 |  441308  1285399 |  236909    2303   106417    46.2 |  0.046 % |
c ==============================================================================
c [1mFound solution: 5121024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2367 |  441325  1285442 |  147108    2367   109675    46.3 |  0.046 % |
c |      2468 |  441325  1285442 |  161818    2468   113846    46.1 |  0.047 % |
c ==============================================================================
c [1mFound solution: 5060608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2522 |  441335  1285468 |  147111    2522   116155    46.1 |  0.047 % |
c |      2623 |  441335  1285468 |  161822    2623   119822    45.7 |  0.048 % |
c |      2776 |  441335  1285468 |  178004    2776   131258    47.3 |  0.048 % |
c ==============================================================================
c [1mFound solution: 5022720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2826 |  441345  1285492 |  147115    2826   133538    47.3 |  0.048 % |
c |      2926 |  441345  1285492 |  161826    2926   137038    46.8 |  0.048 % |
c ==============================================================================
c [1mFound solution: 4892672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2993 |  441361  1285530 |  147120    2993   140517    46.9 |  0.048 % |
c |      3093 |  441361  1285530 |  161832    3093   144868    46.8 |  0.049 % |
c |      3243 |  441361  1285530 |  178015    3243   151155    46.6 |  0.049 % |
c |      3468 |  441361  1285530 |  195816    3468   162183    46.8 |  0.049 % |
c |      3805 |  441361  1285530 |  215398    3805   177916    46.8 |  0.049 % |
c |      4313 |  441361  1285530 |  236938    4313   203493    47.2 |  0.049 % |
c |      5073 |  441361  1285530 |  260632    5073   238215    47.0 |  0.049 % |
c |      6212 |  441361  1285530 |  286695    6212   290626    46.8 |  0.049 % |
c |      7925 |  441361  1285530 |  315364    7925   373140    47.1 |  0.049 % |
c |     10487 |  441361  1285530 |  346901   10487   502342    47.9 |  0.049 % |
c ==============================================================================
c [1mFound solution: 3130368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11357 |  441373  1285563 |  147124   11357   548645    48.3 |  0.049 % |
c ==============================================================================
c [1mFound solution: 3030016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11368 |  441383  1285588 |  147127   11368   548955    48.3 |  0.049 % |
c |     11468 |  441383  1285588 |  161839   11468   553078    48.2 |  0.050 % |
c ==============================================================================
c [1mFound solution: 2987008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11526 |  441396  1285620 |  147132   11526   555621    48.2 |  0.050 % |
c |     11627 |  441396  1285620 |  161845   11627   559847    48.2 |  0.051 % |
c ==============================================================================
c [1mFound solution: 2855936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11752 |  441403  1285637 |  147134   11752   565521    48.1 |  0.051 % |
c |     11855 |  441403  1285637 |  161847   11855   569209    48.0 |  0.052 % |
c |     12005 |  441403  1285637 |  178032   12005   578630    48.2 |  0.052 % |
c |     12230 |  441403  1285637 |  195835   12230   588352    48.1 |  0.052 % |
c ==============================================================================
c [1mFound solution: 2851840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12386 |  441412  1285660 |  147137   12386   595871    48.1 |  0.052 % |
c ==============================================================================
c [1mFound solution: 2816000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12476 |  441422  1285685 |  147140   12476   599897    48.1 |  0.052 % |
c |     12576 |  441415  1285670 |  161854   12571   604076    48.1 |  0.054 % |
c ==============================================================================
c [1mFound solution: 2775040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12595 |  441424  1285691 |  147141   12590   604749    48.0 |  0.054 % |
c |     12695 |  441424  1285691 |  161855   12690   608940    48.0 |  0.055 % |
c |     12846 |  441424  1285691 |  178040   12841   616100    48.0 |  0.055 % |
c ==============================================================================
c [1mFound solution: 2662400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12972 |  441436  1285719 |  147145   12967   622239    48.0 |  0.055 % |
c |     13072 |  441436  1285719 |  161859   13067   626166    47.9 |  0.056 % |
c |     13222 |  441436  1285719 |  178045   13217   633053    47.9 |  0.056 % |
c |     13448 |  441436  1285719 |  195849   13443   643739    47.9 |  0.056 % |
c |     13785 |  441436  1285719 |  215434   13780   659014    47.8 |  0.056 % |
c |     14291 |  441436  1285719 |  236978   14286   680978    47.7 |  0.056 % |
c |     15050 |  441436  1285719 |  260676   15045   715068    47.5 |  0.056 % |
c ==============================================================================
c [1mFound solution: 2650112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15554 |  441445  1285739 |  147148   15549   738967    47.5 |  0.056 % |
c |     15654 |  441440  1285729 |  161862   15644   742466    47.5 |  0.057 % |
c |     15805 |  441440  1285729 |  178049   15795   748653    47.4 |  0.057 % |
c |     16031 |  441440  1285729 |  195853   16021   759741    47.4 |  0.057 % |
c |     16369 |  441440  1285729 |  215439   16359   777405    47.5 |  0.057 % |
c ==============================================================================
c [1mFound solution: 2510848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16562 |  441452  1285758 |  147150   16552   785530    47.5 |  0.057 % |
c ==============================================================================
c [1mFound solution: 2456576[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16639 |  441463  1285784 |  147154   16629   788726    47.4 |  0.057 % |
c |     16739 |  441463  1285784 |  161869   16729   792734    47.4 |  0.059 % |
c |     16889 |  441463  1285784 |  178056   16879   799286    47.4 |  0.059 % |
c |     17114 |  441463  1285784 |  195861   17104   809644    47.3 |  0.059 % |
c |     17451 |  441463  1285784 |  215448   17441   825471    47.3 |  0.059 % |
c |     17957 |  441463  1285784 |  236992   17947   850339    47.4 |  0.059 % |
c ==============================================================================
c [1mFound solution: 2454528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18184 |  441474  1285811 |  147158   18174   861848    47.4 |  0.059 % |
c ==============================================================================
c [1mFound solution: 2437120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18214 |  441486  1285839 |  147162   18204   863992    47.5 |  0.059 % |
c |     18315 |  441486  1285839 |  161878   18305   867683    47.4 |  0.060 % |
c ==============================================================================
c [1mFound solution: 2432000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18354 |  441499  1285869 |  147166   18344   869636    47.4 |  0.060 % |
c |     18455 |  441499  1285869 |  161882   18445   873073    47.3 |  0.061 % |
c |     18607 |  441499  1285869 |  178070   18597   884539    47.6 |  0.061 % |
c |     18832 |  441499  1285869 |  195877   18822   898770    47.8 |  0.061 % |
c ==============================================================================
c [1mFound solution: 2405376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18988 |  441511  1285897 |  147170   18978   904556    47.7 |  0.061 % |
c ==============================================================================
c [1mFound solution: 2371584[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19036 |  441519  1285915 |  147173   19026   906591    47.7 |  0.061 % |
c |     19136 |  441519  1285915 |  161890   19126   910640    47.6 |  0.062 % |
c |     19286 |  441519  1285915 |  178079   19276   917023    47.6 |  0.062 % |
c |     19511 |  441519  1285915 |  195887   19501   926601    47.5 |  0.062 % |
c ==============================================================================
c [1mFound solution: 2337792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19570 |  441525  1285930 |  147175   19560   929041    47.5 |  0.062 % |
c ==============================================================================
c [1mFound solution: 2190336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19602 |  441534  1285950 |  147178   19592   930390    47.5 |  0.062 % |
c |     19704 |  441534  1285950 |  161895   19694   934818    47.5 |  0.063 % |
c |     19857 |  441534  1285950 |  178085   19847   941270    47.4 |  0.063 % |
c |     20085 |  441516  1285910 |  195893   20046   949831    47.4 |  0.067 % |
c ==============================================================================
c [1mFound solution: 2168832[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20272 |  441526  1285932 |  147175   20233   956629    47.3 |  0.067 % |
c |     20374 |  441526  1285932 |  161892   20335   960960    47.3 |  0.067 % |
c ==============================================================================
c [1mFound solution: 2154496[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20514 |  441534  1285950 |  147178   20475   967662    47.3 |  0.067 % |
c |     20614 |  441534  1285950 |  161895   20575   972104    47.2 |  0.068 % |
c |     20769 |  441534  1285950 |  178085   20730   978293    47.2 |  0.068 % |
c ==============================================================================
c [1mFound solution: 2117632[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20947 |  441540  1285963 |  147180   20908   986503    47.2 |  0.068 % |
c |     21047 |  441540  1285963 |  161898   21008   990370    47.1 |  0.069 % |
c |     21197 |  441540  1285963 |  178087   21158   997355    47.1 |  0.069 % |
c |     21422 |  441540  1285963 |  195896   21383  1007184    47.1 |  0.069 % |
c ==============================================================================
c [1mFound solution: 2114560[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21696 |  441549  1285983 |  147183   21657  1019168    47.1 |  0.069 % |
c ==============================================================================
c [1mFound solution: 1947648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21730 |  441557  1286002 |  147185   21691  1020931    47.1 |  0.069 % |
c ==============================================================================
c [1mFound solution: 1937408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21744 |  441566  1286025 |  147188   21705  1021695    47.1 |  0.069 % |
c |     21844 |  441566  1286025 |  161906   21805  1026027    47.1 |  0.070 % |
c ==============================================================================
c [1mFound solution: 1893376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21949 |  441574  1286045 |  147191   21910  1029023    47.0 |  0.070 % |
c |     22049 |  441574  1286045 |  161910   22010  1033110    46.9 |  0.071 % |
c |     22199 |  441574  1286045 |  178101   22160  1038508    46.9 |  0.071 % |
c ==============================================================================
c [1mFound solution: 1881088[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22225 |  441578  1286055 |  147192   22186  1039839    46.9 |  0.071 % |
c ==============================================================================
c [1mFound solution: 1748992[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22319 |  441590  1286083 |  147196   22280  1043648    46.8 |  0.071 % |
c |     22419 |  441590  1286083 |  161915   22380  1047923    46.8 |  0.072 % |
c ==============================================================================
c [1mFound solution: 1742848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22427 |  441602  1286111 |  147200   22388  1048258    46.8 |  0.072 % |
c ==============================================================================
c [1mFound solution: 1703936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22453 |  441605  1286118 |  147201   22414  1049690    46.8 |  0.072 % |
c |     22555 |  441605  1286118 |  161921   22516  1054292    46.8 |  0.074 % |
c |     22705 |  441605  1286118 |  178113   22666  1061590    46.8 |  0.074 % |
c |     22931 |  441605  1286118 |  195924   22892  1071090    46.8 |  0.074 % |
c |     23268 |  441605  1286118 |  215516   23229  1088121    46.8 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1601536[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23453 |  441608  1286125 |  147202   23414  1096341    46.8 |  0.074 % |
c |     23555 |  441608  1286125 |  161922   23516  1098789    46.7 |  0.074 % |
c |     23705 |  441608  1286125 |  178114   23666  1105702    46.7 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1558528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23717 |  441615  1286145 |  147205   23678  1106109    46.7 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1415168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23734 |  441623  1286164 |  147207   23695  1106742    46.7 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1394688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23797 |  441634  1286190 |  147211   23758  1109356    46.7 |  0.074 % |
c |     23897 |  441627  1286175 |  161932   23853  1112691    46.6 |  0.078 % |
c |     24047 |  441627  1286175 |  178125   24003  1119318    46.6 |  0.078 % |
c |     24272 |  441627  1286175 |  195937   24228  1131072    46.7 |  0.078 % |
c ==============================================================================
c [1mFound solution: 1338368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24446 |  441634  1286191 |  147211   24402  1138915    46.7 |  0.078 % |
c |     24547 |  441634  1286191 |  161932   24503  1145546    46.8 |  0.078 % |
c ==============================================================================
c [1mFound solution: 1326080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24682 |  441641  1286207 |  147213   24638  1150434    46.7 |  0.078 % |
c ==============================================================================
c [1mFound solution: 1316864[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24715 |  441649  1286225 |  147216   24671  1151706    46.7 |  0.078 % |
c |     24815 |  441649  1286225 |  161937   24771  1155628    46.7 |  0.080 % |
c ==============================================================================
c [1mFound solution: 1281024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24842 |  441658  1286247 |  147219   24798  1156594    46.6 |  0.080 % |
c ==============================================================================
c [1mFound solution: 1177600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24907 |  441665  1286263 |  147221   24863  1159311    46.6 |  0.080 % |
c |     25008 |  441665  1286263 |  161943   24964  1164044    46.6 |  0.081 % |
c |     25158 |  441665  1286263 |  178137   25114  1172031    46.7 |  0.081 % |
c |     25384 |  441665  1286263 |  195951   25340  1181976    46.6 |  0.081 % |
c ==============================================================================
c [1mFound solution: 1070080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25476 |  441676  1286287 |  147225   25432  1185106    46.6 |  0.081 % |
c ==============================================================================
c [1mFound solution: 1029120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25551 |  441653  1286224 |  147217   24181  1129685    46.7 |  0.081 % |
#### 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.45 0.81 0.86 2/54 29413
Raw data (stat): 29413 (runsolver) R 29412 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543150172 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.53 0.82 0.86 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14440 0 0 0 964 35 0 0 25 0 1 0 543150172 66211840 13353 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16165 13353 603 41 0 16124 0
vsize: 64660
[startup+20.0015 s]
Raw data (loadavg): 0.60 0.82 0.86 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14520 0 0 0 1963 35 0 0 25 0 1 0 543150172 66768896 13433 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16301 13433 603 41 0 16260 0
vsize: 65204
[startup+30.0016 s]
Raw data (loadavg): 0.66 0.83 0.86 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14520 0 0 0 2963 35 0 0 25 0 1 0 543150172 66768896 13433 4294967295 134512640 134672761 3221224528 3221223652 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16301 13433 603 41 0 16260 0
vsize: 65204
[startup+40.0021 s]
Raw data (loadavg): 0.72 0.83 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14528 0 0 0 3963 36 0 0 25 0 1 0 543150172 66768896 13441 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16301 13441 603 41 0 16260 0
vsize: 65204
[startup+50.0024 s]
Raw data (loadavg): 0.76 0.84 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14545 0 0 0 4963 36 0 0 25 0 1 0 543150172 66768896 13458 4294967295 134512640 134672761 3221224528 3221223632 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16301 13458 603 41 0 16260 0
vsize: 65204
[startup+60.0025 s]
Raw data (loadavg): 0.80 0.84 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14563 0 0 0 5963 36 0 0 25 0 1 0 543150172 66904064 13476 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16334 13476 603 41 0 16293 0
vsize: 65336
[startup+70.0034 s]
Raw data (loadavg): 0.83 0.85 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14578 0 0 0 6962 36 0 0 25 0 1 0 543150172 66904064 13491 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16334 13491 603 41 0 16293 0
vsize: 65336
[startup+80.0036 s]
Raw data (loadavg): 0.85 0.85 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14593 0 0 0 7962 37 0 0 25 0 1 0 543150172 67039232 13506 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 13506 603 41 0 16326 0
vsize: 65468
[startup+90.0035 s]
Raw data (loadavg): 0.87 0.86 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14609 0 0 0 8962 37 0 0 25 0 1 0 543150172 67039232 13522 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 13522 603 41 0 16326 0
vsize: 65468
[startup+100.003 s]
Raw data (loadavg): 0.89 0.86 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14631 0 0 0 9962 37 0 0 25 0 1 0 543150172 67174400 13544 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16400 13544 603 41 0 16359 0
vsize: 65600
[startup+110.004 s]
Raw data (loadavg): 0.91 0.86 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14654 0 0 0 10962 37 0 0 25 0 1 0 543150172 67174400 13567 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16400 13567 603 41 0 16359 0
vsize: 65600
[startup+120.005 s]
Raw data (loadavg): 0.92 0.87 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14669 0 0 0 11963 37 0 0 25 0 1 0 543150172 67309568 13582 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16433 13582 603 41 0 16392 0
vsize: 65732
[startup+130.005 s]
Raw data (loadavg): 0.93 0.87 0.87 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14685 0 0 0 12963 37 0 0 25 0 1 0 543150172 67309568 13598 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16433 13598 603 41 0 16392 0
vsize: 65732
[startup+140.005 s]
Raw data (loadavg): 0.94 0.88 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14704 0 0 0 13963 37 0 0 25 0 1 0 543150172 67444736 13617 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16466 13617 603 41 0 16425 0
vsize: 65864
[startup+150.005 s]
Raw data (loadavg): 0.95 0.88 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14720 0 0 0 14963 37 0 0 25 0 1 0 543150172 67579904 13633 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16499 13633 603 41 0 16458 0
vsize: 65996
[startup+160.005 s]
Raw data (loadavg): 0.96 0.88 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14735 0 0 0 15963 37 0 0 25 0 1 0 543150172 67579904 13648 4294967295 134512640 134672761 3221224528 3221223672 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16499 13648 603 41 0 16458 0
vsize: 65996
[startup+170.005 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14748 0 0 0 16963 37 0 0 25 0 1 0 543150172 67579904 13661 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16499 13661 603 41 0 16458 0
vsize: 65996
[startup+180.005 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14761 0 0 0 17963 37 0 0 25 0 1 0 543150172 67715072 13674 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16532 13674 603 41 0 16491 0
vsize: 66128
[startup+190.006 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14776 0 0 0 18963 37 0 0 25 0 1 0 543150172 67715072 13689 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16532 13689 603 41 0 16491 0
vsize: 66128
[startup+200.006 s]
Raw data (loadavg): 0.98 0.89 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14790 0 0 0 19963 37 0 0 25 0 1 0 543150172 67846144 13703 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16564 13703 603 41 0 16523 0
vsize: 66256
[startup+210.007 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14801 0 0 0 20964 37 0 0 25 0 1 0 543150172 67846144 13714 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16564 13714 603 41 0 16523 0
vsize: 66256
[startup+220.008 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14813 0 0 0 21964 38 0 0 25 0 1 0 543150172 67846144 13726 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16564 13726 603 41 0 16523 0
vsize: 66256
[startup+230.007 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14829 0 0 0 22964 38 0 0 25 0 1 0 543150172 67989504 13742 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16599 13742 603 41 0 16558 0
vsize: 66396
[startup+240.007 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14848 0 0 0 23964 38 0 0 25 0 1 0 543150172 67989504 13761 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16599 13761 603 41 0 16558 0
vsize: 66396
[startup+250.007 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14863 0 0 0 24964 38 0 0 25 0 1 0 543150172 68149248 13776 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16638 13776 603 41 0 16597 0
vsize: 66552
[startup+260.008 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14877 0 0 0 25965 38 0 0 25 0 1 0 543150172 68149248 13790 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16638 13790 603 41 0 16597 0
vsize: 66552
[startup+270.008 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14891 0 0 0 26965 38 0 0 25 0 1 0 543150172 68149248 13804 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16638 13804 603 41 0 16597 0
vsize: 66552
[startup+280.008 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14902 0 0 0 27965 38 0 0 25 0 1 0 543150172 68280320 13815 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16670 13815 603 41 0 16629 0
vsize: 66680
[startup+290.008 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14917 0 0 0 28965 38 0 0 25 0 1 0 543150172 68280320 13830 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16670 13830 603 41 0 16629 0
vsize: 66680
[startup+300.008 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14930 0 0 0 29965 38 0 0 25 0 1 0 543150172 68415488 13843 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16703 13843 603 41 0 16662 0
vsize: 66812
[startup+310.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14954 0 0 0 30965 38 0 0 25 0 1 0 543150172 68567040 13867 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16740 13867 603 41 0 16699 0
vsize: 66960
[startup+320.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14961 0 0 0 31965 38 0 0 25 0 1 0 543150172 68567040 13874 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16740 13874 603 41 0 16699 0
vsize: 66960
[startup+330.009 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14978 0 0 0 32965 38 0 0 25 0 1 0 543150172 68567040 13891 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16740 13891 603 41 0 16699 0
vsize: 66960
[startup+340.01 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 14992 0 0 0 33965 38 0 0 25 0 1 0 543150172 68702208 13905 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16773 13905 603 41 0 16732 0
vsize: 67092
[startup+350.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15009 0 0 0 34966 38 0 0 25 0 1 0 543150172 68702208 13922 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16773 13922 603 41 0 16732 0
vsize: 67092
[startup+360.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15020 0 0 0 35966 38 0 0 25 0 1 0 543150172 68833280 13933 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16805 13933 603 41 0 16764 0
vsize: 67220
[startup+370.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15032 0 0 0 36966 38 0 0 25 0 1 0 543150172 68833280 13945 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16805 13945 603 41 0 16764 0
vsize: 67220
[startup+380.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15047 0 0 0 37966 38 0 0 25 0 1 0 543150172 68964352 13960 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16837 13960 603 41 0 16796 0
vsize: 67348
[startup+390.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15060 0 0 0 38966 39 0 0 25 0 1 0 543150172 68964352 13973 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16837 13973 603 41 0 16796 0
vsize: 67348
[startup+400.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15069 0 0 0 39966 39 0 0 25 0 1 0 543150172 68964352 13982 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16837 13982 603 41 0 16796 0
vsize: 67348
[startup+410.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15081 0 0 0 40966 39 0 0 25 0 1 0 543150172 69095424 13994 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16869 13994 603 41 0 16828 0
vsize: 67476
[startup+420.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15102 0 0 0 41966 39 0 0 25 0 1 0 543150172 69095424 14015 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16869 14015 603 41 0 16828 0
vsize: 67476
[startup+430.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15117 0 0 0 42965 40 0 0 25 0 1 0 543150172 69259264 14030 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16909 14030 603 41 0 16868 0
vsize: 67636
[startup+440.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15132 0 0 0 43965 40 0 0 25 0 1 0 543150172 69259264 14045 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16909 14045 603 41 0 16868 0
vsize: 67636
[startup+450.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15152 0 0 0 44965 40 0 0 25 0 1 0 543150172 69390336 14065 4294967295 134512640 134672761 3221224528 3221223652 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16941 14065 603 41 0 16900 0
vsize: 67764
[startup+460.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15164 0 0 0 45965 40 0 0 25 0 1 0 543150172 69390336 14077 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16941 14077 603 41 0 16900 0
vsize: 67764
[startup+470.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15170 0 0 0 46966 40 0 0 25 0 1 0 543150172 69390336 14083 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16941 14083 603 41 0 16900 0
vsize: 67764
[startup+480.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15183 0 0 0 47966 40 0 0 25 0 1 0 543150172 69521408 14096 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16973 14096 603 41 0 16932 0
vsize: 67892
[startup+490.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15203 0 0 0 48966 40 0 0 25 0 1 0 543150172 69521408 14116 4294967295 134512640 134672761 3221224528 3221223632 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16973 14116 603 41 0 16932 0
vsize: 67892
[startup+500.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15216 0 0 0 49966 40 0 0 25 0 1 0 543150172 69652480 14129 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17005 14129 603 41 0 16964 0
vsize: 68020
[startup+510.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15221 0 0 0 50966 40 0 0 25 0 1 0 543150172 69652480 14134 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17005 14134 603 41 0 16964 0
vsize: 68020
[startup+520.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15229 0 0 0 51966 40 0 0 25 0 1 0 543150172 69652480 14142 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17005 14142 603 41 0 16964 0
vsize: 68020
[startup+530.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15240 0 0 0 52966 40 0 0 25 0 1 0 543150172 69779456 14153 4294967295 134512640 134672761 3221224528 3221223632 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17036 14153 603 41 0 16995 0
vsize: 68144
[startup+540.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15256 0 0 0 53966 40 0 0 25 0 1 0 543150172 69779456 14169 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17036 14169 603 41 0 16995 0
vsize: 68144
[startup+550.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15265 0 0 0 54966 40 0 0 25 0 1 0 543150172 69779456 14178 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17036 14178 603 41 0 16995 0
vsize: 68144
[startup+560.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15273 0 0 0 55966 40 0 0 25 0 1 0 543150172 69906432 14186 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17067 14186 603 41 0 17026 0
vsize: 68268
[startup+570.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15286 0 0 0 56967 40 0 0 25 0 1 0 543150172 69906432 14199 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17067 14199 603 41 0 17026 0
vsize: 68268
[startup+580.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15294 0 0 0 57967 40 0 0 25 0 1 0 543150172 69906432 14207 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17067 14207 603 41 0 17026 0
vsize: 68268
[startup+590.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15306 0 0 0 58967 40 0 0 25 0 1 0 543150172 70037504 14219 4294967295 134512640 134672761 3221224528 3221223696 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17099 14219 603 41 0 17058 0
vsize: 68396
[startup+600.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15315 0 0 0 59967 40 0 0 25 0 1 0 543150172 70037504 14228 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17099 14228 603 41 0 17058 0
vsize: 68396
[startup+610.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15333 0 0 0 60967 40 0 0 25 0 1 0 543150172 70189056 14246 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17136 14246 603 41 0 17095 0
vsize: 68544
[startup+620.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15339 0 0 0 61968 40 0 0 25 0 1 0 543150172 70189056 14252 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17136 14252 603 41 0 17095 0
vsize: 68544
[startup+630.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15349 0 0 0 62968 41 0 0 25 0 1 0 543150172 70189056 14262 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17136 14262 603 41 0 17095 0
vsize: 68544
[startup+640.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15361 0 0 0 63968 41 0 0 25 0 1 0 543150172 70189056 14274 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17136 14274 603 41 0 17095 0
vsize: 68544
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15371 0 0 0 64968 41 0 0 25 0 1 0 543150172 70320128 14284 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17168 14284 603 41 0 17127 0
vsize: 68672
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15388 0 0 0 65968 41 0 0 25 0 1 0 543150172 70320128 14301 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17168 14301 603 41 0 17127 0
vsize: 68672
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15402 0 0 0 66968 41 0 0 25 0 1 0 543150172 70459392 14315 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17202 14315 603 41 0 17161 0
vsize: 68808
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15414 0 0 0 67968 41 0 0 25 0 1 0 543150172 70459392 14327 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17202 14327 603 41 0 17161 0
vsize: 68808
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15425 0 0 0 68968 41 0 0 25 0 1 0 543150172 70459392 14338 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17202 14338 603 41 0 17161 0
vsize: 68808
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15452 0 0 0 69968 41 0 0 25 0 1 0 543150172 70746112 14365 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14365 603 41 0 17231 0
vsize: 69088
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15453 0 0 0 70969 41 0 0 25 0 1 0 543150172 70746112 14366 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14366 603 41 0 17231 0
vsize: 69088
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15455 0 0 0 71969 41 0 0 25 0 1 0 543150172 70746112 14368 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14368 603 41 0 17231 0
vsize: 69088
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15465 0 0 0 72969 41 0 0 25 0 1 0 543150172 70746112 14378 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14378 603 41 0 17231 0
vsize: 69088
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15474 0 0 0 73969 41 0 0 25 0 1 0 543150172 70746112 14387 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14387 603 41 0 17231 0
vsize: 69088
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15482 0 0 0 74969 41 0 0 25 0 1 0 543150172 70746112 14395 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14395 603 41 0 17231 0
vsize: 69088
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15495 0 0 0 75969 42 0 0 25 0 1 0 543150172 70868992 14408 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 14408 603 41 0 17261 0
vsize: 69208
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15503 0 0 0 76969 42 0 0 25 0 1 0 543150172 70868992 14416 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 14416 603 41 0 17261 0
vsize: 69208
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15515 0 0 0 77970 42 0 0 25 0 1 0 543150172 70868992 14428 4294967295 134512640 134672761 3221224528 3221223696 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 14428 603 41 0 17261 0
vsize: 69208
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15528 0 0 0 78970 42 0 0 25 0 1 0 543150172 71000064 14441 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17334 14441 603 41 0 17293 0
vsize: 69336
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15539 0 0 0 79969 42 0 0 25 0 1 0 543150172 71000064 14452 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17334 14452 603 41 0 17293 0
vsize: 69336
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15556 0 0 0 80970 42 0 0 25 0 1 0 543150172 71155712 14469 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17372 14469 603 41 0 17331 0
vsize: 69488
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15568 0 0 0 81970 42 0 0 25 0 1 0 543150172 71155712 14481 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17372 14481 603 41 0 17331 0
vsize: 69488
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15585 0 0 0 82970 42 0 0 25 0 1 0 543150172 71278592 14498 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17402 14498 603 41 0 17361 0
vsize: 69608
[startup+840.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15595 0 0 0 83970 42 0 0 25 0 1 0 543150172 71278592 14508 4294967295 134512640 134672761 3221224528 3221223860 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17402 14508 603 41 0 17361 0
vsize: 69608
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15604 0 0 0 84970 42 0 0 25 0 1 0 543150172 71278592 14517 4294967295 134512640 134672761 3221224528 3221223632 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17402 14517 603 41 0 17361 0
vsize: 69608
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15613 0 0 0 85970 42 0 0 25 0 1 0 543150172 71278592 14526 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17402 14526 603 41 0 17361 0
vsize: 69608
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15627 0 0 0 86971 42 0 0 25 0 1 0 543150172 71409664 14540 4294967295 134512640 134672761 3221224528 3221223632 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17434 14540 603 41 0 17393 0
vsize: 69736
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15634 0 0 0 87971 42 0 0 25 0 1 0 543150172 71409664 14547 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17434 14547 603 41 0 17393 0
vsize: 69736
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15648 0 0 0 88971 42 0 0 25 0 1 0 543150172 71557120 14561 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17470 14561 603 41 0 17429 0
vsize: 69880
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15663 0 0 0 89971 42 0 0 25 0 1 0 543150172 71557120 14576 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17470 14576 603 41 0 17429 0
vsize: 69880
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15670 0 0 0 90971 42 0 0 25 0 1 0 543150172 71557120 14583 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17470 14583 603 41 0 17429 0
vsize: 69880
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15683 0 0 0 91971 42 0 0 25 0 1 0 543150172 71671808 14596 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17498 14596 603 41 0 17457 0
vsize: 69992
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15700 0 0 0 92971 43 0 0 25 0 1 0 543150172 71823360 14613 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17535 14613 603 41 0 17494 0
vsize: 70140
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15706 0 0 0 93972 43 0 0 25 0 1 0 543150172 71823360 14619 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17535 14619 603 41 0 17494 0
vsize: 70140
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15718 0 0 0 94972 43 0 0 25 0 1 0 543150172 71823360 14631 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17535 14631 603 41 0 17494 0
vsize: 70140
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15726 0 0 0 95972 43 0 0 25 0 1 0 543150172 71823360 14639 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17535 14639 603 41 0 17494 0
vsize: 70140
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15737 0 0 0 96972 43 0 0 25 0 1 0 543150172 71946240 14650 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17565 14650 603 41 0 17524 0
vsize: 70260
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15747 0 0 0 97972 43 0 0 25 0 1 0 543150172 71946240 14660 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17565 14660 603 41 0 17524 0
vsize: 70260
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15756 0 0 0 98972 43 0 0 25 0 1 0 543150172 71946240 14669 4294967295 134512640 134672761 3221224528 3221223680 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17565 14669 603 41 0 17524 0
vsize: 70260
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15764 0 0 0 99972 43 0 0 25 0 1 0 543150172 72077312 14677 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17597 14677 603 41 0 17556 0
vsize: 70388
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15775 0 0 0 100972 43 0 0 25 0 1 0 543150172 72077312 14688 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17597 14688 603 41 0 17556 0
vsize: 70388
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15784 0 0 0 101972 43 0 0 25 0 1 0 543150172 72077312 14697 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17597 14697 603 41 0 17556 0
vsize: 70388
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15801 0 0 0 102972 43 0 0 25 0 1 0 543150172 72208384 14714 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14714 603 41 0 17588 0
vsize: 70516
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15811 0 0 0 103973 43 0 0 25 0 1 0 543150172 72208384 14724 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14724 603 41 0 17588 0
vsize: 70516
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15818 0 0 0 104973 44 0 0 25 0 1 0 543150172 72208384 14731 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14731 603 41 0 17588 0
vsize: 70516
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15826 0 0 0 105973 44 0 0 25 0 1 0 543150172 72208384 14739 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14739 603 41 0 17588 0
vsize: 70516
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15841 0 0 0 106973 44 0 0 25 0 1 0 543150172 72368128 14754 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17668 14754 603 41 0 17627 0
vsize: 70672
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15848 0 0 0 107973 44 0 0 25 0 1 0 543150172 72368128 14761 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17668 14761 603 41 0 17627 0
vsize: 70672
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15858 0 0 0 108973 44 0 0 25 0 1 0 543150172 72368128 14771 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17668 14771 603 41 0 17627 0
vsize: 70672
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15864 0 0 0 109974 44 0 0 25 0 1 0 543150172 72368128 14777 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17668 14777 603 41 0 17627 0
vsize: 70672
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15872 0 0 0 110974 44 0 0 25 0 1 0 543150172 72491008 14785 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17698 14785 603 41 0 17657 0
vsize: 70792
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15883 0 0 0 111974 44 0 0 25 0 1 0 543150172 72491008 14796 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17698 14796 603 41 0 17657 0
vsize: 70792
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15889 0 0 0 112974 44 0 0 25 0 1 0 543150172 72491008 14802 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17698 14802 603 41 0 17657 0
vsize: 70792
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15899 0 0 0 113974 44 0 0 25 0 1 0 543150172 72626176 14812 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14812 603 41 0 17690 0
vsize: 70924
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15909 0 0 0 114974 44 0 0 25 0 1 0 543150172 72626176 14822 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14822 603 41 0 17690 0
vsize: 70924
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15914 0 0 0 115974 44 0 0 25 0 1 0 543150172 72626176 14827 4294967295 134512640 134672761 3221224528 3221223652 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14827 603 41 0 17690 0
vsize: 70924
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15921 0 0 0 116975 44 0 0 25 0 1 0 543150172 72626176 14834 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14834 603 41 0 17690 0
vsize: 70924
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15929 0 0 0 117975 44 0 0 25 0 1 0 543150172 72626176 14842 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14842 603 41 0 17690 0
vsize: 70924
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15941 0 0 0 118975 45 0 0 25 0 1 0 543150172 72757248 14854 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17763 14854 603 41 0 17722 0
vsize: 71052
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29413
Raw data (stat): 29413 (minisat+) R 29412 28546 28545 0 -1 0 15948 0 0 0 119975 45 0 0 25 0 1 0 543150172 72757248 14861 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17763 14861 603 41 0 17722 0
vsize: 71052
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29413
Raw data (stat): 29413 (minisat+) Z 29412 28546 28545 0 -1 12 15951 0 0 0 119975 48 0 0 25 0 1 0 543150172 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.24
CPU user time (s): 1199.76
CPU system time (s): 0.482926
CPU usage (%): 100.014
Max. virtual memory (Kb): 71052
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####