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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-timtab1.opb
MD5SUMbbe4af13307edeeeae2f9b61a7fffb41
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 1541
Biggest coefficient in the objective function 450560000000000
Number of bits for the biggest coefficient in the objective function 49
Sum of the numbers in the objective function 43694073499991809
Number of bits of the sum of numbers in the objective function 56
Biggest number in a constraint 1200000000000000000000
Number of bits of the biggest number in a constraint 71
Biggest sum of numbers in a constraint 4359687500000000475136
Number of bits of the biggest sum of numbers72
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark20.9068
Number of variables3085
Total number of constraints555
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)64
Number of constraints which are nor clauses,nor cardinality constraints491
Minimum length of a constraint1
Maximum length of a constraint111

Trace number 6167

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-20 04:01:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3331 boxname=wulflinc22 idbench=987 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bbe4af13307edeeeae2f9b61a7fffb41  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-timtab1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-timtab1.opb
IDLAUNCH: 3331
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        892608 kB
Buffers:          8940 kB
Cached:         106312 kB
SwapCached:        552 kB
Active:          16840 kB
Inactive:       101000 kB
HighTotal:      131008 kB
HighFree:        23856 kB
LowTotal:       903652 kB
LowFree:        868752 kB
SwapTotal:     2097892 kB
SwapFree:      2096768 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5788 kB
Slab:            18580 kB
Committed_AS:    64264 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:21:59 (client local time) WITH STATUS 10 IN 1209.52 SECONDS
stats: 3331 7 1209.52 10

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 401] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 624 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###########################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.........................................
c ---[ 722]---> BDD-cost:    9
c ---[ 721]---> BDD-cost:   12
c ---[ 720]---> BDD-cost:   12
c ---[ 718]---> BDD-cost:    9
c ---[ 717]---> BDD-cost:   12
c ---[ 715]---> BDD-cost:    9
c ---[ 714]---> BDD-cost:   12
c ---[ 711]---> BDD-cost:    9
c ---[ 710]---> BDD-cost:   12
c ---[ 704]---> BDD-cost:   12
c ---[ 703]---> BDD-cost:   12
c ---[ 702]---> BDD-cost:   12
c ---[ 701]---> BDD-cost:    9
c ---[ 700]---> BDD-cost:   12
c ---[ 699]---> BDD-cost:   12
c ---[ 697]---> BDD-cost:   12
c ---[ 690]---> BDD-cost:   12
c ---[ 689]---> BDD-cost:   12
c ---[ 688]---> BDD-cost:   12
c ---[ 687]---> BDD-cost:   12
c ---[ 686]---> BDD-cost:   12
c ---[ 685]---> BDD-cost:   12
c ---[ 683]---> BDD-cost:    9
c ---[ 682]---> BDD-cost:   12
c ---[ 681]---> BDD-cost:   12
c ---[ 680]---> BDD-cost:   12
c ---[ 679]---> BDD-cost:   12
c ---[ 676]---> BDD-cost:    9
c ---[ 675]---> BDD-cost:   12
c ---[ 674]---> BDD-cost:   12
c ---[ 666]---> BDD-cost:    9
c ---[ 664]---> BDD-cost:    9
c ---[ 663]---> BDD-cost:   12
c ---[ 662]---> BDD-cost:   12
c ---[ 661]---> BDD-cost:   12
c ---[ 660]---> BDD-cost:   12
c ---[ 656]---> BDD-cost:    9
c ---[ 655]---> BDD-cost:    9
c ---[ 654]---> BDD-cost:   12
c ---[ 653]---> BDD-cost:   12
c ---[ 652]---> BDD-cost:    9
c ---[ 650]---> BDD-cost:   12
c ---[ 649]---> BDD-cost:   12
c ---[ 647]---> BDD-cost:   12
c ---[ 641]---> BDD-cost:   12
c ---[ 640]---> BDD-cost:   12
c ---[ 639]---> BDD-cost:   12
c ---[ 638]---> BDD-cost:   12
c ---[ 637]---> BDD-cost:   12
c ---[ 636]---> BDD-cost:   12
c ---[ 634]---> BDD-cost:    9
c ---[ 633]---> BDD-cost:   12
c ---[ 628]---> BDD-cost:   12
c ---[ 627]---> BDD-cost:   12
c ---[ 626]---> BDD-cost:   12
c ---[ 625]---> BDD-cost:   12
c ---[ 624]---> BDD-cost:   12
c ---[ 623]---> BDD-cost:   12
c ---[ 622]---> BDD-cost:   12
c ---[ 621]---> BDD-cost:   12
c ---[ 619]---> BDD-cost:   12
c ---[ 618]---> BDD-cost:   12
c ---[ 617]---> BDD-cost:   12
c ---[ 616]---> BDD-cost:    9
c ---[ 615]---> BDD-cost:    9
c ---[ 614]---> BDD-cost:   12
c ---[ 609]---> BDD-cost:   12
c ---[ 608]---> BDD-cost:    9
c ---[ 607]---> BDD-cost:   12
c ---[ 606]---> BDD-cost:   12
c ---[ 604]---> BDD-cost:   12
c ---[ 603]---> BDD-cost:   12
c ---[ 602]---> BDD-cost:   12
c ---[ 600]---> BDD-cost:    9
c ---[ 598]---> BDD-cost:   12
c ---[ 597]---> BDD-cost:   12
c ---[ 595]---> BDD-cost:   12
c ---[ 594]---> BDD-cost:    9
c ---[ 593]---> BDD-cost:    9
c ---[ 591]---> BDD-cost:    9
c ---[ 590]---> BDD-cost:   12
c ---[ 589]---> BDD-cost:    9
c ---[ 588]---> BDD-cost:   12
c ---[ 584]---> BDD-cost:   12
c ---[ 583]---> BDD-cost:   12
c ---[ 582]---> BDD-cost:    9
c ---[ 581]---> BDD-cost:    9
c ---[ 578]---> BDD-cost:    9
c ---[ 577]---> BDD-cost:    9
c ---[ 575]---> BDD-cost:   12
c ---[ 574]---> BDD-cost:   12
c ---[ 573]---> BDD-cost:   12
c ---[ 572]---> BDD-cost:   12
c ---[ 571]---> BDD-cost:   12
c ---[ 570]---> BDD-cost:   12
c ---[ 569]---> BDD-cost:    9
c ---[ 566]---> BDD-cost:    9
c ---[ 559]---> BDD-cost:   12
c ---[ 558]---> BDD-cost:    9
c ---[ 556]---> BDD-cost:    9
c ---[ 555]---> BDD-cost:   12
c ---[ 553]---> BDD-cost:    9
c ---[ 551]---> BDD-cost:    9
c ---[ 539]---> BDD-cost:    9
c ---[ 535]---> BDD-cost:    9
c ---[ 532]---> BDD-cost:    9
c ---[ 531]---> BDD-cost:    9
c ---[ 527]---> BDD-cost:    9
c ---[ 523]---> BDD-cost:   12
c ---[ 522]---> BDD-cost:   12
c ---[ 521]---> BDD-cost:   12
c ---[ 519]---> BDD-cost:   12
c ---[ 518]---> BDD-cost:   12
c ---[ 516]---> BDD-cost:    9
c ---[ 515]---> BDD-cost:   12
c ---[ 514]---> BDD-cost:   12
c ---[ 513]---> BDD-cost:   12
c ---[ 512]---> BDD-cost:   12
c ---[ 511]---> BDD-cost:    9
c ---[ 510]---> BDD-cost:    9
c ---[ 509]---> BDD-cost:    9
c ---[ 508]---> BDD-cost:   12
c ---[ 505]---> BDD-cost:   12
c ---[ 504]---> BDD-cost:   12
c ---[ 503]---> BDD-cost:   12
c ---[ 499]---> BDD-cost:   12
c ---[ 497]---> BDD-cost:    9
c ---[ 496]---> BDD-cost:    2
c ---[ 491]---> BDD-cost:    2
c ---[ 490]---> BDD-cost:    2
c ---[ 488]---> BDD-cost:    2
c ---[ 485]---> BDD-cost:    2
c ---[ 482]---> BDD-cost:    2
c ---[ 480]---> BDD-cost:    2
c ---[ 478]---> BDD-cost:    2
c ---[ 476]---> BDD-cost:    2
c ---[ 475]---> BDD-cost:    2
c ---[ 471]---> BDD-cost:    2
c ---[ 467]---> BDD-cost:    2
c ---[ 466]---> BDD-cost:    2
c ---[ 465]---> BDD-cost:    2
c ---[ 451]---> BDD-cost:    2
c ---[ 439]---> Sorter-cost: 1703     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 437]---> BDD-cost:   60
c ---[ 435]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 433]---> BDD-cost:   54
c ---[ 431]---> Sorter-cost: 1021     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 429]---> Sorter-cost:  621     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> BDD-cost:   60
c ---[ 423]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 419]---> BDD-cost:  107
c ---[ 417]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> BDD-cost:   60
c ---[ 413]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 411]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> BDD-cost:   60
c ---[ 403]---> Sorter-cost:  814     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost:  844     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 399]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 397]---> Sorter-cost:  815     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> Sorter-cost:  561     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 393]---> BDD-cost:  119
c ---[ 391]---> BDD-cost:   60
c ---[ 389]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 387]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost: 1092     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 383]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 381]---> Sorter-cost: 2166     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 379]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> Sorter-cost: 1072     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 375]---> BDD-cost:   60
c ---[ 373]---> Sorter-cost: 1066     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> BDD-cost:   73
c ---[ 369]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 367]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 363]---> BDD-cost:   60
c ---[ 361]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 359]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 357]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 355]---> BDD-cost:   70
c ---[ 353]---> Sorter-cost:  816     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 351]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> BDD-cost:   54
c ---[ 347]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 345]---> BDD-cost:  109
c ---[ 343]---> BDD-cost:   96
c ---[ 341]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 339]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 337]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 333]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 331]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 329]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 327]---> BDD-cost:   60
c ---[ 325]---> Sorter-cost: 1227     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 323]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 321]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> BDD-cost:   98
c ---[ 317]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 315]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 313]---> Sorter-cost:  331     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> BDD-cost:   99
c ---[ 307]---> BDD-cost:  114
c ---[ 305]---> BDD-cost:   62
c ---[ 303]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:  815     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 295]---> Sorter-cost:  789     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 293]---> Sorter-cost:  709     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 287]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 285]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> BDD-cost:   60
c ---[ 281]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 279]---> Sorter-cost:  816     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 277]---> BDD-cost:   60
c ---[ 275]---> BDD-cost:   60
c ---[ 273]---> BDD-cost:   46
c ---[ 271]---> BDD-cost:   60
c ---[ 269]---> BDD-cost:   62
c ---[ 267]---> BDD-cost:   46
c ---[ 265]---> BDD-cost:   60
c ---[ 263]---> BDD-cost:   62
c ---[ 261]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 259]---> Sorter-cost:  897     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 257]---> BDD-cost:   99
c ---[ 255]---> BDD-cost:  110
c ---[ 253]---> BDD-cost:  123
c ---[ 251]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost:  881     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost:  995     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 245]---> BDD-cost:    0
c ---[ 243]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 241]---> BDD-cost:   60
c ---[ 239]---> BDD-cost:   99
c ---[ 237]---> BDD-cost:   60
c ---[ 235]---> BDD-cost:  123
c ---[ 233]---> BDD-cost:  110
c ---[ 231]---> BDD-cost:  123
c ---[ 229]---> Sorter-cost:  719     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 227]---> BDD-cost:   60
c ---[ 225]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> BDD-cost:  112
c ---[ 219]---> BDD-cost:   98
c ---[ 217]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost: 1444     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 211]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost:  313     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost: 1207     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 203]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 201]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost: 1021     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 197]---> Sorter-cost: 1295     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 195]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 193]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 187]---> BDD-cost:   54
c ---[ 185]---> Sorter-cost: 1024     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 179]---> Sorter-cost: 1497     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 177]---> Sorter-cost: 1434     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 175]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 163]---> Sorter-cost: 1004     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 157]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 155]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 153]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 151]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> BDD-cost:   60
c ---[ 147]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> BDD-cost:   96
c ---[ 139]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> BDD-cost:   54
c ---[ 135]---> BDD-cost:   60
c ---[ 133]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 131]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> BDD-cost:   73
c ---[ 127]---> Sorter-cost:  426     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 125]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 121]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> BDD-cost:   73
c ---[ 115]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost: 1262     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost: 1256     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost: 1093     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost: 1207     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:   10
c ---[  96]---> BDD-cost:   10
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   10
c ---[  93]---> BDD-cost:   10
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   10
c ---[  90]---> BDD-cost:   10
c ---[  89]---> BDD-cost:   10
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   10
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:   10
c ---[  83]---> BDD-cost:   10
c ---[  82]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   10
c ---[  80]---> BDD-cost:   10
c ---[  79]---> BDD-cost:   10
c ---[  78]---> BDD-cost:   10
c ---[  77]---> BDD-cost:   10
c ---[  76]---> BDD-cost:   10
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   10
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   10
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   10
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   10
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   10
c ---[  60]---> BDD-cost:   10
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   10
c ---[  57]---> BDD-cost:   10
c ---[  56]---> BDD-cost:   10
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   10
c ---[  53]---> BDD-cost:   10
c ---[  52]---> BDD-cost:   10
c ---[  51]---> BDD-cost:   10
c ---[  50]---> BDD-cost:   10
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   10
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   10
c ---[  44]---> BDD-cost:   10
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   10
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   10
c ---[  38]---> BDD-cost:   10
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   10
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   10
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:   10
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   10
c ---[  24]---> BDD-cost:   10
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   10
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   10
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   10
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   10
c ---[   1]---> BDD-cost:   10
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  224674   533928 |   74891       0        0     nan |  0.000 % |
c |       100 |  224670   533920 |   82380      98      535     5.5 |  6.750 % |
c |       251 |  224540   533633 |   90618     234     1181     5.0 |  6.795 % |
c |       476 |  224355   533219 |   99679     441     2037     4.6 |  6.856 % |
c |       814 |  224252   532987 |  109647     775     4417     5.7 |  6.889 % |
c |      1320 |  224183   532833 |  120612    1277    10452     8.2 |  6.913 % |
c |      2079 |  224169   532805 |  132673    2029    17250     8.5 |  6.921 % |
c |      3222 |  223827   532044 |  145941    3115    25236     8.1 |  7.040 % |
c |      4930 |  223707   531780 |  160535    4804    42908     8.9 |  7.086 % |
c |      7495 |  223391   531076 |  176589    7323    84537    11.5 |  7.198 % |
c |     11339 |  222872   529922 |  194247   11101   161153    14.5 |  7.379 % |
c |     17106 |  221646   527190 |  213672   16692   222771    13.3 |  7.803 % |
c |     25755 |  218600   520387 |  235040   24984   298094    11.9 |  8.848 % |
c |     38731 |  217418   517758 |  258544   37827   504869    13.3 |  9.263 % |
c |     58193 |  214876   512082 |  284398   56951   756979    13.3 | 10.135 % |
c |     87385 |  212569   506944 |  312838   85800  1257507    14.7 | 10.942 % |
c |    131174 |  209852   500863 |  344122  129212  2075274    16.1 | 11.884 % |
c ==============================================================================
c Found solution: 18020349499994871
c ---[   0]---> 
c *** TERMINATED ***
s SATISFIABLE
v x1_bit_7 x1_bit_6 x1_bit_5 x1_bit_4 x1_bit_3 x1_bit_2 -x1_bit_1 x1_bit0 x1_bit1 -x1_bit2 x4_bit_7 x4_bit_6 x4_bit_5 x4_bit_4 x4_bit_3 x4_bit_2 -x4_bit_1 x4_bit0 -x4_bit1 x4_bit2 -x4_bit3 x4_bit4 -x4_bit5 x5_bit_7 -x5_bit_6 x5_bit_5 -x5_bit_4 -x5_bit_3 x5_bit_2 -x5_bit_1 x5_bit0 x5_bit1 -x5_bit2 x7_bit_7 x7_bit_6 x7_bit_5 x7_bit_4 -x7_bit_3 x7_bit_2 -x7_bit_1 x7_bit0 x7_bit1 x7_bit2 -x7_bit3 x7_bit4 -x7_bit5 x8_bit_7 x8_bit_6 x8_bit_5 x8_bit_4 -x8_bit_3 -x8_bit_2 x8_bit_1 -x8_bit0 -x8_bit1 -x8_bit2 -x12_bit_7 -x12_bit_6 -x12_bit_5 -x12_bit_4 -x12_bit_3 x12_bit_2 x12_bit_1 -x12_bit0 -x12_bit1 -x12_bit2 x14_bit_7 x14_bit_6 -x14_bit_5 x14_bit_4 x14_bit_3 x14_bit_2 -x14_bit_1 x14_bit0 x14_bit1 x14_bit2 -x14_bit3 -x14_bit4 x14_bit5 -x15_bit_7 -x15_bit_6 -x15_bit_5 -x15_bit_4 -x15_bit_3 x15_bit_2 -x15_bit_1 -x15_bit0 -x15_bit1 x15_bit2 x15_bit3 x15_bit4 -x15_bit5 -x16_bit_7 -x16_bit_6 x16_bit_5 x16_bit_4 x16_bit_3 x16_bit_2 -x16_bit_1 x16_bit0 -x16_bit1 x16_bit2 x16_bit3 -x16_bit4 -x16_bit5 x17_bit_7 x17_bit_6 x17_bit_5 x17_bit_4 -x17_bit_3 x17_bit_2 x17_bit_1 x17_bit0 x17_bit1 -x17_bit2 -x17_bit3 -x17_bit4 x17_bit5 -x18_bit_7 -x18_bit_6 -x18_bit_5 -x18_bit_4 -x18_bit_3 x18_bit_2 -x18_bit_1 -x18_bit0 x18_bit1 -x18_bit2 x18_bit3 x18_bit4 x18_bit5 x22_bit_7 x22_bit_6 x22_bit_5 -x22_bit_4 x22_bit_3 -x22_bit_2 -x22_bit_1 -x22_bit0 x22_bit1 -x22_bit2 x25_bit_7 -x25_bit_6 x25_bit_5 x25_bit_4 x25_bit_3 x25_bit_2 x25_bit_1 -x25_bit0 x25_bit1 x25_bit2 -x25_bit3 -x25_bit4 x25_bit5 x27_bit_7 -x27_bit_6 x27_bit_5 x27_bit_4 x27_bit_3 x27_bit_2 x27_bit_1 -x27_bit0 -x27_bit1 -x27_bit2 x27_bit3 -x27_bit4 -x27_bit5 x28_bit_7 x28_bit_6 x28_bit_5 x28_bit_4 -x28_bit_3 -x28_bit_2 -x28_bit_1 -x28_bit0 -x28_bit1 -x28_bit2 x28_bit3 -x28_bit4 x28_bit5 x29_bit_7 x29_bit_6 x29_bit_5 x29_bit_4 -x29_bit_3 x29_bit_2 -x29_bit_1 x29_bit0 -x29_bit1 x29_bit2 -x29_bit3 -x29_bit4 -x29_bit5 x30_bit_7 x30_bit_6 x30_bit_5 x30_bit_4 -x30_bit_3 -x30_bit_2 -x30_bit_1 -x30_bit0 x30_bit1 -x30_bit2 x30_bit3 -x30_bit4 -x30_bit5 x31_bit_7 x31_bit_6 x31_bit_5 x31_bit_4 -x31_bit_3 x31_bit_2 -x31_bit_1 x31_bit0 x31_bit1 -x31_bit2 -x31_bit3 -x31_bit4 x31_bit5 x32_bit_7 -x32_bit_6 -x32_bit_5 -x32_bit_4 -x32_bit_3 x32_bit_2 x32_bit_1 x32_bit0 x32_bit1 x32_bit2 -x32_bit3 x32_bit4 -x32_bit5 x39_bit_7 x39_bit_6 -x39_bit_5 -x39_bit_4 x39_bit_3 x39_bit_2 x39_bit_1 -x39_bit0 -x39_bit1 x39_bit2 -x39_bit3 x39_bit4 x39_bit5 -x40_bit_7 -x40_bit_6 -x40_bit_5 -x40_bit_4 -x40_bit_3 -x40_bit_2 -x40_bit_1 -x40_bit0 x40_bit1 x40_bit2 -x41_bit_7 -x41_bit_6 x41_bit_5 x41_bit_4 -x41_bit_3 -x41_bit_2 x41_bit_1 -x41_bit0 x41_bit1 -x41_bit2 x41_bit3 -x41_bit4 -x41_bit5 -x42_bit_7 -x42_bit_6 x42_bit_5 x42_bit_4 -x42_bit_3 -x42_bit_2 x42_bit_1 x42_bit0 -x42_bit1 -x42_bit2 x42_bit3 -x42_bit4 -x42_bit5 -x44_bit_7 -x44_bit_6 x44_bit_5 x44_bit_4 -x44_bit_3 -x44_bit_2 x44_bit_1 x44_bit0 x44_bit1 x44_bit2 -x44_bit3 -x44_bit4 x44_bit5 -x47_bit_7 x47_bit_6 x47_bit_5 x47_bit_4 -x47_bit_3 x47_bit_2 x47_bit_1 x47_bit0 -x47_bit1 -x47_bit2 -x50_bit_7 x50_bit_6 x50_bit_5 x50_bit_4 x50_bit_3 -x50_bit_2 x50_bit_1 x50_bit0 x50_bit1 x50_bit2 x50_bit3 -x50_bit4 x50_bit5 -x51_bit_7 x51_bit_6 x51_bit_5 x51_bit_4 x51_bit_3 -x51_bit_2 x51_bit_1 x51_bit0 -x51_bit1 -x51_bit2 -x51_bit3 x51_bit4 -x51_bit5 -x52_bit_7 -x52_bit_6 -x52_bit_5 -x52_bit_4 -x52_bit_3 -x52_bit_2 -x52_bit_1 -x52_bit0 -x52_bit1 -x52_bit2 -x52_bit3 -x52_bit4 -x52_bit5 -x53_bit_7 x53_bit_6 x53_bit_5 x53_bit_4 x53_bit_3 -x53_bit_2 x53_bit_1 -x53_bit0 x53_bit1 x53_bit2 -x53_bit3 x53_bit4 -x53_bit5 x54_bit_7 x54_bit_6 x54_bit_5 x54_bit_4 x54_bit_3 x54_bit_2 -x54_bit_1 x54_bit0 -x54_bit1 x54_bit2 -x54_bit3 -x54_bit4 x54_bit5 x55_bit_7 x55_bit_6 x55_bit_5 x55_bit_4 x55_bit_3 x55_bit_2 -x55_bit_1 x55_bit0 x55_bit1 x55_bit2 -x55_bit3 -x55_bit4 -x55_bit5 x57_bit_7 -x57_bit_6 -x57_bit_5 -x57_bit_4 x57_bit_3 x57_bit_2 x57_bit_1 x57_bit0 x57_bit1 -x57_bit2 -x59_bit_7 -x59_bit_6 x59_bit_5 -x59_bit_4 x59_bit_3 -x59_bit_2 x59_bit_1 x59_bit0 -x59_bit1 x59_bit2 x62_bit_7 x62_bit_6 x62_bit_5 -x62_bit_4 x62_bit_3 x62_bit_2 -x62_bit_1 -x62_bit0 -x62_bit1 x62_bit2 -x62_bit3 x62_bit4 -x62_bit5 x63_bit_7 x63_bit_6 x63_bit_5 -x63_bit_4 x63_bit_3 x63_bit_2 -x63_bit_1 -x63_bit0 x63_bit1 -x63_bit2 -x63_bit3 x63_bit4 x63_bit5 -x64_bit_7 x64_bit_6 x64_bit_5 -x64_bit_4 -x64_bit_3 x64_bit_2 -x64_bit_1 x64_bit0 x64_bit1 -x64_bit2 -x64_bit3 -x64_bit4 -x64_bit5 -x65_bit_7 x65_bit_6 x65_bit_5 -x65_bit_4 -x65_bit_3 x65_bit_2 -x65_bit_1 x65_bit0 -x65_bit1 -x65_bit2 -x65_bit3 -x65_bit4 x65_bit5 -x66_bit_7 -x66_bit_6 -x66_bit_5 x66_bit_4 x66_bit_3 -x66_bit_2 x66_bit_1 x66_bit0 -x66_bit1 -x66_bit2 x66_bit3 -x66_bit4 -x66_bit5 x67_bit_7 x67_bit_6 -x67_bit_5 x67_bit_4 x67_bit_3 x67_bit_2 -x67_bit_1 -x67_bit0 -x67_bit1 -x67_bit2 x68_bit_7 -x68_bit_6 x68_bit_5 -x68_bit_4 -x68_bit_3 -x68_bit_2 x68_bit_1 x68_bit0 x68_bit1 -x68_bit2 -x71_bit_7 -x71_bit_6 -x71_bit_5 -x71_bit_4 -x71_bit_3 -x71_bit_2 -x71_bit_1 -x71_bit0 -x71_bit1 -x71_bit2 -x72_bit_7 -x72_bit_6 -x72_bit_5 x72_bit_4 x72_bit_3 -x72_bit_2 -x72_bit_1 x72_bit0 x72_bit1 x72_bit2 x72_bit3 x72_bit4 -x72_bit5 -x75_bit_7 -x75_bit_6 -x75_bit_5 x75_bit_4 -x75_bit_3 x75_bit_2 x75_bit_1 x75_bit0 x75_bit1 -x75_bit2 x75_bit3 -x75_bit4 x75_bit5 -x76_bit_7 -x76_bit_6 -x76_bit_5 x76_bit_4 x76_bit_3 -x76_bit_2 -x76_bit_1 -x76_bit0 -x76_bit1 -x76_bit2 -x76_bit3 -x76_bit4 x76_bit5 -x77_bit_7 -x77_bit_6 -x77_bit_5 x77_bit_4 -x77_bit_3 x77_bit_2 x77_bit_1 x77_bit0 x77_bit1 x77_bit2 -x77_bit3 x77_bit4 -x77_bit5 x78_bit_7 -x78_bit_6 x78_bit_5 -x78_bit_4 -x78_bit_3 -x78_bit_2 -x78_bit_1 -x78_bit0 -x78_bit1 x78_bit2 -x78_bit3 x78_bit4 x78_bit5 -x79_bit_7 -x79_bit_6 -x79_bit_5 -x79_bit_4 -x79_bit_3 -x79_bit_2 -x79_bit_1 -x79_bit0 -x79_bit1 -x79_bit2 x79_bit3 x79_bit4 -x79_bit5 -x80_bit_7 -x80_bit_6 x80_bit_5 -x80_bit_4 x80_bit_3 x80_bit_2 -x80_bit_1 x80_bit0 -x80_bit1 x80_bit2 x80_bit3 -x80_bit4 -x80_bit5 x81_bit_7 x81_bit_6 -x81_bit_5 x81_bit_4 -x81_bit_3 -x81_bit_2 x81_bit_1 -x81_bit0 x81_bit1 x81_bit2 -x81_bit3 x81_bit4 -x81_bit5 -x85_bit_7 -x85_bit_6 -x85_bit_5 x85_bit_4 -x85_bit_3 x85_bit_2 x85_bit_1 -x85_bit0 -x85_bit1 -x85_bit2 x85_bit3 x85_bit4 -x85_bit5 x86_bit_7 -x86_bit_6 x86_bit_5 -x86_bit_4 -x86_bit_3 -x86_bit_2 -x86_bit_1 x86_bit0 -x86_bit1 x86_bit2 -x86_bit3 x86_bit4 x86_bit5 -x87_bit_7 -x87_bit_6 -x87_bit_5 -x87_bit_4 x87_bit_3 -x87_bit_2 -x87_bit_1 x87_bit0 x87_bit1 -x87_bit2 x87_bit3 -x87_bit4 -x87_bit5 -x88_bit_7 -x88_bit_6 -x88_bit_5 -x88_bit_4 x88_bit_3 -x88_bit_2 x88_bit_1 -x88_bit0 -x88_bit1 -x88_bit2 x88_bit3 -x88_bit4 -x88_bit5 x89_bit_7 x89_bit_6 x89_bit_5 x89_bit_4 -x89_bit_3 -x89_bit_2 -x89_bit_1 x89_bit0 x89_bit1 -x89_bit2 x91_bit_7 -x91_bit_6 -x91_bit_5 -x91_bit_4 -x91_bit_3 x91_bit_2 -x91_bit_1 -x91_bit0 -x91_bit1 x91_bit2 x91_bit3 -x91_bit4 x91_bit5 x92_bit_7 -x92_bit_6 -x92_bit_5 -x92_bit_4 -x92_bit_3 x92_bit_2 -x92_bit_1 -x92_bit0 x92_bit1 x92_bit2 x92_bit3 -x92_bit4 -x92_bit5 -x93_bit_7 x93_bit_6 -x93_bit_5 -x93_bit_4 -x93_bit_3 x93_bit_2 x93_bit_1 x93_bit0 x93_bit1 -x93_bit2 -x93_bit3 x93_bit4 x93_bit5 -x94_bit_7 -x94_bit_6 x94_bit_5 x94_bit_4 -x94_bit_3 -x94_bit_2 -x94_bit_1 -x94_bit0 -x94_bit1 -x94_bit2 -x94_bit3 -x94_bit4 -x94_bit5 -x103_bit_7 -x103_bit_6 x103_bit_5 -x103_bit_4 x103_bit_3 x103_bit_2 x103_bit_1 x103_bit0 -x103_bit1 x103_bit2 -x103_bit3 -x103_bit4 x103_bit5 -x104_bit_7 x104_bit_6 -x104_bit_5 -x104_bit_4 -x104_bit_3 x104_bit_2 x104_bit_1 x104_bit0 -x104_bit1 -x104_bit2 -x104_bit3 -x104_bit4 x104_bit5 x107_bit_7 -x107_bit_6 x107_bit_5 x107_bit_4 x107_bit_3 x107_bit_2 -x107_bit_1 -x107_bit0 x107_bit1 -x107_bit2 x108_bit_7 x108_bit_6 x108_bit_5 -x108_bit_4 -x108_bit_3 x108_bit_2 -x108_bit_1 -x108_bit0 -x108_bit1 -x108_bit2 -x110_bit_7 x110_bit_6 -x110_bit_5 -x110_bit_4 -x110_bit_3 -x110_bit_2 -x110_bit_1 x110_bit0 x110_bit1 x110_bit2 -x110_bit3 -x110_bit4 x110_bit5 -x111_bit_7 x111_bit_6 -x111_bit_5 -x111_bit_4 -x111_bit_3 -x111_bit_2 -x111_bit_1 -x111_bit0 x111_bit1 -x111_bit2 x111_bit3 -x111_bit4 -x111_bit5 -x112_bit_7 -x112_bit_6 x112_bit_5 -x112_bit_4 x112_bit_3 -x112_bit_2 -x112_bit_1 -x112_bit0 -x112_bit1 x112_bit2 x112_bit3 x112_bit4 -x112_bit5 x113_bit_7 x113_bit_6 -x113_bit_5 x113_bit_4 -x113_bit_3 x113_bit_2 -x113_bit_1 x113_bit0 -x113_bit1 x113_bit2 -x113_bit3 -x113_bit4 x113_bit5 x115_bit_7 x115_bit_6 x115_bit_5 x115_bit_4 -x115_bit_3 x115_bit_2 x115_bit_1 x115_bit0 -x115_bit1 -x115_bit2 -x118_bit_7 -x118_bit_6 -x118_bit_5 x118_bit_4 -x118_bit_3 x118_bit_2 -x118_bit_1 -x118_bit0 x118_bit1 x118_bit2 -x118_bit3 x118_bit4 -x118_bit5 -x119_bit_7 -x119_bit_6 -x119_bit_5 x119_bit_4 x119_bit_3 -x119_bit_2 x119_bit_1 x119_bit0 -x119_bit1 -x119_bit2 x119_bit3 -x119_bit4 x119_bit5 x123_bit_7 x123_bit_6 x123_bit_5 x123_bit_4 x123_bit_3 x123_bit_2 -x123_bit_1 x123_bit0 -x123_bit1 -x123_bit2 -x124_bit_7 -x124_bit_6 -x124_bit_5 x124_bit_4 x124_bit_3 x124_bit_2 -x124_bit_1 x124_bit0 x124_bit1 -x124_bit2 -x124_bit3 x124_bit4 x124_bit5 x126_bit_7 -x126_bit_6 -x126_bit_5 x126_bit_4 x126_bit_3 -x126_bit_2 x126_bit_1 x126_bit0 x126_bit1 -x126_bit2 -x126_bit3 -x126_bit4 -x126_bit5 -x127_bit_7 -x127_bit_6 -x127_bit_5 x127_bit_4 x127_bit_3 -x127_bit_2 x127_bit_1 x127_bit0 x127_bit1 x127_bit2 x127_bit3 -x127_bit4 x127_bit5 x129_bit_7 x129_bit_6 x129_bit_5 -x129_bit_4 -x129_bit_3 x129_bit_2 x129_bit_1 x129_bit0 x129_bit1 -x129_bit2 -x130_bit_7 -x130_bit_6 -x130_bit_5 -x130_bit_4 -x130_bit_3 -x130_bit_2 -x130_bit_1 -x130_bit0 -x130_bit1 x130_bit2 x131_bit_7 x131_bit_6 x131_bit_5 -x131_bit_4 x131_bit_3 x131_bit_2 -x131_bit_1 x131_bit0 -x131_bit1 x131_bit2 x131_bit3 x131_bit4 -x131_bit5 -x132_bit_7 -x132_bit_6 -x132_bit_5 -x132_bit_4 -x132_bit_3 -x132_bit_2 -x132_bit_1 x132_bit0 -x132_bit1 x132_bit2 x134_bit_7 x134_bit_6 -x134_bit_5 -x134_bit_4 -x134_bit_3 -x134_bit_2 -x134_bit_1 x134_bit0 x134_bit1 -x134_bit2 -x136_bit_7 -x136_bit_6 -x136_bit_5 -x136_bit_4 -x136_bit_3 x136_bit_2 x136_bit_1 x136_bit0 -x136_bit1 -x136_bit2 -x136_bit3 -x136_bit4 -x136_bit5 -x137_bit_7 x137_bit_6 -x137_bit_5 -x137_bit_4 x137_bit_3 x137_bit_2 x137_bit_1 x137_bit0 x137_bit1 x137_bit2 x137_bit3 -x137_bit4 -x137_bit5 -x138_bit_7 x138_bit_6 x138_bit_5 x138_bit_4 x138_bit_3 x138_bit_2 -x138_bit_1 -x138_bit0 -x138_bit1 x138_bit2 -x138_bit3 -x138_bit4 x138_bit5 -x140_bit_7 -x140_bit_6 -x140_bit_5 -x140_bit_4 -x140_bit_3 x140_bit_2 x140_bit_1 -x140_bit0 -x140_bit1 -x140_bit2 -x140_bit3 -x140_bit4 x140_bit5 -x141_bit_7 -x141_bit_6 -x141_bit_5 x141_bit_4 x141_bit_3 x141_bit_2 -x141_bit_1 -x141_bit0 -x141_bit1 -x141_bit2 -x142_bit_7 -x142_bit_6 x142_bit_5 x142_bit_4 x142_bit_3 x142_bit_2 x142_bit_1 x142_bit0 x142_bit1 -x142_bit2 x144_bit_7 -x144_bit_6 x144_bit_5 x144_bit_4 x144_bit_3 x144_bit_2 x144_bit_1 x144_bit0 x144_bit1 -x144_bit2 x144_bit3 x144_bit4 -x144_bit5 x145_bit_7 x145_bit_6 x145_bit_5 x145_bit_4 x145_bit_3 x145_bit_2 x145_bit_1 -x145_bit0 -x145_bit1 -x145_bit2 x146_bit_7 -x146_bit_6 -x146_bit_5 -x146_bit_4 -x146_bit_3 -x146_bit_2 -x146_bit_1 -x146_bit0 -x146_bit1 -x146_bit2 x147_bit_7 -x147_bit_6 -x147_bit_5 -x147_bit_4 -x147_bit_3 x147_bit_2 x147_bit_1 x147_bit0 x147_bit1 x147_bit2 x147_bit3 -x147_bit4 -x147_bit5 -x152_bit_7 x152_bit_6 x152_bit_5 x152_bit_4 -x152_bit_3 -x152_bit_2 x152_bit_1 -x152_bit0 -x152_bit1 -x152_bit2 x152_bit3 -x152_bit4 -x152_bit5 x153_bit_7 x153_bit_6 x153_bit_5 x153_bit_4 -x153_bit_3 -x153_bit_2 -x153_bit_1 -x153_bit0 x153_bit1 x153_bit2 x153_bit3 -x153_bit4 x153_bit5 -x154_bit_7 -x154_bit_6 -x154_bit_5 -x154_bit_4 -x154_bit_3 -x154_bit_2 x154_bit_1 x154_bit0 -x154_bit1 -x154_bit2 x155_bit_7 -x155_bit_6 x155_bit_5 -x155_bit_4 -x155_bit_3 x155_bit_2 -x155_bit_1 x155_bit0 -x155_bit1 -x155_bit2 -x155_bit3 x155_bit4 x155_bit5 -x157_bit_7 x157_bit_6 x157_bit_5 x157_bit_4 -x157_bit_3 -x157_bit_2 -x157_bit_1 -x157_bit0 -x157_bit1 -x157_bit2 x158_bit_7 -x158_bit_6 x158_bit_5 x158_bit_4 -x158_bit_3 x158_bit_2 -x158_bit_1 x158_bit0 -x158_bit1 x158_bit2 -x158_bit3 x158_bit4 -x158_bit5 -x159_bit_7 -x159_bit_6 -x159_bit_5 -x159_bit_4 x159_bit_3 x159_bit_2 x159_bit_1 -x159_bit0 x159_bit1 -x159_bit2 -x159_bit3 -x159_bit4 x159_bit5 -x162_bit_7 -x162_bit_6 -x162_bit_5 -x162_bit_4 x162_bit_3 x162_bit_2 x162_bit_1 -x162_bit0 -x162_bit1 x162_bit2 -x162_bit3 -x162_bit4 -x162_bit5 x163_bit_7 x163_bit_6 x163_bit_5 x163_bit_4 -x163_bit_3 x163_bit_2 -x163_bit_1 x163_bit0 x163_bit1 -x163_bit2 x163_bit3 x163_bit4 -x163_bit5 x165_bit_7 -x165_bit_6 -x165_bit_5 -x165_bit_4 x165_bit_3 -x165_bit_2 -x165_bit_1 -x165_bit0 -x165_bit1 -x165_bit2 -x167_bit_7 -x167_bit_6 -x167_bit_5 -x167_bit_4 -x167_bit_3 -x167_bit_2 -x167_bit_1 -x167_bit0 -x167_bit1 x167_bit2 -x170_bit_7 -x170_bit_6 -x170_bit_5 -x170_bit_4 -x170_bit_3 -x170_bit_2 -x170_bit_1 -x170_bit0 -x170_bit1 x170_bit2 x172_bit_7 -x172_bit_6 x172_bit_5 x172_bit_4 x172_bit_3 -x172_bit_2 -x172_bit_1 -x172_bit0 x172_bit1 -x172_bit2 x173_bit_7 -x173_bit_6 x173_bit_5 x173_bit_4 -x173_bit_3 -x173_bit_2 x173_bit_1 x173_bit0 x173_bit1 -x173_bit2 -x173_bit3 -x173_bit4 -x173_bit5 -x174_bit_7 -x174_bit_6 -x174_bit_5 -x174_bit_4 -x174_bit_3 -x174_bit_2 -x174_bit_1 -x174_bit0 -x174_bit1 x174_bit2 -x174_bit3 x174_bit4 -x174_bit5 -x176_bit_7 -x176_bit_6 -x176_bit_5 -x176_bit_4 x176_bit_3 x176_bit_2 -x176_bit_1 x176_bit0 x176_bit1 -x176_bit2 -x176_bit3 -x176_bit4 x176_bit5 x177_bit_7 x177_bit_6 -x177_bit_5 x177_bit_4 -x177_bit_3 x177_bit_2 -x177_bit_1 x177_bit0 -x177_bit1 -x177_bit2 x177_bit3 x177_bit4 x177_bit5 x179_bit_7 x179_bit_6 -x179_bit_5 x179_bit_4 x179_bit_3 -x179_bit_2 x179_bit_1 -x179_bit0 -x179_bit1 -x179_bit2 x179_bit3 -x179_bit4 -x179_bit5 x180_bit_7 x180_bit_6 -x180_bit_5 x180_bit_4 -x180_bit_3 x180_bit_2 -x180_bit_1 x180_bit0 -x180_bit1 -x180_bit2 -x180_bit3 x180_bit4 x180_bit5 x184_bit_7 x184_bit_6 x184_bit_5 -x184_bit_4 x184_bit_3 -x184_bit_2 x184_bit_1 -x184_bit0 -x184_bit1 -x184_bit2 -x187_bit_7 x187_bit_6 x187_bit_5 x187_bit_4 x187_bit_3 x187_bit_2 x187_bit_1 -x187_bit0 -x187_bit1 x187_bit2 x187_bit3 -x187_bit4 x187_bit5 x188_bit_7 -x188_bit_6 -x188_bit_5 x188_bit_4 x188_bit_3 -x188_bit_2 x188_bit_1 x188_bit0 x188_bit1 -x188_bit2 -x190_bit_7 -x190_bit_6 -x190_bit_5 -x190_bit_4 -x190_bit_3 x190_bit_2 x190_bit_1 -x190_bit0 x190_bit1 x190_bit2 x190_bit3 -x190_bit4 x190_bit5 x191_bit_7 x191_bit_6 -x191_bit_5 -x191_bit_4 x191_bit_3 -x191_bit_2 -x191_bit_1 -x191_bit0 -x191_bit1 -x191_bit2 x192_bit_7 x192_bit_6 -x192_bit_5 -x192_bit_4 -x192_bit_3 -x192_bit_2 x192_bit_1 -x192_bit0 -x192_bit1 -x192_bit2 -x193_bit_7 -x193_bit_6 -x193_bit_5 x193_bit_4 x193_bit_3 x193_bit_2 -x193_bit_1 x193_bit0 -x193_bit1 -x193_bit2 -x193_bit3 x193_bit4 x193_bit5 x194_bit_7 x194_bit_6 x194_bit_5 -x194_bit_4 x194_bit_3 x194_bit_2 x194_bit_1 x194_bit0 -x194_bit1 -x194_bit2 x194_bit3 -x194_bit4 x194_bit5 x196_bit_7 -x196_bit_6 x196_bit_5 -x196_bit_4 -x196_bit_3 -x196_bit_2 -x196_bit_1 -x196_bit0 -x196_bit1 -x196_bit2 -x197_bit_7 -x197_bit_6 -x197_bit_5 -x197_bit_4 x197_bit_3 -x197_bit_2 -x197_bit_1 x197_bit0 -x197_bit1 -x197_bit2 -x197_bit3 x197_bit4 -x197_bit5 x198_bit_7 x198_bit_6 x198_bit_5 x198_bit_4 -x198_bit_3 -x198_bit_2 x198_bit_1 x198_bit0 -x198_bit1 -x198_bit2 x198_bit3 -x198_bit4 -x198_bit5 x203_bit_7 -x203_bit_6 x203_bit_5 -x203_bit_4 x203_bit_3 -x203_bit_2 x203_bit_1 -x203_bit0 -x203_bit1 x203_bit2 -x203_bit3 -x203_bit4 -x203_bit5 x206_bit_7 x206_bit_6 x206_bit_5 x206_bit_4 x206_bit_3 x206_bit_2 -x206_bit_1 -x206_bit0 -x206_bit1 -x206_bit2 -x206_bit3 -x206_bit4 x206_bit5 x207_bit_7 x207_bit_6 -x207_bit_5 -x207_bit_4 -x207_bit_3 x207_bit_2 x207_bit_1 x207_bit0 -x207_bit1 -x207_bit2 x212_bit_7 -x212_bit_6 -x212_bit_5 x212_bit_4 x212_bit_3 -x212_bit_2 -x212_bit_1 -x212_bit0 -x212_bit1 -x212_bit2 -x213_bit_7 x213_bit_6 -x213_bit_5 -x213_bit_4 x213_bit_3 -x213_bit_2 -x213_bit_1 -x213_bit0 -x213_bit1 -x213_bit2 x214_bit_7 x214_bit_6 x214_bit_5 -x214_bit_4 -x214_bit_3 x214_bit_2 x214_bit_1 x214_bit0 -x214_bit1 -x214_bit2 -x216_bit_7 x216_bit_6 -x216_bit_5 x216_bit_4 x216_bit_3 -x216_bit_2 x216_bit_1 -x216_bit0 -x216_bit1 x216_bit2 x216_bit3 x216_bit4 -x216_bit5 x217_bit_7 -x217_bit_6 x217_bit_5 x217_bit_4 -x217_bit_3 -x217_bit_2 -x217_bit_1 x217_bit0 x217_bit1 -x217_bit2 -x217_bit3 x217_bit4 x217_bit5 x222_bit_7 x222_bit_6 x222_bit_5 x222_bit_4 x222_bit_3 x222_bit_2 -x222_bit_1 -x222_bit0 x222_bit1 -x222_bit2 -x222_bit3 -x222_bit4 -x222_bit5 -x226_bit_7 -x226_bit_6 -x226_bit_5 x226_bit_4 x226_bit_3 x226_bit_2 -x226_bit_1 -x226_bit0 x226_bit1 -x226_bit2 x2_bit_7 x2_bit_6 x2_bit_5 x2_bit_4 x2_bit_3 x2_bit_2 -x2_bit_1 x2_bit0 x2_bit1 x2_bit2 -x2_bit3 -x2_bit4 x2_bit5 x3_bit_7 x3_bit_6 x3_bit_5 x3_bit_4 x3_bit_3 x3_bit_2 -x3_bit_1 -x3_bit0 x3_bit1 x3_bit2 -x3_bit3 -x3_bit4 x3_bit5 x6_bit_7 -x6_bit_6 -x6_bit_5 -x6_bit_4 x6_bit_3 x6_bit_2 -x6_bit_1 x6_bit0 -x6_bit1 -x6_bit2 -x6_bit3 x6_bit4 -x6_bit5 x9_bit_7 x9_bit_6 -x9_bit_5 x9_bit_4 x9_bit_3 -x9_bit_2 x9_bit_1 x9_bit0 x9_bit1 x9_bit2 -x9_bit3 -x9_bit4 -x9_bit5 -x10_bit_7 x10_bit_6 -x10_bit_5 x10_bit_4 -x10_bit_3 -x10_bit_2 x10_bit_1 x10_bit0 -x10_bit1 x10_bit2 x10_bit3 x10_bit4 -x10_bit5 x11_bit_7 -x11_bit_6 -x11_bit_5 x11_bit_4 -x11_bit_3 -x11_bit_2 -x11_bit_1 x11_bit0 -x11_bit1 -x11_bit2 -x11_bit3 -x11_bit4 x11_bit5 -x13_bit_7 -x13_bit_6 -x13_bit_5 x13_bit_4 x13_bit_3 -x13_bit_2 -x13_bit_1 x13_bit0 x13_bit1 -x13_bit2 -x13_bit3 -x13_bit4 -x13_bit5 -x19_bit_7 x19_bit_6 -x19_bit_5 -x19_bit_4 -x19_bit_3 x19_bit_2 x19_bit_1 x19_bit0 -x19_bit1 -x19_bit2 x19_bit3 -x19_bit4 x19_bit5 -x20_bit_7 x20_bit_6 -x20_bit_5 -x20_bit_4 -x20_bit_3 x20_bit_2 x20_bit_1 x20_bit0 x20_bit1 -x20_bit2 x20_bit3 -x20_bit4 -x20_bit5 -x21_bit_7 -x21_bit_6 -x21_bit_5 x21_bit_4 -x21_bit_3 x21_bit_2 x21_bit_1 -x21_bit0 x21_bit1 -x21_bit2 -x21_bit3 x21_bit4 -x21_bit5 x23_bit_7 -x23_bit_6 x23_bit_5 x23_bit_4 x23_bit_3 x23_bit_2 x23_bit_1 x23_bit0 x23_bit1 x23_bit2 -x23_bit3 -x23_bit4 x23_bit5 -x24_bit_7 -x24_bit_6 -x24_bit_5 x24_bit_4 -x24_bit_3 -x24_bit_2 x24_bit_1 x24_bit0 x24_bit1 -x24_bit2 -x24_bit3 -x24_bit4 -x24_bit5 x26_bit_7 -x26_bit_6 x26_bit_5 x26_bit_4 x26_bit_3 x26_bit_2 x26_bit_1 x26_bit0 -x26_bit1 -x26_bit2 x26_bit3 -x26_bit4 -x26_bit5 x33_bit_7 x33_bit_6 -x33_bit_5 -x33_bit_4 x33_bit_3 x33_bit_2 x33_bit_1 x33_bit0 x33_bit1 x33_bit2 -x33_bit3 x33_bit4 -x33_bit5 -x34_bit_7 x34_bit_6 x34_bit_5 x34_bit_4 x34_bit_3 -x34_bit_2 x34_bit_1 -x34_bit0 -x34_bit1 -x34_bit2 x34_bit3 -x34_bit4 -x34_bit5 x35_bit_7 -x35_bit_6 x35_bit_5 x35_bit_4 x35_bit_3 -x35_bit_2 -x35_bit_1 x35_bit0 x35_bit1 x35_bit2 x35_bit3 x35_bit4 -x35_bit5 -x36_bit_7 x36_bit_6 x36_bit_5 x36_bit_4 x36_bit_3 -x36_bit_2 x36_bit_1 -x36_bit0 x36_bit1 x36_bit2 -x36_bit3 -x36_bit4 x36_bit5 -x37_bit_7 -x37_bit_6 -x37_bit_5 x37_bit_4 x37_bit_3 x37_bit_2 -x37_bit_1 -x37_bit0 -x37_bit1 x37_bit2 -x37_bit3 x37_bit4 -x37_bit5 x38_bit_7 x38_bit_6 -x38_bit_5 -x38_bit_4 x38_bit_3 x38_bit_2 x38_bit_1 x38_bit0 -x38_bit1 x38_bit2 -x38_bit3 x38_bit4 x38_bit5 -x43_bit_7 -x43_bit_6 x43_bit_5 x43_bit_4 -x43_bit_3 -x43_bit_2 x43_bit_1 -x43_bit0 -x43_bit1 -x43_bit2 x43_bit3 -x43_bit4 x43_bit5 x45_bit_7 -x45_bit_6 -x45_bit_5 -x45_bit_4 -x45_bit_3 x45_bit_2 x45_bit_1 -x45_bit0 x45_bit1 -x45_bit2 x45_bit3 -x45_bit4 x45_bit5 x46_bit_7 -x46_bit_6 -x46_bit_5 -x46_bit_4 -x46_bit_3 x46_bit_2 x46_bit_1 -x46_bit0 -x46_bit1 x46_bit2 x46_bit3 -x46_bit4 -x46_bit5 -x48_bit_7 -x48_bit_6 x48_bit_5 x48_bit_4 -x48_bit_3 -x48_bit_2 x48_bit_1 x48_bit0 -x48_bit1 x48_bit2 -x48_bit3 -x48_bit4 -x48_bit5 -x49_bit_7 -x49_bit_6 x49_bit_5 x49_bit_4 -x49_bit_3 -x49_bit_2 x49_bit_1 x49_bit0 x49_bit1 -x49_bit2 -x49_bit3 -x49_bit4 x49_bit5 -x56_bit_7 -x56_bit_6 -x56_bit_5 -x56_bit_4 -x56_bit_3 -x56_bit_2 -x56_bit_1 -x56_bit0 x56_bit1 x56_bit2 -x56_bit3 x56_bit4 x56_bit5 -x58_bit_7 -x58_bit_6 -x58_bit_5 -x58_bit_4 -x58_bit_3 -x58_bit_2 -x58_bit_1 -x58_bit0 -x58_bit1 -x58_bit2 x58_bit3 x58_bit4 -x58_bit5 -x60_bit_7 -x60_bit_6 x60_bit_5 x60_bit_4 x60_bit_3 x60_bit_2 x60_bit_1 -x60_bit0 -x60_bit1 x60_bit2 -x60_bit3 x60_bit4 -x60_bit5 -x61_bit_7 -x61_bit_6 x61_bit_5 x61_bit_4 x61_bit_3 x61_bit_2 x61_bit_1 -x61_bit0 x61_bit1 -x61_bit2 -x61_bit3 x61_bit4 x61_bit5 -x69_bit_7 -x69_bit_6 -x69_bit_5 -x69_bit_4 x69_bit_3 -x69_bit_2 x69_bit_1 x69_bit0 -x69_bit1 -x69_bit2 -x69_bit3 x69_bit4 x69_bit5 x70_bit_7 -x70_bit_6 x70_bit_5 x70_bit_4 -x70_bit_3 x70_bit_2 x70_bit_1 x70_bit0 -x70_bit1 -x70_bit2 -x70_bit3 x70_bit4 -x70_bit5 -x73_bit_7 -x73_bit_6 -x73_bit_5 x73_bit_4 -x73_bit_3 -x73_bit_2 -x73_bit_1 -x73_bit0 -x73_bit1 -x73_bit2 -x73_bit3 x73_bit4 -x73_bit5 -x74_bit_7 x74_bit_6 x74_bit_5 -x74_bit_4 x74_bit_3 x74_bit_2 x74_bit_1 x74_bit0 x74_bit1 x74_bit2 -x74_bit3 x74_bit4 -x74_bit5 -x82_bit_7 x82_bit_6 -x82_bit_5 -x82_bit_4 -x82_bit_3 -x82_bit_2 x82_bit_1 x82_bit0 x82_bit1 -x82_bit2 -x82_bit3 x82_bit4 -x82_bit5 -x83_bit_7 -x83_bit_6 -x83_bit_5 -x83_bit_4 -x83_bit_3 x83_bit_2 -x83_bit_1 -x83_bit0 x83_bit1 -x83_bit2 x83_bit3 -x83_bit4 x83_bit5 -x84_bit_7 -x84_bit_6 x84_bit_5 -x84_bit_4 -x84_bit_3 -x84_bit_2 -x84_bit_1 -x84_bit0 -x84_bit1 -x84_bit2 -x84_bit3 -x84_bit4 x84_bit5 -x90_bit_7 -x90_bit_6 x90_bit_5 x90_bit_4 x90_bit_3 x90_bit_2 x90_bit_1 -x90_bit0 x90_bit1 x90_bit2 x90_bit3 -x90_bit4 x90_bit5 x95_bit_7 x95_bit_6 -x95_bit_5 x95_bit_4 x95_bit_3 x95_bit_2 -x95_bit_1 -x95_bit0 x95_bit1 x95_bit2 -x95_bit3 x95_bit4 -x95_bit5 -x96_bit_7 -x96_bit_6 -x96_bit_5 -x96_bit_4 x96_bit_3 x96_bit_2 -x96_bit_1 -x96_bit0 -x96_bit1 -x96_bit2 -x96_bit3 -x96_bit4 -x96_bit5 -x97_bit_7 x97_bit_6 -x97_bit_5 -x97_bit_4 -x97_bit_3 x97_bit_2 x97_bit_1 x97_bit0 x97_bit1 -x97_bit2 -x97_bit3 -x97_bit4 -x97_bit5 x98_bit_7 -x98_bit_6 -x98_bit_5 x98_bit_4 x98_bit_3 x98_bit_2 -x98_bit_1 -x98_bit0 x98_bit1 -x98_bit2 x98_bit3 -x98_bit4 x98_bit5 x99_bit_7 x99_bit_6 x99_bit_5 x99_bit_4 x99_bit_3 -x99_bit_2 x99_bit_1 -x99_bit0 x99_bit1 -x99_bit2 x99_bit3 -x99_bit4 -x99_bit5 x100_bit_7 x100_bit_6 x100_bit_5 x100_bit_4 x100_bit_3 -x100_bit_2 x100_bit_1 -x100_bit0 -x100_bit1 -x100_bit2 x100_bit3 -x100_bit4 x100_bit5 -x101_bit_7 -x101_bit_6 x101_bit_5 -x101_bit_4 x101_bit_3 x101_bit_2 x101_bit_1 -x101_bit0 x101_bit1 x101_bit2 x101_bit3 -x101_bit4 -x101_bit5 -x102_bit_7 x102_bit_6 x102_bit_5 x102_bit_4 x102_bit_3 -x102_bit_2 -x102_bit_1 x102_bit0 x102_bit1 -x102_bit2 -x102_bit3 -x102_bit4 -x102_bit5 -x105_bit_7 x105_bit_6 -x105_bit_5 -x105_bit_4 -x105_bit_3 -x105_bit_2 x105_bit_1 x105_bit0 -x105_bit1 -x105_bit2 x105_bit3 -x105_bit4 -x105_bit5 -x106_bit_7 -x106_bit_6 x106_bit_5 -x106_bit_4 -x106_bit_3 x106_bit_2 x106_bit_1 -x106_bit0 x106_bit1 x106_bit2 x106_bit3 -x106_bit4 x106_bit5 -x109_bit_7 x109_bit_6 -x109_bit_5 -x109_bit_4 -x109_bit_3 -x109_bit_2 -x109_bit_1 -x109_bit0 -x109_bit1 -x109_bit2 x109_bit3 -x109_bit4 x109_bit5 -x114_bit_7 x114_bit_6 x114_bit_5 x114_bit_4 x114_bit_3 x114_bit_2 x114_bit_1 x114_bit0 x114_bit1 -x114_bit2 x114_bit3 -x114_bit4 x114_bit5 -x116_bit_7 -x116_bit_6 -x116_bit_5 -x116_bit_4 x116_bit_3 -x116_bit_2 -x116_bit_1 -x116_bit0 x116_bit1 -x116_bit2 x116_bit3 x116_bit4 -x116_bit5 -x117_bit_7 x117_bit_6 x117_bit_5 x117_bit_4 x117_bit_3 -x117_bit_2 x117_bit_1 x117_bit0 x117_bit1 -x117_bit2 -x117_bit3 x117_bit4 -x117_bit5 x120_bit_7 x120_bit_6 -x120_bit_5 x120_bit_4 x120_bit_3 -x120_bit_2 x120_bit_1 x120_bit0 -x120_bit1 -x120_bit2 -x120_bit3 -x120_bit4 x120_bit5 -x121_bit_7 -x121_bit_6 -x121_bit_5 x121_bit_4 -x121_bit_3 x121_bit_2 -x121_bit_1 x121_bit0 -x121_bit1 -x121_bit2 x121_bit3 -x121_bit4 x121_bit5 x122_bit_7 x122_bit_6 x122_bit_5 x122_bit_4 x122_bit_3 x122_bit_2 x122_bit_1 x122_bit0 x122_bit1 -x122_bit2 x122_bit3 x122_bit4 -x122_bit5 x125_bit_7 -x125_bit_6 -x125_bit_5 -x125_bit_4 -x125_bit_3 -x125_bit_2 -x125_bit_1 x125_bit0 x125_bit1 -x125_bit2 -x125_bit3 x125_bit4 -x125_bit5 x128_bit_7 -x128_bit_6 -x128_bit_5 -x128_bit_4 -x128_bit_3 x128_bit_2 -x128_bit_1 x128_bit0 x128_bit1 x128_bit2 x128_bit3 -x128_bit4 -x128_bit5 x133_bit_7 x133_bit_6 x133_bit_5 -x133_bit_4 x133_bit_3 x133_bit_2 -x133_bit_1 x133_bit0 -x133_bit1 x133_bit2 -x133_bit3 -x133_bit4 x133_bit5 -x135_bit_7 -x135_bit_6 -x135_bit_5 -x135_bit_4 -x135_bit_3 x135_bit_2 x135_bit_1 -x135_bit0 x135_bit1 -x135_bit2 -x135_bit3 -x135_bit4 -x135_bit5 -x139_bit_7 x139_bit_6 x139_bit_5 x139_bit_4 -x139_bit_3 -x139_bit_2 x139_bit_1 -x139_bit0 x139_bit1 -x139_bit2 -x139_bit3 x139_bit4 x139_bit5 -x143_bit_7 -x143_bit_6 -x143_bit_5 x143_bit_4 x143_bit_3 x143_bit_2 x143_bit_1 -x143_bit0 x143_bit1 x143_bit2 -x143_bit3 x143_bit4 x143_bit5 -x148_bit_7 -x148_bit_6 x148_bit_5 -x148_bit_4 x148_bit_3 x148_bit_2 -x148_bit_1 x148_bit0 x148_bit1 -x148_bit2 x148_bit3 -x148_bit4 -x148_bit5 x149_bit_7 -x149_bit_6 -x149_bit_5 x149_bit_4 -x149_bit_3 x149_bit_2 x149_bit_1 x149_bit0 x149_bit1 x149_bit2 x149_bit3 -x149_bit4 x149_bit5 -x150_bit_7 -x150_bit_6 x150_bit_5 -x150_bit_4 -x150_bit_3 x150_bit_2 -x150_bit_1 -x150_bit0 -x150_bit1 x150_bit2 -x150_bit3 x150_bit4 -x150_bit5 x151_bit_7 x151_bit_6 x151_bit_5 x151_bit_4 -x151_bit_3 -x151_bit_2 -x151_bit_1 -x151_bit0 -x151_bit1 -x151_bit2 -x151_bit3 x151_bit4 -x151_bit5 -x156_bit_7 -x156_bit_6 -x156_bit_5 -x156_bit_4 -x156_bit_3 x156_bit_2 x156_bit_1 -x156_bit0 -x156_bit1 -x156_bit2 -x156_bit3 x156_bit4 -x156_bit5 x160_bit_7 -x160_bit_6 x160_bit_5 x160_bit_4 x160_bit_3 -x160_bit_2 -x160_bit_1 x160_bit0 -x160_bit1 -x160_bit2 x160_bit3 -x160_bit4 x160_bit5 x161_bit_7 -x161_bit_6 x161_bit_5 x161_bit_4 x161_bit_3 -x161_bit_2 -x161_bit_1 x161_bit0 -x161_bit1 x161_bit2 -x161_bit3 -x161_bit4 -x161_bit5 -x164_bit_7 -x164_bit_6 -x164_bit_5 -x164_bit_4 -x164_bit_3 x164_bit_2 x164_bit_1 -x164_bit0 x164_bit1 -x164_bit2 -x164_bit3 -x164_bit4 -x164_bit5 x166_bit_7 -x166_bit_6 x166_bit_5 x166_bit_4 x166_bit_3 x166_bit_2 -x166_bit_1 x166_bit0 -x166_bit1 -x166_bit2 x166_bit3 x166_bit4 x166_bit5 -x168_bit_7 -x168_bit_6 -x168_bit_5 -x168_bit_4 -x168_bit_3 -x168_bit_2 -x168_bit_1 x168_bit0 -x168_bit1 -x168_bit2 -x168_bit3 -x168_bit4 x168_bit5 x169_bit_7 x169_bit_6 x169_bit_5 x169_bit_4 x169_bit_3 -x169_bit_2 -x169_bit_1 -x169_bit0 -x169_bit1 x169_bit2 -x169_bit3 x169_bit4 x169_bit5 x171_bit_7 x171_bit_6 x171_bit_5 x171_bit_4 x171_bit_3 -x171_bit_2 -x171_bit_1 -x171_bit0 x171_bit1 x171_bit2 -x171_bit3 x171_bit4 -x171_bit5 -x175_bit_7 -x175_bit_6 -x175_bit_5 -x175_bit_4 x175_bit_3 -x175_bit_2 x175_bit_1 x175_bit0 x175_bit1 x175_bit2 x175_bit3 -x175_bit4 x175_bit5 -x178_bit_7 -x178_bit_6 -x178_bit_5 -x178_bit_4 x178_bit_3 -x178_bit_2 x178_bit_1 x178_bit0 -x178_bit1 -x178_bit2 -x178_bit3 x178_bit4 -x178_bit5 -x181_bit_7 -x181_bit_6 x181_bit_5 -x181_bit_4 x181_bit_3 x181_bit_2 -x181_bit_1 x181_bit0 -x181_bit1 x181_bit2 -x181_bit3 x181_bit4 x181_bit5 x182_bit_7 -x182_bit_6 x182_bit_5 -x182_bit_4 -x182_bit_3 -x182_bit_2 -x182_bit_1 x182_bit0 -x182_bit1 x182_bit2 -x182_bit3 -x182_bit4 x182_bit5 x183_bit_7 -x183_bit_6 x183_bit_5 -x183_bit_4 x183_bit_3 -x183_bit_2 x183_bit_1 -x183_bit0 x183_bit1 x183_bit2 -x183_bit3 -x183_bit4 -x183_bit5 x185_bit_7 x185_bit_6 x185_bit_5 x185_bit_4 -x185_bit_3 x185_bit_2 -x185_bit_1 x185_bit0 x185_bit1 x185_bit2 x185_bit3 -x185_bit4 -x185_bit5 x186_bit_7 x186_bit_6 x186_bit_5 x186_bit_4 x186_bit_3 -x186_bit_2 x186_bit_1 x186_bit0 -x186_bit1 x186_bit2 x186_bit3 -x186_bit4 x186_bit5 -x189_bit_7 -x189_bit_6 -x189_bit_5 -x189_bit_4 x189_bit_3 x189_bit_2 -x189_bit_1 x189_bit0 -x189_bit1 x189_bit2 x189_bit3 x189_bit4 -x189_bit5 x195_bit_7 x195_bit_6 x195_bit_5 x195_bit_4 -x195_bit_3 x195_bit_2 x195_bit_1 -x195_bit0 -x195_bit1 -x195_bit2 x195_bit3 -x195_bit4 x195_bit5 x199_bit_7 -x199_bit_6 x199_bit_5 x199_bit_4 x199_bit_3 x199_bit_2 -x199_bit_1 x199_bit0 -x199_bit1 -x199_bit2 -x199_bit3 -x199_bit4 x199_bit5 x200_bit_7 x200_bit_6 -x200_bit_5 -x200_bit_4 -x200_bit_3 x200_bit_2 x200_bit_1 -x200_bit0 -x200_bit1 x200_bit2 x200_bit3 x200_bit4 -x200_bit5 x201_bit_7 -x201_bit_6 x201_bit_5 -x201_bit_4 x201_bit_3 x201_bit_2 x201_bit_1 -x201_bit0 -x201_bit1 x201_bit2 -x201_bit3 -x201_bit4 x201_bit5 x202_bit_7 x202_bit_6 -x202_bit_5 -x202_bit_4 -x202_bit_3 x202_bit_2 x202_bit_1 -x202_bit0 -x202_bit1 x202_bit2 x202_bit3 -x202_bit4 x202_bit5 -x204_bit_7 -x204_bit_6 -x204_bit_5 x204_bit_4 x204_bit_3 -x204_bit_2 x204_bit_1 -x204_bit0 -x204_bit1 -x204_bit2 x204_bit3 -x204_bit4 -x204_bit5 -x205_bit_7 x205_bit_6 x205_bit_5 -x205_bit_4 -x205_bit_3 -x205_bit_2 x205_bit_1 -x205_bit0 -x205_bit1 -x205_bit2 -x205_bit3 x205_bit4 -x205_bit5 x208_bit_7 -x208_bit_6 -x208_bit_5 -x208_bit_4 -x208_bit_3 -x208_bit_2 x208_bit_1 -x208_bit0 -x208_bit1 x208_bit2 -x208_bit3 -x208_bit4 -x208_bit5 x209_bit_7 -x209_bit_6 -x209_bit_5 -x209_bit_4 -x209_bit_3 -x209_bit_2 x209_bit_1 -x209_bit0 x209_bit1 -x209_bit2 -x209_bit3 -x209_bit4 x209_bit5 -x210_bit_7 -x210_bit_6 -x210_bit_5 -x210_bit_4 x210_bit_3 x210_bit_2 x210_bit_1 x210_bit0 -x210_bit1 x210_bit2 -x210_bit3 -x210_bit4 -x210_bit5 x211_bit_7 x211_bit_6 -x211_bit_5 x211_bit_4 x211_bit_3 x211_bit_2 -x211_bit_1 x211_bit0 -x211_bit1 x211_bit2 x211_bit3 x211_bit4 -x211_bit5 x215_bit_7 -x215_bit_6 x215_bit_5 -x215_bit_4 x215_bit_3 x215_bit_2 -x215_bit_1 x215_bit0 -x215_bit1 -x215_bit2 -x215_bit3 -x215_bit4 x215_bit5 -x218_bit_7 x218_bit_6 -x218_bit_5 x218_bit_4 -x218_bit_3 -x218_bit_2 x218_bit_1 x218_bit0 -x218_bit1 -x218_bit2 -x218_bit3 -x218_bit4 x218_bit5 x219_bit_7 x219_bit_6 -x219_bit_5 -x219_bit_4 x219_bit_3 x219_bit_2 -x219_bit_1 x219_bit0 -x219_bit1 -x219_bit2 -x219_bit3 x219_bit4 x219_bit5 x220_bit_7 x220_bit_6 -x220_bit_5 -x220_bit_4 x220_bit_3 x220_bit_2 -x220_bit_1 x220_bit0 x220_bit1 -x220_bit2 -x220_bit3 x220_bit4 -x220_bit5 -x221_bit_7 -x221_bit_6 x221_bit_5 -x221_bit_4 -x221_bit_3 x221_bit_2 x221_bit_1 x221_bit0 x221_bit1 -x221_bit2 x221_bit3 -x221_bit4 x221_bit5 x223_bit_7 -x223_bit_6 -x223_bit_5 -x223_bit_4 -x223_bit_3 -x223_bit_2 x223_bit_1 -x223_bit0 x223_bit1 x223_bit2 -x223_bit3 -x223_bit4 -x223_bit5 x224_bit_7 -x224_bit_6 -x224_bit_5 -x224_bit_4 -x224_bit_3 -x224_bit_2 x224_bit_1 x224_bit0 x224_bit1 -x224_bit2 -x224_bit3 x224_bit4 x224_bit5 x225_bit_7 -x225_bit_6 x225_bit_5 -x225_bit_4 -x225_bit_3 x225_bit_2 -x225_bit_1 -x225_bit0 -x225_bit1 -x225_bit2 x225_bit3 -x225_bit4 x225_bit5 -x227_bit0 x227_bit1 -x227_bit2 x229_bit0 -x229_bit1 -x230_bit0 -x231_bit0 x232_bit0 -x232_bit1 x233_bit0 -x233_bit1 x235_bit0 -x235_bit1 x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 x244_bit0 x245_bit0 x246_bit0 x247_bit0 x249_bit0 x250_bit0 -x251_bit0 x251_bit1 -x252_bit0 x252_bit1 -x252_bit2 x255_bit0 x256_bit0 -x256_bit1 x257_bit0 -x257_bit1 -x257_bit2 -x258_bit0 -x258_bit1 x259_bit0 -x259_bit1 -x260_bit0 -x262_bit0 x263_bit0 x265_bit0 x266_bit0 -x267_bit0 x268_bit0 x269_bit0 x271_bit0 -x272_bit0 -x273_bit0 x273_bit1 -x273_bit2 x274_bit0 -x274_bit1 x275_bit0 -x275_bit1 -x276_bit0 x276_bit1 -x276_bit2 x277_bit0 -x277_bit1 x278_bit0 -x278_bit1 -x279_bit0 x279_bit1 -x279_bit2 -x280_bit0 x280_bit1 -x280_bit2 -x281_bit0 x281_bit1 -x281_bit2 x282_bit0 -x282_bit1 -x283_bit0 x283_bit1 -x284_bit0 x284_bit1 x285_bit0 x286_bit0 -x286_bit1 -x287_bit0 x287_bit1 -x287_bit2 -x288_bit0 x288_bit1 -x288_bit2 -x289_bit0 x289_bit1 -x289_bit2 x290_bit0 -x290_bit1 x291_bit0 -x291_bit1 x292_bit0 -x292_bit1 -x293_bit0 x293_bit1 x294_bit0 -x294_bit1 x295_bit0 -x295_bit1 -x295_bit2 -x296_bit0 x296_bit1 -x297_bit0 x297_bit1 -x298_bit0 x298_bit1 x299_bit0 -x299_bit1 x300_bit0 -x300_bit1 -x301_bit0 x301_bit1 x302_bit0 x303_bit0 x304_bit0 x305_bit0 -x305_bit1 -x306_bit0 x306_bit1 -x307_bit0 -x308_bit0 -x309_bit0 x309_bit1 -x309_bit2 x310_bit0 -x310_bit1 x311_bit0 -x313_bit0 x313_bit1 x314_bit0 x315_bit0 -x315_bit1 x316_bit0 x317_bit0 -x317_bit1 -x318_bit0 x318_bit1 -x319_bit0 -x320_bit0 x321_bit0 -x322_bit0 -x322_bit1 x323_bit0 -x323_bit1 -x324_bit0 x324_bit1 -x325_bit0 x325_bit1 -x325_bit2 -x326_bit0 x326_bit1 -x326_bit2 -x327_bit0 -x328_bit0 x328_bit1 -x328_bit2 -x329_bit0 x329_bit1 -x330_bit0 x330_bit1 x331_bit0 -x332_bit0 x332_bit1 -x333_bit0 -x335_bit0 x336_bit0 -x336_bit1 -x337_bit0 x337_bit1 x338_bit0 -x338_bit1 x339_bit0 -x339_bit1 x340_bit0 x341_bit0 -x341_bit1 -x342_bit0 x342_bit1 -x343_bit0 x344_bit0 -x344_bit1 x345_bit0 -x345_bit1 -x346_bit0 x347_bit0 -x347_bit1 -x348_bit0 -x348_bit1 -x349_bit0 x349_bit1 x350_bit0 x350_bit1 -x351_bit0 x351_bit1 -x351_bit2 -x352_bit0 -x353_bit0 x353_bit1 -x354_bit0 x355_bit0 -x355_bit1 x356_bit0 -x356_bit1 x357_bit0 x358_bit0 -x358_bit1 -x359_bit0 x360_bit0 -x360_bit1 x361_bit0 x362_bit0 -x363_bit0 x364_bit0 -x364_bit1 -x365_bit0 x366_bit0 -x366_bit1 -x367_bit0 -x369_bit0 x369_bit1 -x370_bit0 x371_bit0 -x371_bit1 x372_bit0 -x372_bit1 -x373_bit0 x373_bit1 x374_bit0 x375_bit0 -x375_bit1 x376_bit0 -x376_bit1 -x376_bit2 x377_bit0 -x377_bit1 -x378_bit0 x380_bit0 -x380_bit1 x381_bit0 -x382_bit0 x383_bit0 -x383_bit1 x385_bit0 x386_bit0 -x386_bit1 x387_bit0 x388_bit0 -x388_bit1 -x389_bit0 x390_bit0 -x390_bit1 -x391

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/16323/stat): 16323 (minisat+_script) R 16322 16323 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855498759 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/16323/statm): 174 3 169 147 0 27 0
[pid=16323] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=16324
New process pid=16325
New process pid=16326
execve syscall for /bin/sed executable
One traced child (pid=16325) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=16326) exited with status: 0
One traced child (pid=16324) exited with status: 0
New process pid=16327
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-timtab1.opb
One traced child (pid=16327) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=16328
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-timtab1.opb

