Name | normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-sctap1.opb |
MD5SUM | 3742d8a4a6db91830db1829244573c45 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2147483647 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 10800 |
Biggest coefficient in the objective function | 42949672960 |
Number of bits for the biggest coefficient in the objective function | 36 |
Sum of the numbers in the objective function | 6356551592160 |
Number of bits of the sum of numbers in the objective function | 43 |
Biggest number in a constraint | 42949672960 |
Number of bits of the biggest number in a constraint | 36 |
Biggest sum of numbers in a constraint | 6356551592160 |
Number of bits of the biggest sum of numbers | 43 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1221.94 |
Number of variables | 14400 |
Total number of constraints | 300 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 300 |
Minimum length of a constraint | 90 |
Maximum length of a constraint | 660 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc10 THE 2005-05-25 18:23:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22055 boxname=wulflinc10 idbench=871 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 3742d8a4a6db91830db1829244573c45 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-sctap1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-sctap1.opb IDLAUNCH: 22055 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 2 cpu MHz : 450.999 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: 627664 kB Buffers: 35172 kB Cached: 349616 kB SwapCached: 92 kB Active: 64240 kB Inactive: 323228 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 627412 kB SwapTotal: 2097136 kB SwapFree: 2096752 kB Dirty: 4 kB Writeback: 0 kB Mapped: 6392 kB Slab: 13908 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 18:43:42 (client local time) WITH STATUS 152 IN 1229.9 SECONDS stats: 22055 7 1229.9 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 404 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ######################################################################################################################## c -- Clauses(.)/Splits(s): ss c ---[ 405]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 404]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 403]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 402]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 401]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 400]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 399]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 398]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 397]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 396]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 395]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 394]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 393]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 392]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 391]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 390]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 389]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 388]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 387]---> Sorter-cost: 2697 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 386]---> Sorter-cost: 2697 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 385]---> Sorter-cost: 2697 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 384]---> Sorter-cost: 2697 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 383]---> Sorter-cost: 2697 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 382]---> Sorter-cost: 2697 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 381]---> Sorter-cost: 2697 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 380]---> Sorter-cost: 2697 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 379]---> Sorter-cost: 2697 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 378]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 377]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 376]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 375]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 374]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 373]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 372]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 371]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 370]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 369]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 368]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 367]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 366]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 365]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 364]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 363]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 362]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 361]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 360]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 359]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 358]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 357]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 356]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 355]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 354]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 353]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 352]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 351]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 350]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 349]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 348]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 347]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 346]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 345]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 344]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 343]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 342]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 341]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 340]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 339]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 338]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 337]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 336]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 335]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 334]---> Sorter-cost: 3051 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 333]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 332]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 331]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 330]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 329]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 328]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 327]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 326]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 325]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 324]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 323]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 322]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 321]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 320]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 319]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 318]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 317]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 316]---> Sorter-cost: 1645 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 315]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 314]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 313]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 312]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 311]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 310]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 309]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 308]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 307]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 306]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 305]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 304]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 303]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 302]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 301]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 300]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 299]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 298]---> Sorter-cost: 2746 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 296]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 294]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 292]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 290]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 288]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 286]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 284]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 282]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 280]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 278]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 276]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 274]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 272]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 270]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 268]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 266]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 264]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 262]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 260]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 258]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 256]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 254]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 252]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 250]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 248]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 246]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 244]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 242]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 240]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 238]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 236]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 234]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 232]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 230]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 228]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 226]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 224]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 222]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 220]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 218]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 216]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 214]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 212]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 210]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 208]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 206]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 204]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 202]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 200]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 198]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 196]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 194]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 192]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 190]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 188]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 186]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 184]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 182]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 180]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 178]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 176]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 174]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 172]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 156]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 154]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 152]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 150]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 148]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 146]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 144]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 142]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 140]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 138]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 136]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 134]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 132]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 130]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 128]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 124]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 122]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 118]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 116]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 114]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 110]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 108]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 104]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 102]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 100]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 98]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 96]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 94]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 92]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 90]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 88]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 86]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 84]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 82]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 80]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 78]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 76]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 74]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 72]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 70]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 68]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 66]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 62]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 58]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 55]---> Adder-cost: 700 maxlim: 2147569624 bits: 33/32 c ---[ 54]---> Adder-cost: 700 maxlim: 2147579864 bits: 33/32 c ---[ 53]---> Adder-cost: 700 maxlim: 2147569624 bits: 33/32 c ---[ 52]---> Adder-cost: 700 maxlim: 2147562456 bits: 33/32 c ---[ 51]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 50]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 49]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 48]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 47]---> Adder-cost: 1224 maxlim: 4295067594 bits: 34/33 c ---[ 45]---> Adder-cost: 1224 maxlim: 4295098314 bits: 34/33 c ---[ 44]---> Adder-cost: 1224 maxlim: 4295108554 bits: 34/33 c ---[ 43]---> Adder-cost: 1224 maxlim: 4295098314 bits: 34/33 c ---[ 42]---> Adder-cost: 1224 maxlim: 4295093194 bits: 34/33 c ---[ 41]---> Adder-cost: 1224 maxlim: 4295088074 bits: 34/33 c ---[ 40]---> Adder-cost: 1224 maxlim: 4295077834 bits: 34/33 c ---[ 39]---> Adder-cost: 1224 maxlim: 4295067594 bits: 34/33 c ---[ 38]---> Adder-cost: 1224 maxlim: 4295067594 bits: 34/33 c ---[ 37]---> Sorter-cost: 3604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 3612 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost: 3604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 3604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 3604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 3604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 3604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 3604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 29]---> Sorter-cost: 3604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Adder-cost: 906 maxlim: 2147772272 bits: 33/32 c ---[ 27]---> Adder-cost: 906 maxlim: 2147777392 bits: 33/32 c ---[ 26]---> Adder-cost: 906 maxlim: 2147782512 bits: 33/32 c ---[ 25]---> Adder-cost: 906 maxlim: 2147792752 bits: 33/32 c ---[ 24]---> Adder-cost: 906 maxlim: 2147787632 bits: 33/32 c ---[ 23]---> Adder-cost: 906 maxlim: 2147782512 bits: 33/32 c ---[ 22]---> Adder-cost: 906 maxlim: 2147782512 bits: 33/32 c ---[ 21]---> Adder-cost: 906 maxlim: 2147777392 bits: 33/32 c ---[ 20]---> Adder-cost: 906 maxlim: 2147772272 bits: 33/32 c ---[ 19]---> Adder-cost: 968 maxlim: 2147759990 bits: 33/32 c ---[ 18]---> Adder-cost: 968 maxlim: 2147759990 bits: 33/32 c ---[ 17]---> Adder-cost: 968 maxlim: 2147775350 bits: 33/32 c ---[ 16]---> Adder-cost: 968 maxlim: 2147800950 bits: 33/32 c ---[ 15]---> Adder-cost: 968 maxlim: 2147790710 bits: 33/32 c ---[ 14]---> Adder-cost: 968 maxlim: 2147780470 bits: 33/32 c ---[ 13]---> Adder-cost: 968 maxlim: 2147770230 bits: 33/32 c ---[ 12]---> Adder-cost: 968 maxlim: 2147759990 bits: 33/32 c ---[ 11]---> Adder-cost: 968 maxlim: 2147759990 bits: 33/32 c ---[ 10]---> Adder-cost: 442 maxlim: 1073807326 bits: 32/31 c ---[ 9]---> Adder-cost: 442 maxlim: 1073807326 bits: 32/31 c ---[ 8]---> Adder-cost: 442 maxlim: 1073807326 bits: 32/31 c ---[ 7]---> Adder-cost: 442 maxlim: 1073807326 bits: 32/31 c ---[ 6]---> Adder-cost: 442 maxlim: 1073812446 bits: 32/31 c ---[ 5]---> Adder-cost: 442 maxlim: 1073822686 bits: 32/31 c ---[ 4]---> Adder-cost: 442 maxlim: 1073827806 bits: 32/31 c ---[ 3]---> Adder-cost: 442 maxlim: 1073817566 bits: 32/31 c ---[ 2]---> Adder-cost: 442 maxlim: 1073812446 bits: 32/31 c ---[ 1]---> Adder-cost: 226 maxlim: 5119 bits: 14/13 c ---[ 0]---> Adder-cost: 435 maxlim: 5119 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1087332 2874465 | 362444 0 0 nan | 0.000 % | c | 100 | 1087332 2874465 | 398688 100 786 7.9 | 2.890 % | c | 253 | 1087302 2874399 | 438557 252 1656 6.6 | 2.893 % | c | 478 | 1087281 2874353 | 482412 476 3907 8.2 | 2.894 % | c | 815 | 1087232 2874245 | 530654 810 6543 8.1 | 2.899 % | c | 1321 | 1087218 2874214 | 583719 1315 10917 8.3 | 2.900 % | c | 2080 | 1087167 2874103 | 642091 2070 19416 9.4 | 2.904 % | c | 3219 | 1087108 2873972 | 706300 3202 30209 9.4 | 2.909 % | c | 4928 | 1087108 2873972 | 776930 4911 46317 9.4 | 2.909 % | c | 7492 | 1087078 2873905 | 854623 7473 66923 9.0 | 2.912 % | c | 11336 | 1087040 2873821 | 940086 11316 100803 8.9 | 2.915 % | c | 17102 | 1086682 2873027 | 1034095 17062 146933 8.6 | 2.943 % | c | 25751 | 1085819 2871117 | 1137504 25671 237679 9.3 | 3.012 % | c | 38726 | 1085257 2869872 | 1251254 38617 345891 9.0 | 3.057 % | c | 58187 | 1083917 2866886 | 1376380 58015 530876 9.2 | 3.167 % | c | 87380 | 1082317 2863339 | 1514018 87084 827993 9.5 | 3.300 % | c | 131169 | 1079997 2858186 | 1665420 130771 1237628 9.5 | 3.489 % | c | 196855 | 1076637 2850709 | 1831962 196279 1940424 9.9 | 3.768 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 1214 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.82 0.92 0.92 2/54 1210 Raw data (stat): 1210 (runsolver) R 1209 15547 15546 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782801373 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 0.84 0.92 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0013 s] Raw data (loadavg): 0.87 0.92 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0015 s] Raw data (loadavg): 0.89 0.92 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0011 s] Raw data (loadavg): 0.90 0.92 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0021 s] Raw data (loadavg): 0.92 0.93 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0022 s] Raw data (loadavg): 0.93 0.93 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0028 s] Raw data (loadavg): 0.94 0.93 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0038 s] Raw data (loadavg): 0.95 0.93 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0039 s] Raw data (loadavg): 0.96 0.93 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.96 0.94 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.004 s] Raw data (loadavg): 0.97 0.94 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.005 s] Raw data (loadavg): 0.97 0.94 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.004 s] Raw data (loadavg): 0.98 0.94 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.004 s] Raw data (loadavg): 0.98 0.94 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.004 s] Raw data (loadavg): 0.98 0.94 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.005 s] Raw data (loadavg): 0.98 0.94 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.005 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.004 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.008 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.009 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.009 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.01 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.01 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.01 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.01 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.011 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.01 s] Raw data (loadavg): 0.99 0.95 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.009 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.011 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.01 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.01 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.01 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.009 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.009 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.009 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.01 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.01 s] Raw data (loadavg): 0.99 0.96 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.01 s] Raw data (loadavg): 1.15 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.009 s] Raw data (loadavg): 1.12 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.009 s] Raw data (loadavg): 1.10 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.009 s] Raw data (loadavg): 1.09 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.009 s] Raw data (loadavg): 1.07 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.009 s] Raw data (loadavg): 1.06 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.008 s] Raw data (loadavg): 1.05 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.008 s] Raw data (loadavg): 1.04 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.12 s] Raw data (loadavg): 1.04 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.12 s] Raw data (loadavg): 1.03 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.119 s] Raw data (loadavg): 1.03 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.119 s] Raw data (loadavg): 1.02 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.119 s] Raw data (loadavg): 1.02 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.119 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.119 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.119 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.119 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.119 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.119 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.119 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.119 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.119 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.119 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.119 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.119 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.119 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.119 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.121 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.121 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.121 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.13 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.12 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.13 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.13 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.13 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.13 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.84 s] Raw data (loadavg): 1.00 1.00 0.93 1/53 1214 Raw data (stat): 1210 (minisat+_script) S 1209 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 17 0 1 0 782801373 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.84 CPU time (s): 1229.9 CPU user time (s): 1228.78 CPU system time (s): 1.11583 CPU usage (%): 100.005 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####