Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-5.opb |
MD5SUM | 54f6acf3ab92bda8abb11350f74de20e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -37 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1150 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 1150 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1150 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.08 |
Number of variables | 1150 |
Total number of constraints | 80035 |
Number of constraints which are clauses | 80035 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc7 THE 2005-05-25 17:20:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21920 boxname=wulflinc7 idbench=338 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 54f6acf3ab92bda8abb11350f74de20e /oldhome/oroussel/tmp/wulflinc7/normalized-frb50-23-5.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-frb50-23-5.opb IDLAUNCH: 21920 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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 : 451.050 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: 530264 kB Buffers: 33084 kB Cached: 451000 kB SwapCached: 756 kB Active: 73084 kB Inactive: 413120 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 530012 kB SwapTotal: 2097136 kB SwapFree: 2095584 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5140 kB Slab: 12600 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 17:41:23 (client local time) WITH STATUS 152 IN 1229.87 SECONDS stats: 21920 7 1229.87 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 80035 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 80035 160070 | 26678 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -37[0m c ---[ 0]---> Sorter-cost:63046 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 147951 319392 | 49317 0 0 nan | 0.000 % | c | 100 | 147312 318040 | 54248 57 1282 22.5 | 0.772 % | c | 251 | 146773 316900 | 59673 187 2917 15.6 | 1.422 % | c | 476 | 145213 313544 | 65640 368 5352 14.5 | 3.429 % | c | 813 | 143505 309796 | 72205 621 8354 13.5 | 5.644 % | c | 1320 | 139677 301273 | 79425 1008 13306 13.2 | 10.638 % | c | 2079 | 135693 292365 | 87368 1543 19391 12.6 | 15.964 % | c | 3218 | 129784 278974 | 96104 2359 29829 12.6 | 24.035 % | c | 4926 | 122432 262085 | 105715 3616 48944 13.5 | 34.279 % | c | 7488 | 111938 237654 | 116286 5258 69109 13.1 | 49.006 % | c | 11332 | 101310 212553 | 127915 7785 111547 14.3 | 64.438 % | c ============================================================================== c [1mFound solution: -38[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14084 | 96816 201835 | 32272 9412 143299 15.2 | 64.438 % | c | 14184 | 96772 201727 | 35499 9499 144028 15.2 | 71.052 % | c | 14334 | 96570 201231 | 39049 9550 144833 15.2 | 71.359 % | c | 14560 | 96295 200569 | 42954 9703 147277 15.2 | 71.772 % | c ============================================================================== c [1mFound solution: -40[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14788 | 96036 200007 | 32012 9819 147145 15.0 | 71.772 % | c | 14888 | 96036 200007 | 35213 9919 148330 15.0 | 72.243 % | c | 15038 | 96036 200007 | 38734 10069 149721 14.9 | 72.243 % | c | 15263 | 96036 200007 | 42607 10294 154570 15.0 | 72.243 % | c | 15600 | 95761 199378 | 46868 10569 160536 15.2 | 72.625 % | c | 16106 | 95153 197892 | 51555 10886 169202 15.5 | 73.553 % | c | 16865 | 94758 196946 | 56711 11525 181628 15.8 | 74.144 % | c | 18004 | 94310 195868 | 62382 12430 205545 16.5 | 74.813 % | c | 19713 | 94001 195126 | 68620 13894 265668 19.1 | 75.275 % | c | 22276 | 92381 191245 | 75482 15687 319719 20.4 | 77.691 % | c | 26120 | 91522 189173 | 83030 19074 495885 26.0 | 78.980 % | c ============================================================================== c [1mFound solution: -41[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27853 | 91077 188149 | 30359 20461 588458 28.8 | 78.980 % | c | 27953 | 91077 188149 | 33394 20561 590686 28.7 | 79.629 % | c | 28103 | 91026 188021 | 36734 20631 592469 28.7 | 79.706 % | c | 28328 | 91026 188021 | 40407 20856 599678 28.8 | 79.706 % | c | 28665 | 91026 188021 | 44448 21193 622260 29.4 | 79.706 % | c ============================================================================== c [1mFound solution: -42[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28969 | 90731 187263 | 30243 21322 628608 29.5 | 79.706 % | c | 29069 | 90722 187240 | 33267 21414 632006 29.5 | 80.173 % | c | 29219 | 90593 186934 | 36594 21396 633325 29.6 | 80.358 % | c | 29445 | 90536 186795 | 40253 21617 652375 30.2 | 80.447 % | c | 29782 | 90499 186706 | 44278 21904 668251 30.5 | 80.503 % | c | 30289 | 90299 186216 | 48706 22108 682253 30.9 | 80.809 % | c | 31048 | 90231 186060 | 53577 22782 711877 31.2 | 80.904 % | c | 32187 | 89778 184940 | 58935 23599 766824 32.5 | 81.598 % | c | 33896 | 89773 184929 | 64828 25280 869667 34.4 | 81.605 % | c | 36458 | 89601 184511 | 71311 27781 1104154 39.7 | 81.868 % | c | 40303 | 89001 183057 | 78442 30883 1452224 47.0 | 82.782 % | c | 46069 | 88653 182193 | 86286 36261 1909440 52.7 | 83.326 % | c ============================================================================== c [1mFound solution: -43[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 53577 | 88651 182222 | 29550 43705 2561808 58.6 | 83.326 % | c | 53677 | 88651 182222 | 32505 43805 2563789 58.5 | 83.359 % | c | 53827 | 88622 182151 | 35755 43811 2568576 58.6 | 83.404 % | c | 54052 | 88622 182151 | 39331 44036 2589935 58.8 | 83.404 % | c | 54389 | 88537 181938 | 43264 44316 2602581 58.7 | 83.542 % | c | 54895 | 88502 181851 | 47590 44743 2640960 59.0 | 83.598 % | c | 55654 | 88489 181818 | 52349 45410 2688658 59.2 | 83.620 % | c | 56795 | 88255 181245 | 57584 46245 2798146 60.5 | 83.970 % | c | 58504 | 88255 181245 | 63343 47954 2931810 61.1 | 83.970 % | c | 61066 | 88117 180910 | 69677 50021 3189748 63.8 | 84.181 % | c | 64910 | 88088 180842 | 76645 53834 3616238 67.2 | 84.220 % | c | 70676 | 88083 180831 | 84309 59598 4123646 69.2 | 84.226 % | c ============================================================================== c [1mFound solution: -45[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 76602 | 87920 180446 | 29306 64994 4731142 72.8 | 84.226 % | c | 76704 | 87920 180446 | 32236 65096 4739491 72.8 | 84.488 % | c | 76855 | 87920 180446 | 35460 65247 4745429 72.7 | 84.488 % | c | 77080 | 87920 180446 | 39006 65472 4759519 72.7 | 84.488 % | c | 77417 | 87920 180446 | 42906 65809 4783089 72.7 | 84.488 % | c | 77924 | 87920 180446 | 47197 66316 4834519 72.9 | 84.488 % | c | 78684 | 87915 180435 | 51917 67073 4915209 73.3 | 84.494 % | c | 79823 | 87782 180128 | 57109 67701 5020176 74.2 | 84.681 % | c | 81531 | 87629 179763 | 62820 69363 5207979 75.1 | 84.907 % | c | 84093 | 87629 179763 | 69102 71925 5462668 75.9 | 84.907 % | c | 87937 | 87629 179763 | 76012 75769 5852613 77.2 | 84.907 % | c | 93703 | 87615 179727 | 83613 81487 6335995 77.8 | 84.931 % | c | 102352 | 87615 179727 | 91974 90136 7289858 80.9 | 84.931 % | c | 115328 | 87613 179723 | 101172 103111 8798918 85.3 | 84.933 % | c | 134790 | 87540 179550 | 111289 122522 11000809 89.8 | 85.040 % | c | 163982 | 87270 178893 | 122418 150898 14231492 94.3 | 85.455 % | c | 207771 | 87197 178706 | 134660 54694 5876777 107.4 | 85.578 % | c | 273455 | 87182 178671 | 148126 120376 10322069 85.7 | 85.599 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 12844 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.85 0.97 0.91 2/54 12840 Raw data (stat): 12840 (runsolver) R 12839 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782422206 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99991 s] Raw data (loadavg): 0.87 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0009 s] Raw data (loadavg): 0.89 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0012 s] Raw data (loadavg): 0.91 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0008 s] Raw data (loadavg): 0.92 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0017 s] Raw data (loadavg): 0.93 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.94 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0017 s] Raw data (loadavg): 0.95 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0016 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0009 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+239.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+389.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+399.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+409.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+419.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+429.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+439.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+449.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+459.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+469.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+479.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+489.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+499.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+509.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+519.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+529.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+539.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+549.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+559.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+569.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+579.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+589.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+599.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+609.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+619.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+629.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+639.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+649.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+659.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+669.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+679.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+689.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+699.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+709.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+719.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+729.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+739.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+749.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+759.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+769.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+779.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+789.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+799.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+809.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+819.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+829.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+839.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+849.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+859.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+869.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+879.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+889.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+899.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+909.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+919.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+929.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+939.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+949.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+959.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+969.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+979.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+989.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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+999.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.71 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 12844 Raw data (stat): 12840 (minisat+_script) S 12839 24300 24299 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782422206 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.71 CPU time (s): 1229.87 CPU user time (s): 1229.12 CPU system time (s): 0.753885 CPU usage (%): 100.013 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####