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 6455

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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:      1034724 kB
MemFree:        700492 kB
Buffers:         35432 kB
Cached:         187280 kB
SwapCached:       1212 kB
Active:         147788 kB
Inactive:       155232 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        700236 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25392 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:22:50 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 4870 7 1200.26 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]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 659]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 658]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 657]---> Adder-cost: 238   maxlim: 91   bits: 7/7
c ---[ 656]---> Adder-cost: 260   maxlim: 85   bits: 8/7
c ---[ 655]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 654]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 653]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 652]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 651]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 650]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 649]---> Adder-cost: 28   maxlim: 33   bits: 7/6
c ---[ 648]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 647]---> Adder-cost: 28   maxlim: 34   bits: 7/6
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 |   16799    56773 |    5599       0        0     nan |  0.000 % |
c |       100 |   16799    56773 |    6158     100     1484    14.8 |  8.161 % |
c |       250 |   16793    56756 |    6774     249     2301     9.2 |  8.187 % |
c |       475 |   16781    56722 |    7452     472     3275     6.9 |  8.238 % |
c |       812 |   16781    56722 |    8197     809     4944     6.1 |  8.238 % |
c |      1318 |   16781    56722 |    9017    1315     7249     5.5 |  8.238 % |
c |      2077 |   16781    56722 |    9918    2074    13047     6.3 |  8.238 % |
c |      3216 |   16781    56722 |   10910    3213    33553    10.4 |  8.238 % |
c |      4925 |   16781    56722 |   12001    4922    51059    10.4 |  8.238 % |
c |      7487 |   16781    56722 |   13202    7484   148622    19.9 |  8.238 % |
c |     11336 |   16781    56722 |   14522   11333   419566    37.0 |  8.238 % |
c |     17102 |   16781    56722 |   15974   17099   835093    48.8 |  8.238 % |
c |     25756 |   16781    56722 |   17572   17204  1203943    70.0 |  8.238 % |
c |     38730 |   16781    56722 |   19329   11912  1062792    89.2 |  8.238 % |
c ==============================================================================
c [1mFound solution: 9206[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 |     45173 |   95016   239783 |   31672   18355  1406308    76.6 |  8.238 % |
c |     45273 |   95016   239783 |   34839   18455  1407400    76.3 |  1.075 % |
c |     45423 |   94489   238584 |   38323   18597  1408152    75.7 |  1.560 % |
c |     45649 |   89987   228242 |   42155   18758  1409204    75.1 |  6.081 % |
c |     45987 |   89334   226739 |   46370   19086  1418015    74.3 |  6.748 % |
c |     46494 |   88926   225792 |   51008   19586  1434344    73.2 |  7.189 % |
c |     47254 |   88267   224291 |   56108   20337  1442858    70.9 |  7.836 % |
c |     48393 |   78312   201258 |   61719   21233  1449112    68.2 | 18.384 % |
c |     50101 |   72920   188854 |   67891   22835  1535519    67.2 | 24.017 % |
c |     52663 |   72920   188854 |   74680   25397  1674704    65.9 | 24.017 % |
c |     56508 |   72762   188490 |   82149   29239  2012959    68.8 | 24.186 % |
c |     62275 |   72584   188079 |   90363   35003  2328687    66.5 | 24.378 % |
c |     70925 |   69680   181358 |   99400   43577  2799549    64.2 | 27.474 % |
c |     83899 |   68207   177949 |  109340   56529  3680319    65.1 | 29.010 % |
c |    103361 |   67456   176211 |  120274   75976  5090073    67.0 | 29.829 % |
c |    132555 |   66256   173429 |  132301  105134  7606681    72.4 | 31.132 % |
c |    176345 |   63423   166883 |  145531   16811  1883353   112.0 | 34.164 % |
c ==============================================================================
c [1mFound solution: 9117[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 |    196000 |   61863   163400 |   20621   36367  2155590    59.3 | 34.164 % |
c |    196101 |   61863   163400 |   22683   14706   175859    12.0 | 36.931 % |
c |    196251 |   61863   163400 |   24951   14856   176674    11.9 | 36.931 % |
c |    196476 |   61863   163400 |   27446   15081   178721    11.9 | 36.931 % |
c |    196813 |   61863   163400 |   30191   15418   180167    11.7 | 36.931 % |
c |    197319 |   61863   163400 |   33210   15924   182848    11.5 | 36.931 % |
c |    198078 |   61859   163391 |   36531   16682   205771    12.3 | 36.934 % |
c |    199218 |   61670   162948 |   40184   17817   218555    12.3 | 37.144 % |
c |    200926 |   61660   162925 |   44202   19520   242509    12.4 | 37.153 % |
c |    203488 |   61539   162648 |   48623   22072   275950    12.5 | 37.280 % |
c ==============================================================================
c [1mFound solution: 9106[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 |    206588 |   61466   162486 |   20488   25153   316594    12.6 | 37.280 % |
c |    206688 |   61466   162486 |   22536   25253   317166    12.6 | 37.369 % |
c |    206838 |   61466   162486 |   24790   25403   317728    12.5 | 37.369 % |
c |    207064 |   61466   162486 |   27269   25629   319551    12.5 | 37.369 % |
c |    207401 |   61466   162486 |   29996   25966   321813    12.4 | 37.369 % |
c |    207908 |   61466   162486 |   32996   26473   326204    12.3 | 37.369 % |
c |    208667 |   61466   162486 |   36295   27232   334200    12.3 | 37.369 % |
c |    209806 |   61466   162486 |   39925   28371   349468    12.3 | 37.369 % |
c |    211515 |   61466   162486 |   43917   30080   366967    12.2 | 37.369 % |
c |    214077 |   61466   162486 |   48309   32642   428925    13.1 | 37.369 % |
c |    217921 |   61466   162486 |   53140   36486   488219    13.4 | 37.369 % |
c ==============================================================================
c [1mFound solution: 8898[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 |    219619 |   62095   164041 |   20698   38182   518576    13.6 | 37.369 % |
c |    219719 |   62095   164041 |   22767   19191   201575    10.5 | 37.454 % |
c |    219870 |   62095   164041 |   25044   19342   202760    10.5 | 37.454 % |
c |    220096 |   62089   164027 |   27549   19566   204295    10.4 | 37.461 % |
c |    220434 |   62089   164027 |   30303   19904   206026    10.4 | 37.461 % |
c |    220940 |   62089   164027 |   33334   20410   209839    10.3 | 37.461 % |
c |    221699 |   62089   164027 |   36667   21169   214227    10.1 | 37.461 % |
c |    222838 |   62089   164027 |   40334   22308   226011    10.1 | 37.461 % |
c ==============================================================================
c [1mFound solution: 6886[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 |    223897 |   62500   165032 |   20833   23367   238042    10.2 | 37.461 % |
c |    223997 |   62500   165032 |   22916   23467   238903    10.2 | 37.359 % |
c |    224149 |   62500   165032 |   25207   23619   240341    10.2 | 37.359 % |
c |    224374 |   62500   165032 |   27728   23844   242015    10.1 | 37.359 % |
c |    224711 |   62500   165032 |   30501   24181   245786    10.2 | 37.359 % |
c |    225218 |   62500   165032 |   33551   24688   250953    10.2 | 37.359 % |
c |    225977 |   62500   165032 |   36906   25447   260051    10.2 | 37.359 % |
c |    227117 |   62500   165032 |   40597   26587   276351    10.4 | 37.359 % |
c |    228826 |   62500   165032 |   44657   28296   311146    11.0 | 37.359 % |
c |    231392 |   62496   165023 |   49123   30860   363273    11.8 | 37.362 % |
c |    235236 |   62496   165023 |   54035   34704   463796    13.4 | 37.362 % |
c |    241003 |   62496   165023 |   59438   40471   593307    14.7 | 37.362 % |
c |    249653 |   62496   165023 |   65382   49121   852016    17.3 | 37.362 % |
c |    262629 |   62496   165023 |   71921   62097  1508425    24.3 | 37.362 % |
c ==============================================================================
c [1mFound solution: 6798[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 |    271538 |   62513   165066 |   20837   71006  1713456    24.1 | 37.362 % |
c |    271640 |   62513   165066 |   22920   24384   447473    18.4 | 37.359 % |
c |    271790 |   62513   165066 |   25212   24534   449572    18.3 | 37.359 % |
c |    272015 |   62513   165066 |   27734   24759   450737    18.2 | 37.359 % |
c |    272353 |   62513   165066 |   30507   25097   453553    18.1 | 37.359 % |
c |    272859 |   62503   165042 |   33558   25583   459751    18.0 | 37.369 % |
c |    273618 |   62503   165042 |   36914   26342   476030    18.1 | 37.369 % |
c |    274757 |   62503   165042 |   40605   27481   489172    17.8 | 37.369 % |
c |    276467 |   62503   165042 |   44665   29191   530586    18.2 | 37.369 % |
c |    279029 |   62497   165028 |   49132   31751   595240    18.7 | 37.375 % |
c |    282874 |   62497   165028 |   54045   35596   666711    18.7 | 37.375 % |
c |    288640 |   62491   165014 |   59450   41359   818579    19.8 | 37.382 % |
c |    297289 |   62491   165014 |   65395   50008  1090126    21.8 | 37.382 % |
c |    310263 |   62491   165014 |   71934   62982  1816789    28.8 | 37.382 % |
c |    329724 |   62491   165014 |   79128   82443  3596129    43.6 | 37.382 % |
c ==============================================================================
c [1mFound solution: 6793[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 |    332908 |   62502   165041 |   20834   85627  3784759    44.2 | 37.382 % |
c |    333008 |   62502   165041 |   22917   23246  1131012    48.7 | 37.380 % |
c |    333158 |   62502   165041 |   25209   23396  1131831    48.4 | 37.380 % |
c |    333383 |   62502   165041 |   27730   23621  1133097    48.0 | 37.380 % |
c |    333720 |   62502   165041 |   30503   23958  1135256    47.4 | 37.380 % |
c |    334226 |   62502   165041 |   33553   24464  1142461    46.7 | 37.380 % |
c |    334986 |   62502   165041 |   36908   25224  1152095    45.7 | 37.380 % |
c |    336125 |   62502   165041 |   40599   26363  1175068    44.6 | 37.380 % |
c |    337833 |   62502   165041 |   44659   28071  1214755    43.3 | 37.380 % |
c |    340395 |   62502   165041 |   49125   30633  1279294    41.8 | 37.380 % |
c |    344241 |   62502   165041 |   54038   34479  1361864    39.5 | 37.380 % |
c |    350008 |   62502   165041 |   59441   40246  1452710    36.1 | 37.380 % |
c |    358658 |   62498   165032 |   65386   48894  1676945    34.3 | 37.384 % |
c |    371632 |   62498   165032 |   71924   61868  2204235    35.6 | 37.384 % |
c |    391094 |   62498   165032 |   79117   81330  2793722    34.4 | 37.384 % |
c ==============================================================================
c [1mFound solution: 6680[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 |    399635 |   63079   166456 |   21026   89868  3000725    33.4 | 37.384 % |
c |    399735 |   63079   166456 |   23128   25865   351618    13.6 | 37.482 % |
c |    399886 |   63079   166456 |   25441   26016   353141    13.6 | 37.482 % |
c |    400111 |   63079   166456 |   27985   26241   354722    13.5 | 37.482 % |
c |    400448 |   63079   166456 |   30784   26578   360942    13.6 | 37.482 % |
c |    400954 |   63079   166456 |   33862   27084   369494    13.6 | 37.482 % |
c |    401713 |   63079   166456 |   37248   27843   380258    13.7 | 37.482 % |
c |    402852 |   63079   166456 |   40973   28982   398932    13.8 | 37.482 % |
c |    404561 |   63079   166456 |   45071   30691   439490    14.3 | 37.482 % |
c |    407123 |   63079   166456 |   49578   33253   479254    14.4 | 37.482 % |
c |    410967 |   63079   166456 |   54536   37097   599997    16.2 | 37.482 % |
c |    416733 |   63079   166456 |   59989   42863   758100    17.7 | 37.482 % |
c |    425382 |   63079   166456 |   65988   51512   968059    18.8 | 37.482 % |
c |    438356 |   63079   166456 |   72587   64486  1357613    21.1 | 37.482 % |
c |    457817 |   63079   166456 |   79846   83947  2458640    29.3 | 37.482 % |
c |    487011 |   63079   166456 |   87830   46058  2843566    61.7 | 37.482 % |
c |    530801 |   63079   166456 |   96613   89848  4965111    55.3 | 37.482 % |
c ==============================================================================
c [1mFound solution: 6612[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 |    562687 |   63116   166551 |   21038  121734  7667403    63.0 | 37.482 % |
c |    562787 |   63116   166551 |   23141   24916  1620787    65.1 | 37.475 % |
c |    562938 |   63116   166551 |   25455   25067  1622022    64.7 | 37.475 % |
c |    563163 |   63116   166551 |   28001   25292  1623301    64.2 | 37.475 % |
c |    563500 |   63116   166551 |   30801   25629  1625574    63.4 | 37.475 % |
c |    564006 |   63116   166551 |   33881   26135  1629285    62.3 | 37.475 % |
c |    564767 |   63116   166551 |   37270   26896  1644626    61.1 | 37.475 % |
c |    565907 |   63116   166551 |   40997   28036  1664414    59.4 | 37.475 % |
c |    567621 |   63116   166551 |   45096   29750  1688514    56.8 | 37.475 % |
c |    570183 |   63116   166551 |   49606   32312  1747639    54.1 | 37.475 % |
c |    574027 |   63109   166533 |   54567   36146  1818002    50.3 | 37.484 % |
c |    579793 |   63109   166533 |   60023   41912  1916667    45.7 | 37.484 % |
c |    588442 |   63109   166533 |   66026   50561  2105692    41.6 | 37.484 % |
c |    601416 |   63109   166533 |   72628   63535  2459703    38.7 | 37.484 % |
c |    620877 |   63102   166515 |   79891   82983  3656183    44.1 | 37.494 % |
c ==============================================================================
c [1mFound solution: 6587[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 |    621584 |   63110   166535 |   21036   83690  3668227    43.8 | 37.494 % |
c |    621684 |   63110   166535 |   23139   27670   812289    29.4 | 37.494 % |
c |    621835 |   63110   166535 |   25453   27821   817660    29.4 | 37.494 % |
c |    622062 |   63110   166535 |   27998   28048   820801    29.3 | 37.494 % |
c |    622399 |   63110   166535 |   30798   28385   824738    29.1 | 37.494 % |
c |    622907 |   63110   166535 |   33878   28893   833132    28.8 | 37.494 % |
c |    623666 |   63110   166535 |   37266   29652   842558    28.4 | 37.494 % |
c |    624805 |   63110   166535 |   40993   30791   869061    28.2 | 37.494 % |
c |    626513 |   63110   166535 |   45092   32499   897247    27.6 | 37.494 % |
c |    629076 |   63110   166535 |   49601   35062   929624    26.5 | 37.494 % |
c |    632920 |   63110   166535 |   54561   38906  1198972    30.8 | 37.494 % |
c |    638688 |   63110   166535 |   60018   44674  1333386    29.8 | 37.494 % |
c |    647338 |   63110   166535 |   66019   53324  2186543    41.0 | 37.494 % |
c |    660312 |   63110   166535 |   72621   66298  2598092    39.2 | 37.494 % |
c ==============================================================================
c [1mFound solution: 6489[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 |    668319 |   63541   167594 |   21180   74305  3058906    41.2 | 37.494 % |
c |    668419 |   63541   167594 |   23298   26820   660459    24.6 | 37.554 % |
c |    668569 |   63541   167594 |   25627   26970   661123    24.5 | 37.554 % |
c |    668794 |   63541   167594 |   28190   27195   662510    24.4 | 37.554 % |
c |    669132 |   63541   167594 |   31009   27533   665490    24.2 | 37.554 % |
c |    669638 |   63541   167594 |   34110   28039   672062    24.0 | 37.554 % |
c |    670397 |   63541   167594 |   37521   28798   679342    23.6 | 37.554 % |
c |    671536 |   63541   167594 |   41273   29937   693973    23.2 | 37.554 % |
c |    673244 |   63541   167594 |   45401   31645   732498    23.1 | 37.554 % |
c |    675806 |   63541   167594 |   49941   34207   865224    25.3 | 37.554 % |
c |    679651 |   63535   167580 |   54935   38051   936124    24.6 | 37.560 % |
c |    685417 |   63535   167580 |   60429   43817  1205062    27.5 | 37.560 % |
c |    694066 |   63535   167580 |   66471   52466  1444191    27.5 | 37.560 % |
c ==============================================================================
c [1mFound solution: 6415[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 |    696674 |   63561   167644 |   21187   55074  1519921    27.6 | 37.560 % |
c |    696775 |   63561   167644 |   23305   26341   393838    15.0 | 37.554 % |
c |    696925 |   63561   167644 |   25636   26491   395103    14.9 | 37.554 % |
c |    697150 |   63561   167644 |   28199   26716   398157    14.9 | 37.554 % |
c |    697488 |   63561   167644 |   31019   27054   403192    14.9 | 37.554 % |
c |    697994 |   63561   167644 |   34121   27560   410788    14.9 | 37.554 % |
c |    698755 |   63561   167644 |   37534   28321   426771    15.1 | 37.554 % |
c |    699894 |   63561   167644 |   41287   29460   439907    14.9 | 37.554 % |
c |    701602 |   63561   167644 |   45416   31168   473717    15.2 | 37.554 % |
c |    704164 |   63561   167644 |   49957   33730   544223    16.1 | 37.554 % |
c |    708010 |   63561   167644 |   54953   37576   610886    16.3 | 37.554 % |
c |    713776 |   63561   167644 |   60448   43342   761972    17.6 | 37.554 % |
c |    722425 |   63561   167644 |   66493   51991   984863    18.9 | 37.554 % |
c |    735401 |   63561   167644 |   73143   64967  1448829    22.3 | 37.554 % |
c ==============================================================================
c [1mFound solution: 6397[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 |    745013 |   63577   167682 |   21192   74579  1796583    24.1 | 37.554 % |
c |    745113 |   63577   167682 |   23311   27282   492915    18.1 | 37.550 % |
c |    745263 |   63577   167682 |   25642   27432   495115    18.0 | 37.550 % |
c |    745489 |   63577   167682 |   28206   27658   498043    18.0 | 37.550 % |
c |    745826 |   63577   167682 |   31027   27995   503395    18.0 | 37.550 % |
c |    746332 |   63577   167682 |   34129   28501   511515    17.9 | 37.550 % |
c |    747092 |   63577   167682 |   37542   29261   523299    17.9 | 37.550 % |
c |    748233 |   63577   167682 |   41297   30402   548705    18.0 | 37.550 % |
c |    749943 |   63577   167682 |   45426   32112   572648    17.8 | 37.550 % |
c |    752506 |   63577   167682 |   49969   34675   634802    18.3 | 37.550 % |
c ==============================================================================
c [1mFound solution: 6321[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 |    755078 |   63634   167827 |   21211   37247   691139    18.6 | 37.550 % |
c |    755179 |   63634   167827 |   23332   18725   149603     8.0 | 37.532 % |
c |    755329 |   63634   167827 |   25665   18875   151265     8.0 | 37.533 % |
c |    755555 |   63634   167827 |   28231   19101   156342     8.2 | 37.533 % |
c |    755892 |   63634   167827 |   31055   19438   160522     8.3 | 37.533 % |
c |    756398 |   63634   167827 |   34160   19944   170270     8.5 | 37.532 % |
c |    757157 |   63634   167827 |   37576   20703   181025     8.7 | 37.532 % |
c |    758296 |   63634   167827 |   41334   21842   202976     9.3 | 37.532 % |
c |    760004 |   63634   167827 |   45467   23550   253905    10.8 | 37.533 % |
c |    762567 |   63634   167827 |   50014   26113   297315    11.4 | 37.533 % |
c |    766411 |   63634   167827 |   55015   29957   363358    12.1 | 37.532 % |
c |    772179 |   63634   167827 |   60517   35725   883402    24.7 | 37.533 % |
c |    780830 |   63634   167827 |   66569   44376  1158879    26.1 | 37.533 % |
c ==============================================================================
c [1mFound solution: 6290[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 |    788426 |   63650   167869 |   21216   51972  1450903    27.9 | 37.533 % |
c |    788526 |   63650   167869 |   23337   26086   441991    16.9 | 37.531 % |
c |    788676 |   63650   167869 |   25671   26236   443133    16.9 | 37.531 % |
c |    788901 |   63650   167869 |   28238   26461   444441    16.8 | 37.531 % |
c |    789238 |   63650   167869 |   31062   26798   453088    16.9 | 37.531 % |
c |    789744 |   63650   167869 |   34168   27304   465243    17.0 | 37.531 % |
c |    790503 |   63650   167869 |   37585   28063   481822    17.2 | 37.531 % |
c |    791642 |   63650   167869 |   41343   29202   530191    18.2 | 37.531 % |
c |    793351 |   63650   167869 |   45478   30911   572909    18.5 | 37.531 % |
c |    795913 |   63650   167869 |   50026   33473   616072    18.4 | 37.531 % |
c |    799760 |   63650   167869 |   55028   37320   730020    19.6 | 37.531 % |
c |    805526 |   63650   167869 |   60531   43086  1020544    23.7 | 37.531 % |
c ==============================================================================
c [1mFound solution: 6199[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 |    811522 |   63720   168063 |   21240   49082  1165526    23.7 | 37.531 % |
c |    811622 |   63720   168063 |   23364   24641   351010    14.2 | 37.523 % |
c |    811773 |   63720   168063 |   25700   24792   352470    14.2 | 37.523 % |
c |    811998 |   63720   168063 |   28270   25017   358192    14.3 | 37.523 % |
c |    812336 |   63720   168063 |   31097   25355   366661    14.5 | 37.523 % |
c |    812844 |   63720   168063 |   34207   25863   372926    14.4 | 37.523 % |
c |    813604 |   63711   168044 |   37627   26622   382301    14.4 | 37.526 % |
c |    814743 |   63711   168044 |   41390   27761   400447    14.4 | 37.527 % |
c |    816452 |   63711   168044 |   45529   29470   426082    14.5 | 37.526 % |
c |    819016 |   63711   168044 |   50082   32034   473550    14.8 | 37.526 % |
c |    822860 |   63711   168044 |   55091   35878   542118    15.1 | 37.526 % |
c |    828626 |   63700   168015 |   60600   41277   696887    16.9 | 37.539 % |
c ==============================================================================
c [1mFound solution: 6190[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 |    830054 |   63706   168029 |   21235   42705   740765    17.3 | 37.539 % |
c |    830154 |   63706   168029 |   23358   21453   229591    10.7 | 37.539 % |
c |    830305 |   63706   168029 |   25694   21604   231849    10.7 | 37.539 % |
c |    830530 |   63700   168015 |   28263   21827   234407    10.7 | 37.545 % |
c |    830867 |   63619   167832 |   31090   22072   237985    10.8 | 37.619 % |
c |    831373 |   63619   167832 |   34199   22578   250403    11.1 | 37.619 % |
c |    832134 |   63619   167832 |   37619   23339   270473    11.6 | 37.619 % |
c |    833273 |   63619   167832 |   41381   24478   304508    12.4 | 37.619 % |
c |    834982 |   63619   167832 |   45519   26187   332679    12.7 | 37.619 % |
c |    837545 |   63619   167832 |   50071   28750   409979    14.3 | 37.619 % |
c |    841389 |   63619   167832 |   55078   32594   581170    17.8 | 37.619 % |
c |    847155 |   63619   167832 |   60585   38360   759404    19.8 | 37.619 % |
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 -v#### 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.86 0.99 0.92 2/53 15796
Raw data (stat): 15796 (runsolver) R 15795 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481914042 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.89 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 1913 0 0 0 992 5 0 0 25 0 1 0 481914042 9428992 1891 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1891 603 41 0 2261 0
vsize: 9208
[startup+20.0023 s]
Raw data (loadavg): 0.90 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 2481 0 0 0 1989 8 0 0 25 0 1 0 481914042 11718656 2459 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2459 603 41 0 2820 0
vsize: 11444
[startup+30.0033 s]
Raw data (loadavg): 0.92 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 4551 0 0 0 2984 13 0 0 25 0 1 0 481914042 20889600 4480 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5100 4480 603 41 0 5059 0
vsize: 20400
[startup+40.004 s]
Raw data (loadavg): 0.93 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 4599 0 0 0 3984 13 0 0 25 0 1 0 481914042 21024768 4528 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5133 4528 603 41 0 5092 0
vsize: 20532
[startup+50.0045 s]
Raw data (loadavg): 0.94 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 4605 0 0 0 4984 13 0 0 25 0 1 0 481914042 21024768 4534 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5133 4534 603 41 0 5092 0
vsize: 20532
[startup+60.0046 s]
Raw data (loadavg): 0.95 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 5128 0 0 0 5982 15 0 0 25 0 1 0 481914042 23187456 5057 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5661 5057 603 41 0 5620 0
vsize: 22644
[startup+70.0053 s]
Raw data (loadavg): 0.96 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 5799 0 0 0 6980 17 0 0 25 0 1 0 481914042 26001408 5728 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6348 5728 603 41 0 6307 0
vsize: 25392
[startup+80.0058 s]
Raw data (loadavg): 0.96 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 6302 0 0 0 7978 19 0 0 25 0 1 0 481914042 28024832 6231 4294967295 134512640 134672761 3221224576 3221223760 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6842 6231 603 41 0 6801 0
vsize: 27368
[startup+90.0058 s]
Raw data (loadavg): 0.97 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 6880 0 0 0 8977 21 0 0 25 0 1 0 481914042 30314496 6809 4294967295 134512640 134672761 3221224576 3221223792 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7401 6809 603 41 0 7360 0
vsize: 29604
[startup+100.007 s]
Raw data (loadavg): 0.97 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 7415 0 0 0 9975 23 0 0 25 0 1 0 481914042 32477184 7344 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7929 7344 603 41 0 7888 0
vsize: 31716
[startup+110.007 s]
Raw data (loadavg): 0.98 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 7938 0 0 0 10973 25 0 0 25 0 1 0 481914042 34897920 7867 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8520 7867 603 41 0 8479 0
vsize: 34080
[startup+120.008 s]
Raw data (loadavg): 0.98 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 8545 0 0 0 11971 28 0 0 25 0 1 0 481914042 37322752 8474 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9112 8474 603 41 0 9071 0
vsize: 36448
[startup+130.009 s]
Raw data (loadavg): 0.98 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 9119 0 0 0 12968 31 0 0 25 0 1 0 481914042 39743488 9048 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9703 9048 603 41 0 9662 0
vsize: 38812
[startup+140.009 s]
Raw data (loadavg): 0.98 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 9617 0 0 0 13966 32 0 0 25 0 1 0 481914042 41762816 9546 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10196 9546 603 41 0 10155 0
vsize: 40784
[startup+150.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 10040 0 0 0 14965 34 0 0 25 0 1 0 481914042 43364352 9969 4294967295 134512640 134672761 3221224576 3221223748 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10587 9969 603 41 0 10546 0
vsize: 42348
[startup+160.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 10392 0 0 0 15963 36 0 0 25 0 1 0 481914042 44843008 10321 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10948 10321 603 41 0 10907 0
vsize: 43792
[startup+170.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 10853 0 0 0 16962 38 0 0 25 0 1 0 481914042 46714880 10782 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11405 10782 603 41 0 11364 0
vsize: 45620
[startup+180.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 11318 0 0 0 17961 39 0 0 25 0 1 0 481914042 48578560 11247 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11860 11247 603 41 0 11819 0
vsize: 47440
[startup+190.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 11811 0 0 0 18959 40 0 0 25 0 1 0 481914042 50593792 11740 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12352 11740 603 41 0 12311 0
vsize: 49408
[startup+200.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15796
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 11846 0 0 0 19959 41 0 0 25 0 1 0 481914042 50728960 11775 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12385 11775 603 41 0 12344 0
vsize: 49540
[startup+210.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 12220 0 0 0 20959 41 0 0 25 0 1 0 481914042 52211712 12149 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12747 12149 603 41 0 12706 0
vsize: 50988
[startup+220.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 12666 0 0 0 21958 43 0 0 25 0 1 0 481914042 54099968 12595 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13208 12595 603 41 0 13167 0
vsize: 52832
[startup+230.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 12932 0 0 0 22957 43 0 0 25 0 1 0 481914042 55193600 12861 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13475 12861 603 41 0 13434 0
vsize: 53900
[startup+240.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 13334 0 0 0 23956 44 0 0 25 0 1 0 481914042 56807424 13263 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13869 13263 603 41 0 13828 0
vsize: 55476
[startup+250.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 13682 0 0 0 24955 46 0 0 25 0 1 0 481914042 58150912 13611 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14197 13611 603 41 0 14156 0
vsize: 56788
[startup+260.018 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 14095 0 0 0 25954 47 0 0 25 0 1 0 481914042 60411904 14024 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14749 14025 603 41 0 14708 0
vsize: 58996
[startup+270.019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 14557 0 0 0 26951 50 0 0 25 0 1 0 481914042 62287872 14486 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15207 14486 603 41 0 15166 0
vsize: 60828
[startup+280.019 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 15051 0 0 0 27949 52 0 0 25 0 1 0 481914042 64315392 14980 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15702 14980 603 41 0 15661 0
vsize: 62808
[startup+290.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 15532 0 0 0 28948 54 0 0 25 0 1 0 481914042 66334720 15461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16195 15461 603 41 0 16154 0
vsize: 64780
[startup+300.021 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 15949 0 0 0 29946 56 0 0 25 0 1 0 481914042 67944448 15878 4294967295 134512640 134672761 3221224576 3221223680 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15878 603 41 0 16547 0
vsize: 66352
[startup+310.022 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16379 0 0 0 30945 58 0 0 25 0 1 0 481914042 69685248 16308 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17013 16308 603 41 0 16972 0
vsize: 68052
[startup+320.022 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16433 0 0 0 31944 58 0 0 25 0 1 0 481914042 69955584 16362 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16362 603 41 0 17038 0
vsize: 68316
[startup+330.023 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16433 0 0 0 32944 58 0 0 25 0 1 0 481914042 69955584 16362 4294967295 134512640 134672761 3221224576 3221223776 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16362 603 41 0 17038 0
vsize: 68316
[startup+340.024 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16433 0 0 0 33944 58 0 0 25 0 1 0 481914042 69955584 16362 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16362 603 41 0 17038 0
vsize: 68316
[startup+350.024 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16454 0 0 0 34944 58 0 0 25 0 1 0 481914042 69955584 16383 4294967295 134512640 134672761 3221224576 3221223776 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16383 603 41 0 17038 0
vsize: 68316
[startup+360.026 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16455 0 0 0 35945 58 0 0 25 0 1 0 481914042 69955584 16384 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16384 603 41 0 17038 0
vsize: 68316
[startup+370.027 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16458 0 0 0 36945 58 0 0 25 0 1 0 481914042 69955584 16387 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16387 603 41 0 17038 0
vsize: 68316
[startup+380.028 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 37945 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+390.029 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 38945 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+400.029 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 39945 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+410.03 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 40945 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+420.031 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 41946 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+430.032 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 42946 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+440.033 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 43946 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223712 134565078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+450.033 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 44946 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+460.034 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 45946 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+470.035 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 46946 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+480.036 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 47946 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+490.036 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 48947 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+500.037 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 49947 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+510.038 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 50946 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+520.039 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 51947 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+530.039 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 52947 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+540.039 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 53947 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+550.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 54947 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+560.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16459 0 0 0 55947 58 0 0 25 0 1 0 481914042 69955584 16388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16388 603 41 0 17038 0
vsize: 68316
[startup+570.042 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 56948 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221222560 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+580.043 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 57947 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+590.043 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 58947 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+600.044 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 59948 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+610.044 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 60948 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223680 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+620.045 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 61948 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+630.046 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 62948 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+640.047 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 63948 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+650.047 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 64949 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+660.047 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 65949 58 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+670.049 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 66949 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+680.05 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 67949 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+690.05 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 68949 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+700.055 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 69949 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+710.055 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 70950 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+720.056 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 71950 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+730.057 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 72950 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+740.057 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 73950 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+750.058 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 74951 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+760.059 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 75951 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+770.059 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 76951 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+780.06 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 77951 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+790.062 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 78952 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+800.063 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 79952 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+810.063 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 80952 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+820.064 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 81952 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+830.064 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 82951 59 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223532 1075349836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+840.081 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 83953 60 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+850.082 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 84952 60 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+860.082 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 85952 60 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+870.084 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 86952 61 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223724 1074732964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+880.107 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 87953 61 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+890.108 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 88954 62 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+900.109 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 89953 62 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+910.11 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 90953 62 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+920.111 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 91953 63 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+930.112 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 92953 63 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+940.113 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 93953 64 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223680 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+950.113 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 94952 64 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+960.114 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 95952 65 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+970.116 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 96952 65 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+980.117 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16462 0 0 0 97952 65 0 0 25 0 1 0 481914042 69955584 16391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16391 603 41 0 17038 0
vsize: 68316
[startup+990.118 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16465 0 0 0 98952 66 0 0 25 0 1 0 481914042 69955584 16394 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16394 603 41 0 17038 0
vsize: 68316
[startup+1000.12 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16465 0 0 0 99952 66 0 0 25 0 1 0 481914042 69955584 16394 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16394 603 41 0 17038 0
vsize: 68316
[startup+1010.12 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16465 0 0 0 100952 66 0 0 25 0 1 0 481914042 69955584 16394 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16394 603 41 0 17038 0
vsize: 68316
[startup+1020.12 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 101953 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223760 134559658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1030.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 102953 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1040.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 103953 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1050.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 104953 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1060.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 105954 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1070.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 106954 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1080.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 107953 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1090.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 108953 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1100.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 109954 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223648 134553557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1110.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 110954 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223760 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1120.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16466 0 0 0 111954 66 0 0 25 0 1 0 481914042 69955584 16395 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16395 603 41 0 17038 0
vsize: 68316
[startup+1130.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16467 0 0 0 112954 66 0 0 25 0 1 0 481914042 69955584 16396 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16396 603 41 0 17038 0
vsize: 68316
[startup+1140.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16467 0 0 0 113954 66 0 0 25 0 1 0 481914042 69955584 16396 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16396 603 41 0 17038 0
vsize: 68316
[startup+1150.13 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16467 0 0 0 114954 66 0 0 25 0 1 0 481914042 69955584 16396 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16396 603 41 0 17038 0
vsize: 68316
[startup+1160.14 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16467 0 0 0 115955 66 0 0 25 0 1 0 481914042 69955584 16396 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16396 603 41 0 17038 0
vsize: 68316
[startup+1170.14 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16467 0 0 0 116955 66 0 0 25 0 1 0 481914042 69955584 16396 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16396 603 41 0 17038 0
vsize: 68316
[startup+1180.14 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16467 0 0 0 117955 66 0 0 25 0 1 0 481914042 69955584 16396 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16396 603 41 0 17038 0
vsize: 68316
[startup+1190.14 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16467 0 0 0 118955 66 0 0 25 0 1 0 481914042 69955584 16396 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16396 603 41 0 17038 0
vsize: 68316
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.99 0.92 2/53 15798
Raw data (stat): 15796 (minisat+) R 15795 7987 7986 0 -1 0 16467 0 0 0 119955 66 0 0 25 0 1 0 481914042 69955584 16396 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16396 603 41 0 17038 0
vsize: 68316
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.99 0.92 1/53 15798
Raw data (stat): 15796 (minisat+) Z 15795 7987 7986 0 -1 12 16470 0 0 0 119955 70 0 0 25 0 1 0 481914042 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.18
CPU time (s): 1200.26
CPU user time (s): 1199.56
CPU system time (s): 0.700893
CPU usage (%): 100.007
Max. virtual memory (Kb): 68316
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####