[startup+10.0041 s]
Raw data (loadavg): 0.89 0.95 0.90 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7376 0 0 0 934 32 0 0 25 0 1 0 1855498766 32935936 6996 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 8041 6996 162 162 0 7879 0
[pid=16328] vsize: 32164
Current children cumulated CPU time (s) 9.67
Current children cumulated vsize (Kb) 34292

[startup+20.0048 s]
Raw data (loadavg): 0.90 0.96 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7450 0 0 0 1932 32 0 0 25 0 1 0 1855498766 33226752 7070 4294967295 134512640 135167914 3221224448 3221223148 134562911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8112 7070 162 162 0 7950 0
[pid=16328] vsize: 32448
Current children cumulated CPU time (s) 19.65
Current children cumulated vsize (Kb) 34576

[startup+30.0055 s]
Raw data (loadavg): 0.92 0.96 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7598 0 0 0 2930 33 0 0 25 0 1 0 1855498766 33820672 7218 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 8257 7218 162 162 0 8095 0
[pid=16328] vsize: 33028
Current children cumulated CPU time (s) 29.64
Current children cumulated vsize (Kb) 35156

[startup+40.0062 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7687 0 0 0 3928 34 0 0 25 0 1 0 1855498766 34144256 7307 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8336 7307 162 162 0 8174 0
[pid=16328] vsize: 33344
Current children cumulated CPU time (s) 39.63
Current children cumulated vsize (Kb) 35472

[startup+50.0069 s]
Raw data (loadavg): 0.94 0.96 0.91 1/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) T 16323 16323 21452 0 -1 0 7759 0 0 0 4925 34 0 0 25 0 1 0 1855498766 34488320 7379 4294967295 134512640 135167914 3221224448 3221223192 134865917 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8420 7379 162 162 0 8258 0
[pid=16328] vsize: 33680
Current children cumulated CPU time (s) 49.6
Current children cumulated vsize (Kb) 35808

