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/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-5.opb
MD5SUM	6049145b9f1adfd7114adf044503d587
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2642
Optimality of the best value was proved	NO
Number of terms in the objective function	748
Biggest coefficient in the objective function	240
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	33855
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	240
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	33855
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02984
Number of variables	907
Total number of constraints	1309
Number of constraints which are clauses	126
Number of constraints which are cardinality constraints (but not clauses)	1183
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	134
Trace number 6034

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-14 03:11:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4494 boxname=wulflinc9 idbench=358 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6049145b9f1adfd7114adf044503d587  /oldhome/oroussel/tmp/wulflinc9/normalized-ws97-5.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc9/normalized-ws97-5.opb /oldhome/oroussel/tmp/wulflinc9/normalized-ws97-5.opb
IDLAUNCH: 4494
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        892820 kB
Buffers:         36284 kB
Cached:          85416 kB
SwapCached:        564 kB
Active:          54068 kB
Inactive:        71112 kB
HighTotal:      131008 kB
HighFree:        41636 kB
LowTotal:       903652 kB
LowFree:        851184 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11100 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:31:55 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4494 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 661 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: ##################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .............................................................................................................................
c ---[ 660]---> BDD-cost: 3184
c ---[ 659]---> BDD-cost: 3184
c ---[ 658]---> BDD-cost: 3184
c ---[ 657]---> BDD-cost: 3127
c ---[ 656]---> BDD-cost: 4127
c ---[ 655]---> BDD-cost: 4164
c ---[ 654]---> BDD-cost: 4164
c ---[ 653]---> BDD-cost:  264
c ---[ 652]---> BDD-cost:  264
c ---[ 651]---> BDD-cost:  264
c ---[ 650]---> BDD-cost:  253
c ---[ 649]---> BDD-cost:  476
c ---[ 648]---> BDD-cost:  490
c ---[ 647]---> BDD-cost:  490
c ---[ 645]---> BDD-cost:    5
c ---[ 643]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:    5
c ---[ 639]---> BDD-cost:    3
c ---[ 637]---> BDD-cost:    5
c ---[ 635]---> BDD-cost:    3
c ---[ 633]---> BDD-cost:    5
c ---[ 631]---> BDD-cost:    3
c ---[ 629]---> BDD-cost:    5
c ---[ 627]---> BDD-cost:    3
c ---[ 625]---> BDD-cost:    5
c ---[ 623]---> BDD-cost:    3
c ---[ 621]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    5
c ---[ 617]---> BDD-cost:    3
c ---[ 615]---> BDD-cost:    5
c ---[ 613]---> BDD-cost:    3
c ---[ 611]---> BDD-cost:    5
c ---[ 609]---> BDD-cost:    3
c ---[ 607]---> BDD-cost:    3
c ---[ 605]---> BDD-cost:    5
c ---[ 603]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    5
c ---[ 599]---> BDD-cost:    3
c ---[ 597]---> BDD-cost:    5
c ---[ 595]---> BDD-cost:    3
c ---[ 593]---> BDD-cost:    5
c ---[ 591]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    5
c ---[ 587]---> BDD-cost:    3
c ---[ 585]---> BDD-cost:    5
c ---[ 583]---> BDD-cost:    3
c ---[ 581]---> BDD-cost:    5
c ---[ 579]---> BDD-cost:    3
c ---[ 577]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    3
c ---[ 573]---> BDD-cost:    5
c ---[ 571]---> BDD-cost:    3
c ---[ 569]---> BDD-cost:    5
c ---[ 567]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 563]---> BDD-cost:    3
c ---[ 561]---> BDD-cost:    5
c ---[ 559]---> BDD-cost:    3
c ---[ 557]---> BDD-cost:    5
c ---[ 555]---> BDD-cost:    3
c ---[ 553]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    3
c ---[ 549]---> BDD-cost:    5
c ---[ 547]---> BDD-cost:    3
c ---[ 545]---> BDD-cost:    5
c ---[ 543]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    5
c ---[ 539]---> BDD-cost:    3
c ---[ 537]---> BDD-cost:    5
c ---[ 535]---> BDD-cost:    3
c ---[ 533]---> BDD-cost:    5
c ---[ 531]---> BDD-cost:    3
c ---[ 529]---> BDD-cost:    5
c ---[ 527]---> BDD-cost:    3
c ---[ 525]---> BDD-cost:    5
c ---[ 523]---> BDD-cost:    3
c ---[ 521]---> BDD-cost:    5
c ---[ 519]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    5
c ---[ 515]---> BDD-cost:    3
c ---[ 513]---> BDD-cost:    5
c ---[ 511]---> BDD-cost:    3
c ---[ 509]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    3
c ---[ 505]---> BDD-cost:    5
c ---[ 503]---> BDD-cost:    3
c ---[ 501]---> BDD-cost:    5
c ---[ 499]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:    5
c ---[ 495]---> BDD-cost:    3
c ---[ 493]---> BDD-cost:    5
c ---[ 491]---> BDD-cost:    3
c ---[ 489]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    3
c ---[ 485]---> BDD-cost:    5
c ---[ 483]---> BDD-cost:    3
c ---[ 481]---> BDD-cost:    5
c ---[ 479]---> BDD-cost:    3
c ---[ 477]---> BDD-cost:    5
c ---[ 475]---> BDD-cost:    3
c ---[ 473]---> BDD-cost:    5
c ---[ 471]---> BDD-cost:    3
c ---[ 469]---> BDD-cost:    5
c ---[ 467]---> BDD-cost:    3
c ---[ 465]---> BDD-cost:    3
c ---[ 463]---> BDD-cost:    5
c ---[ 461]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    5
c ---[ 457]---> BDD-cost:    3
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 449]---> BDD-cost:    3
c ---[ 447]---> BDD-cost:    5
c ---[ 445]---> BDD-cost:    3
c ---[ 443]---> BDD-cost:    5
c ---[ 441]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:    5
c ---[ 437]---> BDD-cost:    3
c ---[ 435]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:    5
c ---[ 425]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    5
c ---[ 421]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    5
c ---[ 417]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    5
c ---[ 413]---> BDD-cost:    3
c ---[ 411]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    3
c ---[ 407]---> BDD-cost:    3
c ---[ 405]---> BDD-cost:    5
c ---[ 403]---> BDD-cost:    3
c ---[ 401]---> BDD-cost:    3
c ---[ 399]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    3
c ---[ 395]---> BDD-cost:    5
c ---[ 393]---> BDD-cost:    3
c ---[ 391]---> BDD-cost:    5
c ---[ 389]---> BDD-cost:    3
c ---[ 387]---> BDD-cost:    5
c ---[ 385]---> BDD-cost:    3
c ---[ 383]---> BDD-cost:    5
c ---[ 381]---> BDD-cost:    3
c ---[ 379]---> BDD-cost:    5
c ---[ 377]---> BDD-cost:    3
c ---[ 375]---> BDD-cost:    5
c ---[ 373]---> BDD-cost:    3
c ---[ 371]---> BDD-cost:    5
c ---[ 369]---> BDD-cost:    3
c ---[ 367]---> BDD-cost:    5
c ---[ 365]---> BDD-cost:    3
c ---[ 363]---> BDD-cost:    5
c ---[ 361]---> BDD-cost:    3
c ---[ 359]---> BDD-cost:    5
c ---[ 357]---> BDD-cost:    3
c ---[ 355]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    3
c ---[ 351]---> BDD-cost:    5
c ---[ 349]---> BDD-cost:    3
c ---[ 347]---> BDD-cost:    5
c ---[ 345]---> BDD-cost:    3
c ---[ 343]---> BDD-cost:    5
c ---[ 341]---> BDD-cost:    3
c ---[ 339]---> BDD-cost:    5
c ---[ 337]---> BDD-cost:    3
c ---[ 335]---> BDD-cost:    5
c ---[ 333]---> BDD-cost:    3
c ---[ 327]---> BDD-cost:    5
c ---[ 325]---> BDD-cost:    3
c ---[ 323]---> BDD-cost:    5
c ---[ 321]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    5
c ---[ 317]---> BDD-cost:    3
c ---[ 315]---> BDD-cost:    5
c ---[ 313]---> BDD-cost:    3
c ---[ 311]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    3
c ---[ 307]---> BDD-cost:    5
c ---[ 305]---> BDD-cost:    3
c ---[ 303]---> BDD-cost:    5
c ---[ 301]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 297]---> BDD-cost:    3
c ---[ 295]---> BDD-cost:    5
c ---[ 293]---> BDD-cost:    3
c ---[ 291]---> BDD-cost:    5
c ---[ 289]---> BDD-cost:    3
c ---[ 287]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    3
c ---[ 283]---> BDD-cost:    5
c ---[ 281]---> BDD-cost:    3
c ---[ 279]---> BDD-cost:    5
c ---[ 277]---> BDD-cost:    3
c ---[ 275]---> BDD-cost:    3
c ---[ 273]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    5
c ---[ 267]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    5
c ---[ 255]---> BDD-cost:    3
c ---[ 253]---> BDD-cost:    5
c ---[ 251]---> BDD-cost:    3
c ---[ 249]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:    3
c ---[ 245]---> BDD-cost:    5
c ---[ 243]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    5
c ---[ 239]---> BDD-cost:    3
c ---[ 237]---> BDD-cost:    5
c ---[ 235]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    5
c ---[ 231]---> BDD-cost:    3
c ---[ 229]---> BDD-cost:    5
c ---[ 227]---> BDD-cost:    3
c ---[ 225]---> BDD-cost:    5
c ---[ 223]---> BDD-cost:    3
c ---[ 221]---> BDD-cost:    5
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> BDD-cost:    5
c ---[ 215]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    5
c ---[ 211]---> BDD-cost:    3
c ---[ 209]---> BDD-cost:    5
c ---[ 207]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    5
c ---[ 203]---> BDD-cost:    3
c ---[ 201]---> BDD-cost:    5
c ---[ 199]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    5
c ---[ 195]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    5
c ---[ 191]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    5
c ---[ 187]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    5
c ---[ 183]---> BDD-cost:    3
c ---[ 181]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    3
c ---[ 177]---> BDD-cost:    5
c ---[ 175]---> BDD-cost:    3
c ---[ 173]---> BDD-cost:    5
c ---[ 171]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    5
c ---[ 165]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    5
c ---[ 159]---> BDD-cost:    3
c ---[ 157]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    5
c ---[ 151]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    3
c ---[ 145]---> BDD-cost:    5
c ---[ 143]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    5
c ---[ 139]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    5
c ---[ 131]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    5
c ---[ 127]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  135304   403409 |   45101       0        0     nan |  0.000 % |
c |       100 |  135304   403409 |   49611     100     9086    90.9 |  0.947 % |
c ==============================================================================
c [1mFound solution: 4956[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30425     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       135 |  198671   551567 |   66223     135     9297    68.9 |  0.947 % |
c |       235 |  198560   551316 |   72845     234    10391    44.4 |  0.560 % |
c |       385 |  195114   543424 |   80129     316    10681    33.8 |  2.414 % |
c |       610 |  190417   532586 |   88142     438    11126    25.4 |  5.064 % |
c |       955 |  185411   520991 |   96957     688    17050    24.8 |  7.954 % |
c |      1461 |  181632   512256 |  106652    1095    19319    17.6 | 10.127 % |
c |      2220 |  180253   509062 |  117318    1796    45024    25.1 | 10.923 % |
c |      3359 |  180241   509035 |  129049    2933    56845    19.4 | 10.929 % |
c |      5067 |  178333   504610 |  141954    4565   103112    22.6 | 12.048 % |
c |      7629 |  178333   504610 |  156150    7127   156417    21.9 | 12.048 % |
c |     11473 |  178305   504546 |  171765   10962   346002    31.6 | 12.062 % |
c |     17243 |  177011   501549 |  188941   16647   449140    27.0 | 12.819 % |
c |     25892 |  176265   499806 |  207836   25219   750685    29.8 | 13.279 % |
c |     38868 |  176201   499660 |  228619   38190  1196362    31.3 | 13.316 % |
c |     58329 |  176197   499651 |  251481   57649  2304801    40.0 | 13.317 % |
c ==============================================================================
c [1mFound solution: 4685[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63639 |  176609   500718 |   58869   62959  2947135    46.8 | 13.317 % |
c |     63741 |  176609   500718 |   64755   63061  2953100    46.8 | 13.543 % |
c |     63894 |  176609   500718 |   71231   63214  2961567    46.8 | 13.543 % |
c |     64120 |  176609   500718 |   78354   63440  2975855    46.9 | 13.543 % |
c |     64457 |  176609   500718 |   86190   63777  2986754    46.8 | 13.543 % |
c |     64963 |  176587   500668 |   94809   64282  3011376    46.8 | 13.554 % |
c |     65727 |  176587   500668 |  104290   65046  3077440    47.3 | 13.554 % |
c |     66866 |  176587   500668 |  114719   66185  3122708    47.2 | 13.554 % |
c |     68574 |  176587   500668 |  126190   67893  3201834    47.2 | 13.554 % |
c ==============================================================================
c [1mFound solution: 4470[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70270 |  176554   500600 |   58851   69588  3274794    47.1 | 13.554 % |
c |     70370 |  176554   500600 |   64736   17480   989767    56.6 | 13.634 % |
c |     70520 |  176554   500600 |   71209   17630   995638    56.5 | 13.634 % |
c |     70746 |  176554   500600 |   78330   17856  1000217    56.0 | 13.634 % |
c ==============================================================================
c [1mFound solution: 4256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70795 |  176579   500666 |   58859   17905  1000629    55.9 | 13.634 % |
c |     70895 |  176579   500666 |   64744   18005  1005325    55.8 | 13.632 % |
c |     71046 |  176579   500666 |   71219   18156  1010044    55.6 | 13.632 % |
c |     71275 |  176522   500534 |   78341   18382  1012981    55.1 | 13.666 % |
c |     71613 |  176522   500534 |   86175   18720  1015432    54.2 | 13.666 % |
c |     72120 |  176522   500534 |   94793   19227  1030428    53.6 | 13.666 % |
c ==============================================================================
c [1mFound solution: 3855[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72759 |  176565   500649 |   58855   19866  1045801    52.6 | 13.666 % |
c |     72859 |  176565   500649 |   64740   19966  1050025    52.6 | 13.661 % |
c |     73009 |  176565   500649 |   71214   20116  1054667    52.4 | 13.661 % |
c |     73234 |  176565   500649 |   78336   20341  1068788    52.5 | 13.661 % |
c |     73574 |  176565   500649 |   86169   20681  1079331    52.2 | 13.661 % |
c |     74080 |  176565   500649 |   94786   21187  1110656    52.4 | 13.661 % |
c |     74839 |  176565   500649 |  104265   21946  1151114    52.5 | 13.661 % |
c ==============================================================================
c [1mFound solution: 3758[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75041 |  176920   501512 |   58973   22148  1160787    52.4 | 13.661 % |
c |     75143 |  176920   501512 |   64870   22250  1166820    52.4 | 13.869 % |
c |     75293 |  176920   501512 |   71357   22400  1170760    52.3 | 13.869 % |
c |     75518 |  176920   501512 |   78493   22625  1179462    52.1 | 13.869 % |
c |     75855 |  176920   501512 |   86342   22962  1195236    52.1 | 13.869 % |
c |     76362 |  176920   501512 |   94976   23469  1228074    52.3 | 13.869 % |
c ==============================================================================
c [1mFound solution: 3557[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76534 |  177139   502047 |   59046   23641  1236168    52.3 | 13.869 % |
c |     76637 |  177139   502047 |   64950   23744  1242033    52.3 | 13.988 % |
c |     76790 |  177139   502047 |   71445   23897  1248477    52.2 | 13.988 % |
c |     77016 |  177139   502047 |   78590   24123  1260565    52.3 | 13.988 % |
c ==============================================================================
c [1mFound solution: 3456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77203 |  177159   502101 |   59053   24310  1267226    52.1 | 13.988 % |
c |     77303 |  177159   502101 |   64958   24410  1268190    52.0 | 13.987 % |
c |     77454 |  177159   502101 |   71454   24561  1269326    51.7 | 13.987 % |
c |     77680 |  177159   502101 |   78599   24787  1270540    51.3 | 13.987 % |
c |     78018 |  177159   502101 |   86459   25125  1284282    51.1 | 13.987 % |
c |     78524 |  177159   502101 |   95105   25631  1301635    50.8 | 13.987 % |
c |     79287 |  177159   502101 |  104615   26394  1355111    51.3 | 13.987 % |
c |     80428 |  177159   502101 |  115077   27535  1465511    53.2 | 13.987 % |
c ==============================================================================
c [1mFound solution: 3356[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81724 |  177166   502121 |   59055   28831  1532524    53.2 | 13.987 % |
c |     81824 |  177166   502121 |   64960   28931  1533887    53.0 | 13.988 % |
c |     81975 |  177166   502121 |   71456   29082  1539186    52.9 | 13.988 % |
c |     82204 |  177166   502121 |   78602   29311  1547487    52.8 | 13.988 % |
c |     82541 |  177166   502121 |   86462   29648  1566787    52.8 | 13.988 % |
c |     83050 |  177166   502121 |   95108   30157  1587318    52.6 | 13.988 % |
c |     83810 |  177166   502121 |  104619   30917  1664294    53.8 | 13.988 % |
c ==============================================================================
c [1mFound solution: 3351[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83955 |  177172   502135 |   59057   31062  1672532    53.8 | 13.988 % |
c |     84055 |  177172   502135 |   64962   31162  1678961    53.9 | 13.989 % |
c |     84205 |  177172   502135 |   71458   31312  1688008    53.9 | 13.989 % |
c |     84431 |  177172   502135 |   78604   31538  1701338    53.9 | 13.989 % |
c |     84770 |  177172   502135 |   86465   31877  1722913    54.0 | 13.989 % |
c |     85276 |  177172   502135 |   95111   32383  1746752    53.9 | 13.989 % |
c |     86035 |  177172   502135 |  104623   33142  1787689    53.9 | 13.989 % |
c |     87175 |  177172   502135 |  115085   34282  1865456    54.4 | 13.989 % |
c |     88883 |  177172   502135 |  126593   35990  1948262    54.1 | 13.989 % |
c |     91445 |  177172   502135 |  139253   38552  1999355    51.9 | 13.989 % |
c |     95293 |  177172   502135 |  153178   42400  2287146    53.9 | 13.989 % |
c |    101059 |  177172   502135 |  168496   48166  2626198    54.5 | 13.989 % |
c |    109708 |  177172   502135 |  185346   56815  3294504    58.0 | 13.989 % |
c |    122683 |  177166   502121 |  203880   69788  4387015    62.9 | 13.992 % |
c |    142145 |  177166   502121 |  224268   89250  5041971    56.5 | 13.992 % |
c ==============================================================================
c [1mFound solution: 3350[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    147746 |  177174   502139 |   59058   94851  5603739    59.1 | 13.992 % |
c |    147848 |  177174   502139 |   64963   19109   827494    43.3 | 13.993 % |
c |    147999 |  177174   502139 |   71460   19260   834771    43.3 | 13.993 % |
c |    148225 |  177174   502139 |   78606   19486   848989    43.6 | 13.993 % |
c |    148562 |  177174   502139 |   86466   19823   858209    43.3 | 13.993 % |
c |    149068 |  177170   502130 |   95113   20327   869523    42.8 | 13.995 % |
c |    149827 |  177170   502130 |  104624   21086   899825    42.7 | 13.995 % |
c |    150967 |  177170   502130 |  115087   22226   978243    44.0 | 13.995 % |
c |    152675 |  177170   502130 |  126596   23934  1077496    45.0 | 13.995 % |
c |    155237 |  177170   502130 |  139255   26496  1291780    48.8 | 13.995 % |
c |    159082 |  177170   502130 |  153181   30341  1425428    47.0 | 13.995 % |
c |    164850 |  177170   502130 |  168499   36109  1931271    53.5 | 13.995 % |
c |    173503 |  177170   502130 |  185349   44762  2818801    63.0 | 13.995 % |
c |    186477 |  177170   502130 |  203884   57736  4461250    77.3 | 13.995 % |
c |    205938 |  177170   502130 |  224272   77197  6193139    80.2 | 13.995 % |
c |    235130 |  177170   502130 |  246699  106389  7746072    72.8 | 13.995 % |
c ==============================================================================
c [1mFound solution: 3349[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    239889 |  177376   502633 |   59125  111148  8274339    74.4 | 13.995 % |
c |    239990 |  177376   502633 |   65037   21629  1055139    48.8 | 14.110 % |
c |    240140 |  177376   502633 |   71541   21779  1065392    48.9 | 14.110 % |
c |    240366 |  177376   502633 |   78695   22005  1075377    48.9 | 14.110 % |
c |    240703 |  177376   502633 |   86564   22342  1093745    49.0 | 14.110 % |
c |    241209 |  177376   502633 |   95221   22848  1122300    49.1 | 14.110 % |
c |    241968 |  177376   502633 |  104743   23607  1181256    50.0 | 14.110 % |
c |    243107 |  177376   502633 |  115217   24746  1274774    51.5 | 14.110 % |
c ==============================================================================
c [1mFound solution: 3348[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    244188 |  177384   502651 |   59128   25827  1368244    53.0 | 14.110 % |
c |    244289 |  177384   502651 |   65040   25928  1370512    52.9 | 14.111 % |
c |    244439 |  177384   502651 |   71544   26078  1373093    52.7 | 14.111 % |
c |    244666 |  177384   502651 |   78699   26305  1397230    53.1 | 14.111 % |
c |    245003 |  177384   502651 |   86569   26642  1406176    52.8 | 14.111 % |
c |    245509 |  177384   502651 |   95226   27148  1466628    54.0 | 14.111 % |
c |    246268 |  177384   502651 |  104748   27907  1491851    53.5 | 14.111 % |
c |    247407 |  177384   502651 |  115223   29046  1546327    53.2 | 14.111 % |
c |    249115 |  177384   502651 |  126746   30754  1668825    54.3 | 14.111 % |
c |    251677 |  177384   502651 |  139420   33316  1805037    54.2 | 14.111 % |
c |    255522 |  177384   502651 |  153362   37161  2030785    54.6 | 14.111 % |
c ==============================================================================
c [1mFound solution: 3347[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    257747 |  177392   502669 |   59130   39386  2180548    55.4 | 14.111 % |
c |    257848 |  177392   502669 |   65043   39487  2184038    55.3 | 14.112 % |
c |    257999 |  177392   502669 |   71547   39638  2193084    55.3 | 14.112 % |
c |    258225 |  177392   502669 |   78702   39864  2197781    55.1 | 14.112 % |
c |    258562 |  177392   502669 |   86572   40201  2240162    55.7 | 14.112 % |
c |    259071 |  177392   502669 |   95229   40710  2266475    55.7 | 14.112 % |
c ==============================================================================
c [1mFound solution: 2746[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    259306 |  177438   502778 |   59146   40945  2273776    55.5 | 14.112 % |
c |    259407 |  177438   502778 |   65060   41046  2276391    55.5 | 14.107 % |
c |    259557 |  177438   502778 |   71566   41196  2286602    55.5 | 14.107 % |
c |    259782 |  177438   502778 |   78723   41421  2295246    55.4 | 14.107 % |
c |    260120 |  177438   502778 |   86595   41759  2332513    55.9 | 14.107 % |
c |    260627 |  177438   502778 |   95255   42266  2360673    55.9 | 14.107 % |
c |    261386 |  177438   502778 |  104780   43025  2411467    56.0 | 14.107 % |
c |    262525 |  177438   502778 |  115258   44164  2458048    55.7 | 14.107 % |
c ==============================================================================
c [1mFound solution: 2745[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    262695 |  177443   502789 |   59147   44334  2463525    55.6 | 14.107 % |
c |    262796 |  177443   502789 |   65061   44435  2464640    55.5 | 14.108 % |
c |    262946 |  177443   502789 |   71567   44585  2468120    55.4 | 14.108 % |
c |    263172 |  177443   502789 |   78724   44811  2475855    55.3 | 14.108 % |
c |    263509 |  177443   502789 |   86597   45148  2507269    55.5 | 14.108 % |
c |    264017 |  177443   502789 |   95256   45656  2542287    55.7 | 14.108 % |
c |    264776 |  177443   502789 |  104782   46415  2578334    55.5 | 14.108 % |
c |    265915 |  177443   502789 |  115260   47554  2704822    56.9 | 14.108 % |
c |    267626 |  177443   502789 |  126786   49265  2758039    56.0 | 14.108 % |
c |    270188 |  177443   502789 |  139465   51827  2954062    57.0 | 14.108 % |
c |    274033 |  177443   502789 |  153412   55672  3158798    56.7 | 14.108 % |
c |    279800 |  177443   502789 |  168753   61439  3443505    56.0 | 14.108 % |
c |    288449 |  177443   502789 |  185628   70088  4138981    59.1 | 14.108 % |
c |    301423 |  177443   502789 |  204191   83062  6008088    72.3 | 14.108 % |
c |    320884 |  177435   502770 |  224610  102522  7756032    75.7 | 14.113 % |
c |    350077 |  177435   502770 |  247071  131715 10552176    80.1 | 14.113 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v1 -v127 -v505 v640 -v774 -v4 v256 v508 -v5 -v131 v257 -v383 v509 -v6 -v132 v258 v510 -v7 v133 v512 -v8 v134 v513 v388 v516 v11 -v137 -v517 -v12 v138 v518 -v14 v392 v520 -v15 -v141 v267 v521 -v16 v394 v522 -v17 v143 v523 -v18 v396 v524 v19 -v525 v659 v20 -v146 -v526 v21 -v273 -v527 v22 -v528 v662 v23 -v149 -v529 v24 -v150 -v530 -v25 -v151 v403 v531 -v26 v152 v532 v27 -v153 -v533 -v28 v406 -v534 -v29 v407 v535 v30 -v156 -v536 -v31 v157 v537 v32 -v158 v672 -v806 -v33 -v159 v285 -v539 -v34 v160 v540 -v287 v413 v36 -v162 -v542 -v37 v163 v543 -v38 v164 -v544 v39 -v545 v679 -v813 -v40 v166 v546 -v41 v419 -v547 -v42 v168 v548 -v43 v421 v549 v44 -v170 -v550 v551 -v45 v171 -v552 v686 v46 -v172 -v553 -v47 v173 -v425 v554 -v48 -v174 v426 v555 -v49 v175 v556 v428 -v51 v177 v558 -v52 v178 v559 v431 -v694 v828 -v54 -v180 v432 v561 -v55 v433 v562 -v56 v308 -v563 -v697 v831 -v57 v435 v564 -v58 v436 -v565 v566 -v59 v185 v567 v568 v60 -v569 -v703 v837 -v61 v187 v570 v62 -v314 -v440 -v571 v705 -v839 -v63 v189 v572 -v64 v316 -v573 v65 -v317 -v574 -v66 v318 v575 -v67 v193 -v576 v710 -v68 -v194 v320 -v577 -v711 v845 -v69 -v195 v447 -v578 -v70 v196 v579 v71 -v580 v714 -v72 v198 v581 -v73 v582 -v74 v200 v583 -v75 v201 v584 -v76 v202 v585 -v78 -v204 -v330 v456 v587 -v79 v457 -v588 v722 -v589 -v81 -v207 v333 -v459 -v590 -v82 v334 -v591 -v83 v335 -v461 -v592 v726 -v727 v861 v85 -v211 -v594 -v728 v862 -v86 -v212 v464 v595 v87 -v213 -v596 -v730 v864 -v88 v214 -v597 -v89 v467 -v598 v732 -v90 -v216 v468 -v599 -v600 -v92 -v218 -v602 -v93 v219 v603 v94 -v220 -v604 v738 -v872 -v96 v222 v606 v349 -v475 v741 -v98 v224 v608 -v99 v351 -v477 -v609 -v743 v877 v226 -v744 v878 v227 -v745 v879 -v102 -v228 v354 -v480 -v612 v103 -v229 -v355 -v481 -v613 v104 -v614 v748 -v105 -v231 v357 -v483 -v615 v106 -v616 -v107 v233 -v485 -v617 v108 -v234 -v618 -v109 v235 -v619 v753 -v110 -v236 v362 -v488 -v620 -v754 v888 -v756 v890 v113 -v365 -v623 v240 v115 -v241 -v493 -v625 v759 v116 -v242 -v626 -v627 v761 -v895 v117 -v495 -v628 -v118 v370 -v630 v764 -v898 -v119 -v631 -v765 v899 v120 -v246 -v632 -v766 v900 -v121 v373 -v633 -v122 v374 -v500 -v634 v123 -v635 v903 -v124 v376 -v502 -v636 -v770 v904 -v771 v905 v126 -v638 v772 -v2 -v128 -v506 -v3 -v507 -v641 -v130 -v642 -v776 -v643 -v777 -v384 -v644 -v778 v645 -v779 -v259 -v646 -v780 -v260 -v386 -v647 -v781 -v261 -v387 -v136 -v389 -v264 -v390 -v652 -v786 -v654 -v788 -v655 -v789 -v142 -v656 -v790 -v269 -v657 -v791 -v270 -v658 -v792 -v145 -v271 -v272 -v398 -v660 v794 -v147 -v399 -v661 v795 -v148 -v400 -v275 -v663 v797 -v276 -v402 -v664 v798 -v277 -v665 -v799 -v278 -v404 -v666 -v800 -v279 -v405 -v667 v801 -v154 -v280 -v668 v802 -v155 -v281 -v669 -v803 -v283 -v409 -v671 -v805 -v411 -v286 -v412 -v674 -v808 v675 -v809 -v289 -v415 -v677 -v811 -v290 -v416 v678 -v812 -v165 -v291 -v417 -v292 -v680 -v814 -v294 -v420 -v682 -v816 -v169 -v683 -v817 -v296 -v422 -v684 v818 -v685 -v819 -v297 -v423 -v820 -v299 -v688 -v822 -v300 -v689 -v823 -v301 -v427 -v690 -v824 -v50 -v176 -v302 -v557 -v691 v825 -v303 -v429 -v692 -v826 -v304 -v430 -v693 -v827 -v53 -v179 -v305 -v560 -v306 -v695 -v829 -v181 -v696 -v830 -v182 -v434 -v183 -v309 -v698 -v832 -v184 -v310 -v700 -v834 -v311 -v437 -v701 -v835 -v702 -v836 -v186 -v312 -v438 -v313 -v439 -v704 -v838 -v188 -v315 -v706 -v840 -v190 -v442 -v707 v841 -v191 -v443 -v192 -v444 -v709 -v843 -v319 -v445 -v844 -v446 -v321 -v846 -v322 -v448 -v713 -v847 -v197 -v323 -v449 -v324 -v450 -v715 -v849 -v325 -v716 -v850 -v326 -v452 -v717 -v851 -v327 -v453 -v718 -v852 -v328 -v454 -v719 -v853 -v721 -v855 -v205 -v331 -v856 -v206 -v724 v858 -v208 -v460 -v337 -v463 -v338 -v729 -v863 -v339 -v465 -v340 -v466 -v731 v865 -v215 -v341 -v866 -v342 -v733 v867 -v217 -v344 -v736 v870 -v345 -v471 -v737 -v871 -v346 -v472 -v347 -v739 v873 -v348 -v740 -v874 -v350 -v476 -v742 -v876 -v225 -v352 -v478 -v353 -v479 -v746 v880 -v747 v881 -v749 v883 -v484 -v750 v884 -v359 -v360 -v486 v752 -v886 -v361 -v487 -v887 v755 -v889 -v238 -v490 -v491 v757 -v891 -v114 -v366 -v492 -v624 -v367 -v893 -v368 -v494 v760 -v894 -v243 -v369#### 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.93 0.97 0.91 2/54 3434
Raw data (stat): 3434 (runsolver) R 3433 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423031741 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 5374 0 0 0 983 15 0 0 25 0 1 0 423031741 24453120 5204 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5970 5204 603 41 0 5929 0
vsize: 23880
[startup+20.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 5404 0 0 0 1983 16 0 0 25 0 1 0 423031741 24588288 5234 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6003 5234 603 41 0 5962 0
vsize: 24012
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 5721 0 0 0 2981 17 0 0 25 0 1 0 423031741 25833472 5551 4294967295 134512640 134672761 3221224560 3221223664 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6307 5551 603 41 0 6266 0
vsize: 25228
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 5919 0 0 0 3980 18 0 0 25 0 1 0 423031741 26722304 5749 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6524 5749 603 41 0 6483 0
vsize: 26096
[startup+50.0028 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 6081 0 0 0 4979 19 0 0 25 0 1 0 423031741 27262976 5911 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6656 5911 603 41 0 6615 0
vsize: 26624
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 6209 0 0 0 5978 20 0 0 25 0 1 0 423031741 27795456 6039 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6786 6039 603 41 0 6745 0
vsize: 27144
[startup+70.0044 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 6434 0 0 0 6977 21 0 0 25 0 1 0 423031741 28733440 6264 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7015 6264 603 41 0 6974 0
vsize: 28060
[startup+80.0052 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 6660 0 0 0 7976 22 0 0 25 0 1 0 423031741 29798400 6490 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7275 6490 603 41 0 7234 0
vsize: 29100
[startup+90.0055 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 6937 0 0 0 8975 23 0 0 25 0 1 0 423031741 30875648 6767 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7538 6767 603 41 0 7497 0
vsize: 30152
[startup+100.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 7194 0 0 0 9973 24 0 0 25 0 1 0 423031741 31948800 7024 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7800 7024 603 41 0 7759 0
vsize: 31200
[startup+110.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 7544 0 0 0 10972 25 0 0 25 0 1 0 423031741 33300480 7374 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8130 7374 603 41 0 8089 0
vsize: 32520
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 7898 0 0 0 11971 27 0 0 25 0 1 0 423031741 34787328 7728 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8493 7728 603 41 0 8452 0
vsize: 33972
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 8220 0 0 0 12969 28 0 0 25 0 1 0 423031741 35995648 8050 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8788 8050 603 41 0 8747 0
vsize: 35152
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 8450 0 0 0 13967 30 0 0 25 0 1 0 423031741 36937728 8280 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9018 8280 603 41 0 8977 0
vsize: 36072
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 8795 0 0 0 14966 31 0 0 25 0 1 0 423031741 38416384 8625 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9379 8625 603 41 0 9338 0
vsize: 37516
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9104 0 0 0 15966 32 0 0 25 0 1 0 423031741 39854080 8934 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9730 8934 603 41 0 9689 0
vsize: 38920
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9291 0 0 0 16966 32 0 0 25 0 1 0 423031741 40660992 9121 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9121 603 41 0 9886 0
vsize: 39708
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9310 0 0 0 17966 32 0 0 25 0 1 0 423031741 40660992 9140 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9140 603 41 0 9886 0
vsize: 39708
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 18966 32 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 19966 32 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 20966 33 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223664 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 21966 33 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 22966 33 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 23967 33 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 24967 33 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 25967 33 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 26967 33 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223744 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9314 0 0 0 27967 33 0 0 25 0 1 0 423031741 40660992 9144 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9144 603 41 0 9886 0
vsize: 39708
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9362 0 0 0 28967 33 0 0 25 0 1 0 423031741 40931328 9192 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9993 9192 603 41 0 9952 0
vsize: 39972
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9511 0 0 0 29967 33 0 0 25 0 1 0 423031741 41467904 9341 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10124 9341 603 41 0 10083 0
vsize: 40496
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9779 0 0 0 30966 34 0 0 25 0 1 0 423031741 42541056 9609 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10386 9609 603 41 0 10345 0
vsize: 41544
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 9992 0 0 0 31966 34 0 0 25 0 1 0 423031741 43479040 9822 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10615 9822 603 41 0 10574 0
vsize: 42460
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 10188 0 0 0 32965 35 0 0 25 0 1 0 423031741 44277760 10018 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10810 10018 603 41 0 10769 0
vsize: 43240
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 10519 0 0 0 33964 36 0 0 25 0 1 0 423031741 45613056 10349 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11136 10349 603 41 0 11095 0
vsize: 44544
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 10846 0 0 0 34963 38 0 0 25 0 1 0 423031741 46960640 10676 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11465 10676 603 41 0 11424 0
vsize: 45860
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 11127 0 0 0 35963 38 0 0 25 0 1 0 423031741 48041984 10957 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11729 10957 603 41 0 11688 0
vsize: 46916
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 11354 0 0 0 36963 39 0 0 25 0 1 0 423031741 48992256 11184 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11961 11184 603 41 0 11920 0
vsize: 47844
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 11589 0 0 0 37962 39 0 0 25 0 1 0 423031741 50085888 11419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12228 11419 603 41 0 12187 0
vsize: 48912
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 11911 0 0 0 38962 40 0 0 25 0 1 0 423031741 51294208 11741 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12523 11741 603 41 0 12482 0
vsize: 50092
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 39961 40 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 40962 40 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 41962 40 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223744 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 42962 40 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 43962 40 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 44962 40 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223744 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 45963 40 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 46963 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 47963 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 48963 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 49963 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 50964 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 51964 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 52964 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 53964 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223696 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 54964 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12153 0 0 0 55964 41 0 0 25 0 1 0 423031741 52330496 11983 4294967295 134512640 134672761 3221224560 3221223664 134559859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 11983 603 41 0 12735 0
vsize: 51104
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12341 0 0 0 56965 41 0 0 25 0 1 0 423031741 53137408 12171 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12171 603 41 0 12932 0
vsize: 51892
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12540 0 0 0 57964 42 0 0 25 0 1 0 423031741 53940224 12370 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13169 12370 603 41 0 13128 0
vsize: 52676
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12719 0 0 0 58964 42 0 0 25 0 1 0 423031741 54611968 12549 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13333 12549 603 41 0 13292 0
vsize: 53332
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 12887 0 0 0 59963 43 0 0 25 0 1 0 423031741 55279616 12717 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13496 12717 603 41 0 13455 0
vsize: 53984
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 13194 0 0 0 60961 44 0 0 25 0 1 0 423031741 56623104 13024 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13824 13024 603 41 0 13783 0
vsize: 55296
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 13521 0 0 0 61960 45 0 0 25 0 1 0 423031741 57950208 13351 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14148 13351 603 41 0 14107 0
vsize: 56592
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 13858 0 0 0 62960 46 0 0 25 0 1 0 423031741 59314176 13688 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14481 13688 603 41 0 14440 0
vsize: 57924
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 14090 0 0 0 63960 46 0 0 25 0 1 0 423031741 60264448 13920 4294967295 134512640 134672761 3221224560 3221223744 134559388 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14713 13920 603 41 0 14672 0
vsize: 58852
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 14242 0 0 0 64959 46 0 0 25 0 1 0 423031741 61009920 14072 4294967295 134512640 134672761 3221224560 3221223664 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14895 14072 603 41 0 14854 0
vsize: 59580
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 14445 0 0 0 65959 47 0 0 25 0 1 0 423031741 61726720 14275 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15070 14275 603 41 0 15029 0
vsize: 60280
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 14634 0 0 0 66958 48 0 0 25 0 1 0 423031741 62570496 14464 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15276 14464 603 41 0 15235 0
vsize: 61104
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 14892 0 0 0 67958 49 0 0 25 0 1 0 423031741 63647744 14722 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15539 14722 603 41 0 15498 0
vsize: 62156
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15045 0 0 0 68957 50 0 0 25 0 1 0 423031741 64315392 14875 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15702 14875 603 41 0 15661 0
vsize: 62808
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15219 0 0 0 69956 51 0 0 25 0 1 0 423031741 64983040 15049 4294967295 134512640 134672761 3221224560 3221223664 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15865 15049 603 41 0 15824 0
vsize: 63460
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15304 0 0 0 70956 51 0 0 25 0 1 0 423031741 65249280 15134 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15134 603 41 0 15889 0
vsize: 63720
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15304 0 0 0 71956 51 0 0 25 0 1 0 423031741 65249280 15134 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15134 603 41 0 15889 0
vsize: 63720
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 72956 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 73957 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 74957 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 75957 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 76957 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 77957 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 78957 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 79958 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 80958 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 81958 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 82958 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 83958 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 84958 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223716 134560075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 85959 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 86959 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 87959 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 88959 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 89959 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 90960 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 91960 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 92960 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 93960 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15306 0 0 0 94960 51 0 0 25 0 1 0 423031741 65249280 15136 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15930 15136 603 41 0 15889 0
vsize: 63720
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15352 0 0 0 95961 51 0 0 25 0 1 0 423031741 65540096 15182 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16001 15182 603 41 0 15960 0
vsize: 64004
[startup+970.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15549 0 0 0 96961 51 0 0 25 0 1 0 423031741 66342912 15379 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16197 15379 603 41 0 16156 0
vsize: 64788
[startup+980.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15689 0 0 0 97960 52 0 0 25 0 1 0 423031741 66875392 15519 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16327 15519 603 41 0 16286 0
vsize: 65308
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15820 0 0 0 98960 52 0 0 25 0 1 0 423031741 67407872 15650 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16457 15650 603 41 0 16416 0
vsize: 65828
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 15983 0 0 0 99959 53 0 0 25 0 1 0 423031741 68067328 15813 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16618 15813 603 41 0 16577 0
vsize: 66472
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 16143 0 0 0 100959 53 0 0 25 0 1 0 423031741 68747264 15973 4294967295 134512640 134672761 3221224560 3221223664 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16784 15973 603 41 0 16743 0
vsize: 67136
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 16285 0 0 0 101959 54 0 0 25 0 1 0 423031741 69279744 16115 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16914 16115 603 41 0 16873 0
vsize: 67656
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 16439 0 0 0 102959 54 0 0 25 0 1 0 423031741 69955584 16269 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16269 603 41 0 17038 0
vsize: 68316
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 16588 0 0 0 103959 54 0 0 25 0 1 0 423031741 70488064 16418 4294967295 134512640 134672761 3221224560 3221223696 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17209 16418 603 41 0 17168 0
vsize: 68836
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 16708 0 0 0 104959 54 0 0 25 0 1 0 423031741 71024640 16538 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17340 16538 603 41 0 17299 0
vsize: 69360
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 16845 0 0 0 105959 55 0 0 25 0 1 0 423031741 71553024 16675 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17469 16675 603 41 0 17428 0
vsize: 69876
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 16994 0 0 0 106958 55 0 0 25 0 1 0 423031741 72220672 16824 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17632 16824 603 41 0 17591 0
vsize: 70528
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 17165 0 0 0 107958 56 0 0 25 0 1 0 423031741 72900608 16995 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17798 16995 603 41 0 17757 0
vsize: 71192
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 17322 0 0 0 108958 56 0 0 25 0 1 0 423031741 73568256 17152 4294967295 134512640 134672761 3221224560 3221223664 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17961 17152 603 41 0 17920 0
vsize: 71844
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 17455 0 0 0 109958 56 0 0 25 0 1 0 423031741 74104832 17285 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18092 17285 603 41 0 18051 0
vsize: 72368
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 17585 0 0 0 110958 57 0 0 25 0 1 0 423031741 74633216 17415 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18221 17415 603 41 0 18180 0
vsize: 72884
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 17738 0 0 0 111957 57 0 0 25 0 1 0 423031741 75309056 17568 4294967295 134512640 134672761 3221224560 3221223664 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18386 17568 603 41 0 18345 0
vsize: 73544
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 17867 0 0 0 112957 58 0 0 25 0 1 0 423031741 75706368 17697 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18483 17697 603 41 0 18442 0
vsize: 73932
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 17995 0 0 0 113957 58 0 0 25 0 1 0 423031741 76759040 17825 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18740 17825 603 41 0 18699 0
vsize: 74960
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 18102 0 0 0 114955 59 0 0 25 0 1 0 423031741 77176832 17932 4294967295 134512640 134672761 3221224560 3221223664 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18842 17932 603 41 0 18801 0
vsize: 75368
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 18208 0 0 0 115955 59 0 0 25 0 1 0 423031741 77709312 18038 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18972 18038 603 41 0 18931 0
vsize: 75888
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 18326 0 0 0 116955 60 0 0 25 0 1 0 423031741 78106624 18156 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19069 18156 603 41 0 19028 0
vsize: 76276
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 18469 0 0 0 117954 60 0 0 25 0 1 0 423031741 78782464 18299 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19234 18299 603 41 0 19193 0
vsize: 76936
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 18615 0 0 0 118954 61 0 0 25 0 1 0 423031741 79331328 18445 4294967295 134512640 134672761 3221224560 3221223664 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19368 18445 603 41 0 19327 0
vsize: 77472
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3434
Raw data (stat): 3434 (minisat+) R 3433 30854 30853 0 -1 0 18724 0 0 0 119954 61 0 0 25 0 1 0 423031741 79859712 18554 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19497 18554 603 41 0 19456 0
vsize: 77988
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3434
Raw data (stat): 3434 (minisat+) Z 3433 30854 30853 0 -1 12 18727 0 0 0 119954 65 0 0 25 0 1 0 423031741 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.2
CPU user time (s): 1199.55
CPU system time (s): 0.6539
CPU usage (%): 100.011
Max. virtual memory (Kb): 77988
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####