[startup+60.4395 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7781 0 0 0 5924 35 0 0 25 0 1 0 1855498766 34553856 7401 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8436 7401 162 162 0 8274 0
[pid=16328] vsize: 33744
Current children cumulated CPU time (s) 59.6
Current children cumulated vsize (Kb) 35872

[startup+70.4402 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7822 0 0 0 6924 35 0 0 25 0 1 0 1855498766 34709504 7442 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8474 7442 162 162 0 8312 0
[pid=16328] vsize: 33896
Current children cumulated CPU time (s) 69.6
Current children cumulated vsize (Kb) 36024

[startup+80.4409 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7860 0 0 0 7923 35 0 0 25 0 1 0 1855498766 34856960 7480 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8510 7480 162 162 0 8348 0
[pid=16328] vsize: 34040
Current children cumulated CPU time (s) 79.59
Current children cumulated vsize (Kb) 36168

[startup+90.4416 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7936 0 0 0 8923 36 0 0 25 0 1 0 1855498766 35127296 7556 4294967295 134512640 135167914 3221224448 3221223168 134560222 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8576 7556 162 162 0 8414 0
[pid=16328] vsize: 34304
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 36432

[startup+100.442 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 7973 0 0 0 9922 36 0 0 25 0 1 0 1855498766 35270656 7593 4294967295 134512640 135167914 3221224448 3221223108 134567722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8611 7593 162 162 0 8449 0
[pid=16328] vsize: 34444
Current children cumulated CPU time (s) 99.59
Current children cumulated vsize (Kb) 36572

[startup+110.443 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8109 0 0 0 10920 37 0 0 25 0 1 0 1855498766 35946496 7729 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8776 7729 162 162 0 8614 0
[pid=16328] vsize: 35104
Current children cumulated CPU time (s) 109.58
Current children cumulated vsize (Kb) 37232

[startup+120.444 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8219 0 0 0 11919 38 0 0 25 0 1 0 1855498766 36380672 7839 4294967295 134512640 135167914 3221224448 3221223156 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8882 7839 162 162 0 8720 0
[pid=16328] vsize: 35528
Current children cumulated CPU time (s) 119.58
Current children cumulated vsize (Kb) 37656

[startup+130.444 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8256 0 0 0 12918 39 0 0 25 0 1 0 1855498766 36528128 7876 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8918 7876 162 162 0 8756 0
[pid=16328] vsize: 35672
Current children cumulated CPU time (s) 129.58
Current children cumulated vsize (Kb) 37800

[startup+140.444 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8337 0 0 0 13917 39 0 0 25 0 1 0 1855498766 36823040 7957 4294967295 134512640 135167914 3221224448 3221223152 134562628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 8990 7957 162 162 0 8828 0
[pid=16328] vsize: 35960
Current children cumulated CPU time (s) 139.57
Current children cumulated vsize (Kb) 38088

[startup+150.446 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8389 0 0 0 14916 40 0 0 25 0 1 0 1855498766 37031936 8009 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9041 8009 162 162 0 8879 0
[pid=16328] vsize: 36164
Current children cumulated CPU time (s) 149.57
Current children cumulated vsize (Kb) 38292

[startup+160.447 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8438 0 0 0 15915 40 0 0 25 0 1 0 1855498766 37220352 8058 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9087 8058 162 162 0 8925 0
[pid=16328] vsize: 36348
Current children cumulated CPU time (s) 159.56
Current children cumulated vsize (Kb) 38476

[startup+170.446 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8516 0 0 0 16914 41 0 0 25 0 1 0 1855498766 37531648 8136 4294967295 134512640 135167914 3221224448 3221223232 134564290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9163 8136 162 162 0 9001 0
[pid=16328] vsize: 36652
Current children cumulated CPU time (s) 169.56
Current children cumulated vsize (Kb) 38780

[startup+180.447 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) T 16323 16323 21452 0 -1 0 8561 0 0 0 17945 41 0 0 25 0 1 0 1855498766 37707776 8181 4294967295 134512640 135167914 3221224448 3221222844 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9206 8181 162 162 0 9044 0
[pid=16328] vsize: 36824
Current children cumulated CPU time (s) 179.87
Current children cumulated vsize (Kb) 38952

[startup+190.865 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8612 0 0 0 18944 42 0 0 25 0 1 0 1855498766 37908480 8232 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9255 8232 162 162 0 9093 0
[pid=16328] vsize: 37020
Current children cumulated CPU time (s) 189.87
Current children cumulated vsize (Kb) 39148

[startup+200.865 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8648 0 0 0 19944 42 0 0 25 0 1 0 1855498766 38047744 8268 4294967295 134512640 135167914 3221224448 3221223152 134562910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9289 8268 162 162 0 9127 0
[pid=16328] vsize: 37156
Current children cumulated CPU time (s) 199.87
Current children cumulated vsize (Kb) 39284

[startup+210.866 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8699 0 0 0 20943 42 0 0 25 0 1 0 1855498766 38244352 8319 4294967295 134512640 135167914 3221224448 3221223108 134567711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9337 8319 162 162 0 9175 0
[pid=16328] vsize: 37348
Current children cumulated CPU time (s) 209.86
Current children cumulated vsize (Kb) 39476

[startup+220.867 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8773 0 0 0 21942 43 0 0 25 0 1 0 1855498766 38539264 8393 4294967295 134512640 135167914 3221224448 3221223108 134567702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9409 8393 162 162 0 9247 0
[pid=16328] vsize: 37636
Current children cumulated CPU time (s) 219.86
Current children cumulated vsize (Kb) 39764

[startup+230.867 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8822 0 0 0 22941 43 0 0 25 0 1 0 1855498766 38989824 8442 4294967295 134512640 135167914 3221224448 3221223152 134562647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9519 8442 162 162 0 9357 0
[pid=16328] vsize: 38076
Current children cumulated CPU time (s) 229.85
Current children cumulated vsize (Kb) 40204

[startup+240.868 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8873 0 0 0 23940 43 0 0 25 0 1 0 1855498766 39194624 8493 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9569 8493 162 162 0 9407 0
[pid=16328] vsize: 38276
Current children cumulated CPU time (s) 239.84
Current children cumulated vsize (Kb) 40404

[startup+250.87 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8914 0 0 0 24940 43 0 0 25 0 1 0 1855498766 39350272 8534 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9607 8534 162 162 0 9445 0
[pid=16328] vsize: 38428
Current children cumulated CPU time (s) 249.84
Current children cumulated vsize (Kb) 40556

[startup+260.871 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 8964 0 0 0 25939 44 0 0 25 0 1 0 1855498766 39546880 8584 4294967295 134512640 135167914 3221224448 3221223156 134558173 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9655 8584 162 162 0 9493 0
[pid=16328] vsize: 38620
Current children cumulated CPU time (s) 259.84
Current children cumulated vsize (Kb) 40748

[startup+270.871 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9019 0 0 0 26939 44 0 0 25 0 1 0 1855498766 39763968 8639 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9708 8639 162 162 0 9546 0
[pid=16328] vsize: 38832
Current children cumulated CPU time (s) 269.84
Current children cumulated vsize (Kb) 40960

[startup+280.872 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9097 0 0 0 27938 45 0 0 25 0 1 0 1855498766 40071168 8717 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9783 8717 162 162 0 9621 0
[pid=16328] vsize: 39132
Current children cumulated CPU time (s) 279.84
Current children cumulated vsize (Kb) 41260

[startup+290.873 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9163 0 0 0 28937 45 0 0 25 0 1 0 1855498766 40333312 8783 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9847 8783 162 162 0 9685 0
[pid=16328] vsize: 39388
Current children cumulated CPU time (s) 289.83
Current children cumulated vsize (Kb) 41516

[startup+300.873 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9311 0 0 0 29934 47 0 0 25 0 1 0 1855498766 40923136 8931 4294967295 134512640 135167914 3221224448 3221223156 134558171 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 9991 8931 162 162 0 9829 0
[pid=16328] vsize: 39964
Current children cumulated CPU time (s) 299.82
Current children cumulated vsize (Kb) 42092

[startup+310.874 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9368 0 0 0 30933 47 0 0 25 0 1 0 1855498766 41148416 8988 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10046 8988 162 162 0 9884 0
[pid=16328] vsize: 40184
Current children cumulated CPU time (s) 309.81
Current children cumulated vsize (Kb) 42312

[startup+320.875 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9410 0 0 0 31931 48 0 0 25 0 1 0 1855498766 41312256 9030 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10086 9030 162 162 0 9924 0
[pid=16328] vsize: 40344
Current children cumulated CPU time (s) 319.8
Current children cumulated vsize (Kb) 42472

[startup+330.877 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9452 0 0 0 32930 48 0 0 25 0 1 0 1855498766 41480192 9072 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10127 9072 162 162 0 9965 0
[pid=16328] vsize: 40508
Current children cumulated CPU time (s) 329.79
Current children cumulated vsize (Kb) 42636

[startup+340.877 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9507 0 0 0 33929 49 0 0 25 0 1 0 1855498766 41697280 9127 4294967295 134512640 135167914 3221224448 3221223136 134562920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10180 9127 162 162 0 10018 0
[pid=16328] vsize: 40720
Current children cumulated CPU time (s) 339.79
Current children cumulated vsize (Kb) 42848

[startup+350.878 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9594 0 0 0 34928 49 0 0 25 0 1 0 1855498766 42020864 9214 4294967295 134512640 135167914 3221224448 3221223088 134561392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10259 9214 162 162 0 10097 0
[pid=16328] vsize: 41036
Current children cumulated CPU time (s) 349.78
Current children cumulated vsize (Kb) 43164

[startup+360.879 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9649 0 0 0 35927 50 0 0 25 0 1 0 1855498766 42233856 9269 4294967295 134512640 135167914 3221224448 3221223120 134566760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10311 9269 162 162 0 10149 0
[pid=16328] vsize: 41244
Current children cumulated CPU time (s) 359.78
Current children cumulated vsize (Kb) 43372

[startup+370.879 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9715 0 0 0 36926 50 0 0 25 0 1 0 1855498766 42496000 9335 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10375 9335 162 162 0 10213 0
[pid=16328] vsize: 41500
Current children cumulated CPU time (s) 369.77
Current children cumulated vsize (Kb) 43628

[startup+380.88 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9766 0 0 0 37925 51 0 0 25 0 1 0 1855498766 42696704 9386 4294967295 134512640 135167914 3221224448 3221223156 134558138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10424 9386 162 162 0 10262 0
[pid=16328] vsize: 41696
Current children cumulated CPU time (s) 379.77
Current children cumulated vsize (Kb) 43824

[startup+390.881 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9825 0 0 0 38924 51 0 0 25 0 1 0 1855498766 42926080 9445 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10480 9445 162 162 0 10318 0
[pid=16328] vsize: 41920
Current children cumulated CPU time (s) 389.76
Current children cumulated vsize (Kb) 44048

[startup+400.883 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9888 0 0 0 39923 52 0 0 25 0 1 0 1855498766 43175936 9508 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10541 9508 162 162 0 10379 0
[pid=16328] vsize: 42164
Current children cumulated CPU time (s) 399.76
Current children cumulated vsize (Kb) 44292

[startup+410.883 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 9956 0 0 0 40922 53 0 0 25 0 1 0 1855498766 43442176 9576 4294967295 134512640 135167914 3221224448 3221223188 134563640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10606 9576 162 162 0 10444 0
[pid=16328] vsize: 42424
Current children cumulated CPU time (s) 409.76
Current children cumulated vsize (Kb) 44552

[startup+420.884 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10016 0 0 0 41921 53 0 0 25 0 1 0 1855498766 43679744 9636 4294967295 134512640 135167914 3221224448 3221223184 134559449 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10664 9636 162 162 0 10502 0
[pid=16328] vsize: 42656
Current children cumulated CPU time (s) 419.75
Current children cumulated vsize (Kb) 44784

[startup+430.885 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10093 0 0 0 42920 54 0 0 25 0 1 0 1855498766 43982848 9713 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10738 9713 162 162 0 10576 0
[pid=16328] vsize: 42952
Current children cumulated CPU time (s) 429.75
Current children cumulated vsize (Kb) 45080

[startup+440.885 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10124 0 0 0 43919 54 0 0 25 0 1 0 1855498766 44097536 9744 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10766 9744 162 162 0 10604 0
[pid=16328] vsize: 43064
Current children cumulated CPU time (s) 439.74
Current children cumulated vsize (Kb) 45192

[startup+450.887 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10170 0 0 0 44919 54 0 0 25 0 1 0 1855498766 44277760 9790 4294967295 134512640 135167914 3221224448 3221223152 134562660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10810 9790 162 162 0 10648 0
[pid=16328] vsize: 43240
Current children cumulated CPU time (s) 449.74
Current children cumulated vsize (Kb) 45368

[startup+460.888 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10224 0 0 0 45919 54 0 0 25 0 1 0 1855498766 44490752 9844 4294967295 134512640 135167914 3221224448 3221223152 134562552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10862 9844 162 162 0 10700 0
[pid=16328] vsize: 43448
Current children cumulated CPU time (s) 459.74
Current children cumulated vsize (Kb) 45576

[startup+470.889 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10271 0 0 0 46918 55 0 0 25 0 1 0 1855498766 44679168 9891 4294967295 134512640 135167914 3221224448 3221223152 134562815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10908 9891 162 162 0 10746 0
[pid=16328] vsize: 43632
Current children cumulated CPU time (s) 469.74
Current children cumulated vsize (Kb) 45760

[startup+480.889 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10317 0 0 0 47917 55 0 0 25 0 1 0 1855498766 44859392 9937 4294967295 134512640 135167914 3221224448 3221223108 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 10952 9937 162 162 0 10790 0
[pid=16328] vsize: 43808
Current children cumulated CPU time (s) 479.73
Current children cumulated vsize (Kb) 45936

[startup+490.89 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10438 0 0 0 48916 55 0 0 25 0 1 0 1855498766 45338624 10058 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11069 10058 162 162 0 10907 0
[pid=16328] vsize: 44276
Current children cumulated CPU time (s) 489.72
Current children cumulated vsize (Kb) 46404

[startup+500.892 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10534 0 0 0 49914 56 0 0 25 0 1 0 1855498766 45719552 10154 4294967295 134512640 135167914 3221224448 3221223152 134562940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11162 10154 162 162 0 11000 0
[pid=16328] vsize: 44648
Current children cumulated CPU time (s) 499.71
Current children cumulated vsize (Kb) 46776

[startup+510.892 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10611 0 0 0 50913 57 0 0 25 0 1 0 1855498766 46026752 10231 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 11237 10231 162 162 0 11075 0
[pid=16328] vsize: 44948
Current children cumulated CPU time (s) 509.71
Current children cumulated vsize (Kb) 47076

[startup+520.893 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10673 0 0 0 51911 57 0 0 25 0 1 0 1855498766 46796800 10293 4294967295 134512640 135167914 3221224448 3221223108 134567705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11425 10293 162 162 0 11263 0
[pid=16328] vsize: 45700
Current children cumulated CPU time (s) 519.69
Current children cumulated vsize (Kb) 47828

[startup+530.895 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10718 0 0 0 52911 58 0 0 25 0 1 0 1855498766 46972928 10338 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11468 10338 162 162 0 11306 0
[pid=16328] vsize: 45872
Current children cumulated CPU time (s) 529.7
Current children cumulated vsize (Kb) 48000

[startup+540.896 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10766 0 0 0 53910 59 0 0 25 0 1 0 1855498766 47165440 10386 4294967295 134512640 135167914 3221224448 3221223152 134562837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11515 10386 162 162 0 11353 0
[pid=16328] vsize: 46060
Current children cumulated CPU time (s) 539.7
Current children cumulated vsize (Kb) 48188

[startup+550.896 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10812 0 0 0 54910 59 0 0 25 0 1 0 1855498766 47345664 10432 4294967295 134512640 135167914 3221224448 3221223108 134567702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11559 10432 162 162 0 11397 0
[pid=16328] vsize: 46236
Current children cumulated CPU time (s) 549.7
Current children cumulated vsize (Kb) 48364

[startup+560.897 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10912 0 0 0 55908 60 0 0 25 0 1 0 1855498766 47742976 10532 4294967295 134512640 135167914 3221224448 3221223152 134562528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11656 10532 162 162 0 11494 0
[pid=16328] vsize: 46624
Current children cumulated CPU time (s) 559.69
Current children cumulated vsize (Kb) 48752

[startup+570.898 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 10973 0 0 0 56907 60 0 0 25 0 1 0 1855498766 47984640 10593 4294967295 134512640 135167914 3221224448 3221223152 134562864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11715 10593 162 162 0 11553 0
[pid=16328] vsize: 46860
Current children cumulated CPU time (s) 569.68
Current children cumulated vsize (Kb) 48988

[startup+580.898 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11017 0 0 0 57906 61 0 0 25 0 1 0 1855498766 48160768 10637 4294967295 134512640 135167914 3221224448 3221223156 134558184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11758 10637 162 162 0 11596 0
[pid=16328] vsize: 47032
Current children cumulated CPU time (s) 579.68
Current children cumulated vsize (Kb) 49160

[startup+590.899 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11102 0 0 0 58905 61 0 0 25 0 1 0 1855498766 48496640 10722 4294967295 134512640 135167914 3221224448 3221223156 134558102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11840 10722 162 162 0 11678 0
[pid=16328] vsize: 47360
Current children cumulated CPU time (s) 589.67
Current children cumulated vsize (Kb) 49488

[startup+600.9 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11160 0 0 0 59903 62 0 0 25 0 1 0 1855498766 48726016 10780 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 11896 10780 162 162 0 11734 0
[pid=16328] vsize: 47584
Current children cumulated CPU time (s) 599.66
Current children cumulated vsize (Kb) 49712

[startup+610.901 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11217 0 0 0 60902 63 0 0 25 0 1 0 1855498766 48955392 10837 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 11952 10837 162 162 0 11790 0
[pid=16328] vsize: 47808
Current children cumulated CPU time (s) 609.66
Current children cumulated vsize (Kb) 49936

[startup+620.901 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11271 0 0 0 61900 64 0 0 25 0 1 0 1855498766 49164288 10891 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12003 10891 162 162 0 11841 0
[pid=16328] vsize: 48012
Current children cumulated CPU time (s) 619.65
Current children cumulated vsize (Kb) 50140

[startup+630.903 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11310 0 0 0 62899 64 0 0 25 0 1 0 1855498766 49315840 10930 4294967295 134512640 135167914 3221224448 3221223152 134562647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12040 10930 162 162 0 11878 0
[pid=16328] vsize: 48160
Current children cumulated CPU time (s) 629.64
Current children cumulated vsize (Kb) 50288

[startup+640.904 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11385 0 0 0 63897 66 0 0 25 0 1 0 1855498766 49614848 11005 4294967295 134512640 135167914 3221224448 3221223152 134562618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12113 11005 162 162 0 11951 0
[pid=16328] vsize: 48452
Current children cumulated CPU time (s) 639.64
Current children cumulated vsize (Kb) 50580

[startup+650.904 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11432 0 0 0 64896 66 0 0 25 0 1 0 1855498766 49803264 11052 4294967295 134512640 135167914 3221224448 3221223120 134562249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12159 11052 162 162 0 11997 0
[pid=16328] vsize: 48636
Current children cumulated CPU time (s) 649.63
Current children cumulated vsize (Kb) 50764

[startup+660.906 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11476 0 0 0 65895 67 0 0 25 0 1 0 1855498766 49975296 11096 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12201 11096 162 162 0 12039 0
[pid=16328] vsize: 48804
Current children cumulated CPU time (s) 659.63
Current children cumulated vsize (Kb) 50932

[startup+670.907 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11530 0 0 0 66893 68 0 0 25 0 1 0 1855498766 50192384 11150 4294967295 134512640 135167914 3221224448 3221223152 134562932 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12254 11150 162 162 0 12092 0
[pid=16328] vsize: 49016
Current children cumulated CPU time (s) 669.62
Current children cumulated vsize (Kb) 51144

[startup+680.908 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11576 0 0 0 67892 69 0 0 25 0 1 0 1855498766 50372608 11196 4294967295 134512640 135167914 3221224448 3221223168 134560255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12298 11196 162 162 0 12136 0
[pid=16328] vsize: 49192
Current children cumulated CPU time (s) 679.62
Current children cumulated vsize (Kb) 51320

[startup+690.909 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11637 0 0 0 68890 70 0 0 25 0 1 0 1855498766 50610176 11257 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12356 11257 162 162 0 12194 0
[pid=16328] vsize: 49424
Current children cumulated CPU time (s) 689.61
Current children cumulated vsize (Kb) 51552

[startup+700.911 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11703 0 0 0 69889 71 0 0 25 0 1 0 1855498766 50872320 11323 4294967295 134512640 135167914 3221224448 3221223120 134562384 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12420 11323 162 162 0 12258 0
[pid=16328] vsize: 49680
Current children cumulated CPU time (s) 699.61
Current children cumulated vsize (Kb) 51808

[startup+710.912 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11752 0 0 0 70887 72 0 0 25 0 1 0 1855498766 51068928 11372 4294967295 134512640 135167914 3221224448 3221223136 134566754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12468 11372 162 162 0 12306 0
[pid=16328] vsize: 49872
Current children cumulated CPU time (s) 709.6
Current children cumulated vsize (Kb) 52000

[startup+720.913 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 11804 0 0 0 71886 73 0 0 25 0 1 0 1855498766 51277824 11424 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16328/statm): 12519 11424 162 162 0 12357 0
[pid=16328] vsize: 50076
Current children cumulated CPU time (s) 719.6
Current children cumulated vsize (Kb) 52204

[startup+730.914 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 13294 0 0 0 72871 81 0 0 23 0 1 0 1855498766 56680448 12789 4294967295 134512640 135167914 3221224448 3220913632 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 13838 12789 162 162 0 13676 0
[pid=16328] vsize: 55352
Current children cumulated CPU time (s) 729.53
Current children cumulated vsize (Kb) 57480

[startup+740.914 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 73839 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215808 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 739.37
Current children cumulated vsize (Kb) 68848

[startup+750.916 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 74839 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215432 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 749.37
Current children cumulated vsize (Kb) 68848

[startup+760.916 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 75839 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215776 134720503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 759.37
Current children cumulated vsize (Kb) 68848

[startup+770.916 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 76840 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215984 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 769.38
Current children cumulated vsize (Kb) 68848

[startup+780.917 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 77840 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215920 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 779.38
Current children cumulated vsize (Kb) 68848

[startup+790.917 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 78840 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215756 134723269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 789.38
Current children cumulated vsize (Kb) 68848

[startup+800.918 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 79840 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216000 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 799.38
Current children cumulated vsize (Kb) 68848

[startup+810.919 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 80841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216096 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 809.39
Current children cumulated vsize (Kb) 68848

[startup+820.92 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 81841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216184 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 819.39
Current children cumulated vsize (Kb) 68848

[startup+830.92 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 82841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216704 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 829.39
Current children cumulated vsize (Kb) 68848

[startup+840.921 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 83841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215884 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 839.39
Current children cumulated vsize (Kb) 68848

[startup+850.922 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 84841 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216484 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 849.39
Current children cumulated vsize (Kb) 68848

[startup+860.922 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 85842 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216160 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 859.4
Current children cumulated vsize (Kb) 68848

[startup+870.923 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 86842 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216076 134718182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 869.4
Current children cumulated vsize (Kb) 68848

[startup+880.924 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 87842 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216752 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 879.4
Current children cumulated vsize (Kb) 68848

[startup+890.924 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 88842 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215772 134722231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 889.4
Current children cumulated vsize (Kb) 68848

[startup+900.924 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 89843 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215776 134720472 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 899.41
Current children cumulated vsize (Kb) 68848

[startup+910.925 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 90843 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221217040 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 909.41
Current children cumulated vsize (Kb) 68848

[startup+920.925 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 91843 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216368 134629353 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 919.41
Current children cumulated vsize (Kb) 68848

[startup+930.925 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 92843 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215904 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 929.41
Current children cumulated vsize (Kb) 68848

[startup+940.926 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 93844 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215776 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 939.42
Current children cumulated vsize (Kb) 68848

[startup+950.927 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 94844 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215808 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 949.42
Current children cumulated vsize (Kb) 68848

[startup+960.928 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 95844 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216728 134629360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 959.42
Current children cumulated vsize (Kb) 68848

[startup+970.928 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 96844 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216464 134696233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 969.42
Current children cumulated vsize (Kb) 68848

[startup+980.929 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 97845 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216416 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 979.43
Current children cumulated vsize (Kb) 68848

[startup+990.93 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 98845 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215984 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 989.43
Current children cumulated vsize (Kb) 68848

[startup+1000.93 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 99845 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216016 134629373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 999.43
Current children cumulated vsize (Kb) 68848

[startup+1010.93 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 100845 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216856 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1009.43
Current children cumulated vsize (Kb) 68848

[startup+1020.93 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 101846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216352 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1019.44
Current children cumulated vsize (Kb) 68848

[startup+1030.93 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 102846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216304 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1029.44
Current children cumulated vsize (Kb) 68848

[startup+1040.93 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 103846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215920 134844650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1039.44
Current children cumulated vsize (Kb) 68848

[startup+1050.93 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 104846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216448 134696304 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1049.44
Current children cumulated vsize (Kb) 68848

[startup+1060.93 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 105846 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221217216 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1059.44
Current children cumulated vsize (Kb) 68848

[startup+1070.93 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 106847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216112 134696264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1069.45
Current children cumulated vsize (Kb) 68848

[startup+1080.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 107847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216448 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1079.45
Current children cumulated vsize (Kb) 68848

[startup+1090.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 108847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216032 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1089.45
Current children cumulated vsize (Kb) 68848

[startup+1100.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 109847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216320 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1099.45
Current children cumulated vsize (Kb) 68848

[startup+1110.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 110847 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216176 134694329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1109.45
Current children cumulated vsize (Kb) 68848

[startup+1120.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 111848 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215984 134694532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1119.46
Current children cumulated vsize (Kb) 68848

[startup+1130.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 112848 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216324 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1129.46
Current children cumulated vsize (Kb) 68848

[startup+1140.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 113848 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216512 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1139.46
Current children cumulated vsize (Kb) 68848

[startup+1150.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 114848 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216096 134844691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1149.46
Current children cumulated vsize (Kb) 68848

[startup+1160.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 115849 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221215968 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1159.47
Current children cumulated vsize (Kb) 68848

[startup+1170.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 116849 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216448 134696350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1169.47
Current children cumulated vsize (Kb) 68848

[startup+1180.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 117849 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216336 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1179.47
Current children cumulated vsize (Kb) 68848

[startup+1190.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 118849 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216336 134694495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1189.47
Current children cumulated vsize (Kb) 68848

[startup+1200.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 119850 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216780 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1199.48
Current children cumulated vsize (Kb) 68848

[startup+1210.94 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 120850 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216208 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1209.48
Current children cumulated vsize (Kb) 68848



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.95 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 16328
Raw data (/proc/16323/stat): 16323 (minisat+_script) S 16322 16323 21452 0 -1 0 314 331 0 0 0 0 0 1 22 0 1 0 1855498759 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/16323/statm): 532 234 485 147 0 385 0
[pid=16323] vsize: 2128
Raw data (/proc/16328/stat): 16328 (minisat+_bignum) R 16323 16323 21452 0 -1 0 17063 0 0 0 120850 97 0 0 25 0 1 0 1855498766 68321280 15404 4294967295 134512640 135167914 3221224448 3221216272 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16328/statm): 16680 15404 162 162 0 16518 0
[pid=16328] vsize: 66720
Current children cumulated CPU time (s) 1209.48
Current children cumulated vsize (Kb) 68848

Sending SIGTERM to -16323
Sleeping 2 seconds
One traced child (pid=16323) ended because it received signal 15 (SIGTERM)
One traced child (pid=16328) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.99
CPU time (s): 1209.52
CPU user time (s): 1208.51
CPU system time (s): 1.00585
CPU usage (%): 99.8784
Max. virtual memory (cumulated for all children) (Kb): 68848

Verifier Data

ERROR: no interpretation found !