Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-3.opb |
MD5SUM | 140696e76e8ed6af142b84a22a9a8f01 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -38 |
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.09 |
Number of variables | 1150 |
Total number of constraints | 81068 |
Number of constraints which are clauses | 81068 |
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 wulflinc21 THE 2005-04-14 01:03:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4096 boxname=wulflinc21 idbench=336 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 140696e76e8ed6af142b84a22a9a8f01 /oldhome/oroussel/tmp/wulflinc21/normalized-frb50-23-3.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc21/normalized-frb50-23-3.opb /oldhome/oroussel/tmp/wulflinc21/normalized-frb50-23-3.opb IDLAUNCH: 4096 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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: 878296 kB Buffers: 27476 kB Cached: 108456 kB SwapCached: 0 kB Active: 36204 kB Inactive: 102632 kB HighTotal: 131008 kB HighFree: 18900 kB LowTotal: 903652 kB LowFree: 859396 kB SwapTotal: 2097892 kB SwapFree: 2097804 kB Dirty: 40 kB Writeback: 0 kB Mapped: 6928 kB Slab: 11900 kB Committed_AS: 63796 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 01:23:47 (client local time) WITH STATUS 10 IN 1209.81 SECONDS stats: 4096 7 1209.81 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 81068 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 81068 162136 | 24320 0 0 nan | 0.000 % | c -- subsuming c | 0 | 81068 162136 | 32427 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 4.30234 s) c ============================================================================== c [1mFound solution: -34[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:63046 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 148830 321097 | 44648 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/46117 c -- var.elim.: 2000/46117 c -- var.elim.: 3000/46117 c -- var.elim.: 4000/46117 c -- var.elim.: 5000/46117 c -- var.elim.: 6000/46117 c -- var.elim.: 7000/46117 c -- var.elim.: 8000/46117 c -- var.elim.: 9000/46117 c -- var.elim.: 10000/46117 c -- var.elim.: 11000/46117 c -- var.elim.: 12000/46117 c -- var.elim.: 13000/46117 c -- var.elim.: 14000/46117 c -- var.elim.: 15000/46117 c -- var.elim.: 16000/46117 c -- var.elim.: 17000/46117 c -- var.elim.: 18000/46117 c -- var.elim.: 19000/46117 c -- var.elim.: 20000/46117 c -- var.elim.: 21000/46117 c -- var.elim.: 22000/46117 c -- var.elim.: 23000/46117 c -- var.elim.: 24000/46117 c -- var.elim.: 25000/46117 c -- var.elim.: 26000/46117 c -- var.elim.: 27000/46117 c -- var.elim.: 28000/46117 c -- var.elim.: 29000/46117 c -- var.elim.: 30000/46117 c -- var.elim.: 31000/46117 c -- var.elim.: 32000/46117 c -- var.elim.: 33000/46117 c -- var.elim.: 34000/46117 c -- var.elim.: 35000/46117 c -- var.elim.: 36000/46117 c -- var.elim.: 37000/46117 c -- var.elim.: 38000/46117 c -- var.elim.: 39000/46117 c -- var.elim.: 40000/46117 c -- var.elim.: 41000/46117 c -- var.elim.: 42000/46117 c -- var.elim.: 43000/46117 c -- var.elim.: 44000/46117 c -- var.elim.: 45000/46117 c -- var.elim.: 46000/46117 c -- var.elim.: 46117/46117 c -- var.elim.: 1000/23378 c -- var.elim.: 2000/23378 c -- var.elim.: 3000/23378 c -- var.elim.: 4000/23378 c -- var.elim.: 5000/23378 c -- var.elim.: 6000/23378 c -- var.elim.: 7000/23378 c -- var.elim.: 8000/23378 c -- var.elim.: 9000/23378 c -- var.elim.: 10000/23378 c -- var.elim.: 11000/23378 c -- var.elim.: 12000/23378 c -- var.elim.: 13000/23378 c -- var.elim.: 14000/23378 c -- var.elim.: 15000/23378 c -- var.elim.: 16000/23378 c -- var.elim.: 17000/23378 c -- var.elim.: 18000/23378 c -- var.elim.: 19000/23378 c -- var.elim.: 20000/23378 c -- var.elim.: 21000/23378 c -- var.elim.: 22000/23378 c -- var.elim.: 23000/23378 c -- var.elim.: 23378/23378 c -- var.elim.: 195/195 c -- var.elim.: 108/108 c -- subsuming c -- var.elim.: 1000/9152 c -- var.elim.: 2000/9152 c -- var.elim.: 3000/9152 c -- var.elim.: 4000/9152 c -- var.elim.: 5000/9152 c -- var.elim.: 6000/9152 c -- var.elim.: 7000/9152 c -- var.elim.: 8000/9152 c -- var.elim.: 9000/9152 c -- var.elim.: 9152/9152 c -- var.elim.: 303/303 c | 0 | 100892 340188 | -- 0 -- -- | -- | -47932/19109 c | 0 | 100892 340188 | 40356 0 0 nan | 0.000 % | c | 101 | 100892 340188 | 44392 101 12083 119.6 | 53.747 % | c | 251 | 100892 340188 | 48831 251 35097 139.8 | 53.747 % | c | 476 | 100892 340188 | 53714 476 100999 212.2 | 53.747 % | c | 813 | 100892 340188 | 59086 813 171228 210.6 | 53.747 % | c | 1319 | 100892 340188 | 64995 1319 271760 206.0 | 53.747 % | c | 2078 | 100892 340188 | 71494 2078 384347 185.0 | 53.747 % | c | 3217 | 100892 340188 | 78643 3217 617334 191.9 | 53.747 % | c | 4925 | 100892 340188 | 86508 4925 1049314 213.1 | 53.747 % | c ============================================================================== c (current CPU-time: 307.105 s) c ============================================================================== c [1mFound solution: -36[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 6025 | 111239 368545 | 33371 6025 1316312 218.5 | 53.747 % | c -- subsuming c -- var.elim.: 1000/17884 c -- var.elim.: 2000/17884 c -- var.elim.: 3000/17884 c -- var.elim.: 4000/17884 c -- var.elim.: 5000/17884 c -- var.elim.: 6000/17884 c -- var.elim.: 7000/17884 c -- var.elim.: 8000/17884 c -- var.elim.: 9000/17884 c -- var.elim.: 10000/17884 c -- var.elim.: 11000/17884 c -- var.elim.: 12000/17884 c -- var.elim.: 13000/17884 c -- var.elim.: 14000/17884 c -- var.elim.: 15000/17884 c -- var.elim.: 16000/17884 c -- var.elim.: 17000/17884 c -- var.elim.: 17884/17884 c -- var.elim.: 1000/7671 c -- var.elim.: 2000/7671 c -- var.elim.: 3000/7671 c -- var.elim.: 4000/7671 c -- var.elim.: 5000/7671 c -- var.elim.: 6000/7671 c -- var.elim.: 7000/7671 c -- var.elim.: 7671/7671 c -- var.elim.: 222/222 c -- subsuming c -- var.elim.: 1000/6351 c -- var.elim.: 2000/6351 c -- var.elim.: 3000/6351 c -- var.elim.: 4000/6351 c -- var.elim.: 5000/6351 c -- var.elim.: 6000/6351 c -- var.elim.: 6351/6351 c -- var.elim.: 94/94 c | 6025 | 101008 348080 | -- 6025 -- -- | -- | -10214/-18482 c | 6025 | 101008 348080 | 40403 5721 1059944 185.3 | 53.747 % | c | 6125 | 101008 348080 | 44443 5821 1079767 185.5 | 60.946 % | c | 6275 | 101008 348080 | 48887 5971 1138903 190.7 | 60.946 % | c | 6500 | 101008 348080 | 53776 6196 1194916 192.9 | 60.946 % | c | 6837 | 100964 347593 | 59128 6527 1273665 195.1 | 61.025 % | c | 7343 | 100942 347338 | 65027 7026 1382454 196.8 | 61.065 % | c | 8102 | 100761 345466 | 71401 7777 1559752 200.6 | 61.353 % | c | 9243 | 100725 345072 | 78513 8913 1845029 207.0 | 61.415 % | c | 10951 | 100506 342970 | 86177 10612 2251481 212.2 | 61.776 % | c | 13513 | 100506 342970 | 94795 13174 3141932 238.5 | 61.776 % | c | 17357 | 100329 341231 | 104091 16997 4564597 268.6 | 62.075 % | c | 23123 | 99556 333573 | 113617 22665 6585902 290.6 | 63.389 % | c ============================================================================== c (current CPU-time: 464.324 s) c ============================================================================== c [1mFound solution: -38[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 26253 | 101332 336479 | 30399 25760 7828826 303.9 | 63.389 % | c -- subsuming c -- var.elim.: 1000/11347 c -- var.elim.: 2000/11347 c -- var.elim.: 3000/11347 c -- var.elim.: 4000/11347 c -- var.elim.: 5000/11347 c -- var.elim.: 6000/11347 c -- var.elim.: 7000/11347 c -- var.elim.: 8000/11347 c -- var.elim.: 9000/11347 c -- var.elim.: 10000/11347 c -- var.elim.: 11000/11347 c -- var.elim.: 11347/11347 c -- var.elim.: 1000/3323 c -- var.elim.: 2000/3323 c -- var.elim.: 3000/3323 c -- var.elim.: 3323/3323 c -- var.elim.: 185/185 c | 26253 | 99308 328484 | -- 25760 -- -- | -- | -2007/538 c | 26253 | 99308 328484 | 39723 23860 4766544 199.8 | 63.389 % | c ============================================================================== c (current CPU-time: 492.396 s) c ============================================================================== c [1mFound solution: -39[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 26349 | 108635 353735 | 32590 23956 4817658 201.1 | 63.389 % | c -- subsuming c -- var.elim.: 1000/15825 c -- var.elim.: 2000/15825 c -- var.elim.: 3000/15825 c -- var.elim.: 4000/15825 c -- var.elim.: 5000/15825 c -- var.elim.: 6000/15825 c -- var.elim.: 7000/15825 c -- var.elim.: 8000/15825 c -- var.elim.: 9000/15825 c -- var.elim.: 10000/15825 c -- var.elim.: 11000/15825 c -- var.elim.: 12000/15825 c -- var.elim.: 13000/15825 c -- var.elim.: 14000/15825 c -- var.elim.: 15000/15825 c -- var.elim.: 15825/15825 c -- var.elim.: 1000/6594 c -- var.elim.: 2000/6594 c -- var.elim.: 3000/6594 c -- var.elim.: 4000/6594 c -- var.elim.: 5000/6594 c -- var.elim.: 6000/6594 c -- var.elim.: 6594/6594 c -- var.elim.: 20/20 c -- subsuming c -- var.elim.: 1000/6354 c -- var.elim.: 2000/6354 c -- var.elim.: 3000/6354 c -- var.elim.: 4000/6354 c -- var.elim.: 5000/6354 c -- var.elim.: 6000/6354 c -- var.elim.: 6354/6354 c -- var.elim.: 17/17 c | 26349 | 99432 338231 | -- 23956 -- -- | -- | -9195/-15487 c | 26349 | 99432 338231 | 39772 23956 4817658 201.1 | 63.389 % | c | 26451 | 99432 338231 | 43750 24058 4836397 201.0 | 64.966 % | c | 26601 | 99432 338231 | 48125 24208 4899663 202.4 | 64.966 % | c | 26826 | 99432 338231 | 52937 24433 4947565 202.5 | 64.966 % | c | 27163 | 99368 337768 | 58193 24535 4980443 203.0 | 65.046 % | c | 27669 | 99368 337768 | 64013 25041 5139272 205.2 | 65.046 % | c | 28429 | 99368 337768 | 70414 25801 5410376 209.7 | 65.046 % | c | 29568 | 99248 336626 | 77362 26930 5706240 211.9 | 65.255 % | c | 31276 | 99154 335654 | 85018 28607 6222488 217.5 | 65.419 % | c ============================================================================== c (current CPU-time: 588.496 s) c ============================================================================== c [1mFound solution: -41[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 32594 | 99393 335337 | 29817 29909 6644875 222.2 | 65.419 % | c -- subsuming c -- var.elim.: 1000/8466 c -- var.elim.: 2000/8466 c -- var.elim.: 3000/8466 c -- var.elim.: 4000/8466 c -- var.elim.: 5000/8466 c -- var.elim.: 6000/8466 c -- var.elim.: 7000/8466 c -- var.elim.: 8000/8466 c -- var.elim.: 8466/8466 c -- var.elim.: 356/356 c -- var.elim.: 3/3 c | 32594 | 99038 334813 | -- 29909 -- -- | -- | -355/-523 c | 32594 | 99038 334813 | 39615 29909 6644875 222.2 | 65.419 % | c | 32695 | 99038 334813 | 43576 30010 6678002 222.5 | 65.657 % | c | 32845 | 98970 334150 | 47901 30082 6681152 222.1 | 65.775 % | c | 33070 | 98970 334150 | 52691 30307 6763666 223.2 | 65.775 % | c | 33407 | 98950 333928 | 57949 30632 6869049 224.2 | 65.810 % | c | 33913 | 98874 333160 | 63695 31129 7042506 226.2 | 65.943 % | c | 34672 | 98806 332533 | 70016 31866 7379338 231.6 | 66.061 % | c | 35811 | 98690 331374 | 76927 32984 7732134 234.4 | 66.263 % | c | 37520 | 98630 330797 | 84568 34666 8227094 237.3 | 66.368 % | c | 40082 | 98512 329689 | 92914 37214 9091264 244.3 | 66.570 % | c | 43926 | 98401 328551 | 102090 41026 10483329 255.5 | 66.762 % | c | 49692 | 98107 325728 | 111964 46737 12778050 273.4 | 67.275 % | c | 58341 | 97257 317290 | 122093 55201 15929869 288.6 | 68.725 % | c | 71315 | 96909 313817 | 133822 68091 21048572 309.1 | 69.315 % | c | 90776 | 95797 302642 | 145515 87304 29247279 335.0 | 71.211 % | c c *** TERMINATED *** s SATISFIABLE v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 C601 -C600 -C599 -C598 -C597 C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 C331 -C330 -C329 -C328 -C327 -C326 -C#### 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): 1.28 1.04 0.93 2/55 3122 Raw data (stat): 3122 (runsolver) R 3121 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 357746392 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0003 s] Raw data (loadavg): 1.24 1.03 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9373 0 0 0 955 44 0 0 25 0 1 0 357746392 41185280 8795 4294967295 134512640 134672761 3221224560 3221222864 134566562 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10055 8795 603 41 0 10014 0 vsize: 40220 [startup+20.001 s] Raw data (loadavg): 1.20 1.03 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9374 0 0 0 1954 44 0 0 25 0 1 0 357746392 41185280 8796 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10055 8796 603 41 0 10014 0 vsize: 40220 [startup+30.0021 s] Raw data (loadavg): 1.17 1.03 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9381 0 0 0 2955 44 0 0 25 0 1 0 357746392 41185280 8803 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10055 8803 603 41 0 10014 0 vsize: 40220 [startup+40.0023 s] Raw data (loadavg): 1.14 1.03 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9381 0 0 0 3954 44 0 0 25 0 1 0 357746392 41185280 8803 4294967295 134512640 134672761 3221224560 3221223152 134607938 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10055 8803 603 41 0 10014 0 vsize: 40220 [startup+50.002 s] Raw data (loadavg): 1.12 1.03 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9382 0 0 0 4954 44 0 0 25 0 1 0 357746392 41185280 8804 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10055 8804 603 41 0 10014 0 vsize: 40220 [startup+60.0027 s] Raw data (loadavg): 1.10 1.03 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9383 0 0 0 5954 44 0 0 25 0 1 0 357746392 41185280 8805 4294967295 134512640 134672761 3221224560 3221222992 134604055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10055 8805 603 41 0 10014 0 vsize: 40220 [startup+70.0034 s] Raw data (loadavg): 1.09 1.03 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9384 0 0 0 6955 44 0 0 25 0 1 0 357746392 41185280 8806 4294967295 134512640 134672761 3221224560 3221223056 134644240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10055 8806 603 41 0 10014 0 vsize: 40220 [startup+80.0041 s] Raw data (loadavg): 1.07 1.02 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9390 0 0 0 7955 45 0 0 25 0 1 0 357746392 41185280 8812 4294967295 134512640 134672761 3221224560 3221222992 134605675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10055 8812 603 41 0 10014 0 vsize: 40220 [startup+90.0042 s] Raw data (loadavg): 1.06 1.02 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9391 0 0 0 8954 45 0 0 25 0 1 0 357746392 41185280 8813 4294967295 134512640 134672761 3221224560 3221222880 1075352369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10055 8813 603 41 0 10014 0 vsize: 40220 [startup+100.003 s] Raw data (loadavg): 1.05 1.02 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9395 0 0 0 9954 45 0 0 25 0 1 0 357746392 41349120 8817 4294967295 134512640 134672761 3221224560 3221223040 134541816 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10095 8817 603 41 0 10054 0 vsize: 40380 [startup+110.004 s] Raw data (loadavg): 1.04 1.02 0.93 2/55 3122 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9397 0 0 0 10954 45 0 0 25 0 1 0 357746392 41349120 8819 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10095 8819 603 41 0 10054 0 vsize: 40380 [startup+120.004 s] Raw data (loadavg): 1.04 1.02 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9430 0 0 0 11954 46 0 0 25 0 1 0 357746392 41611264 8852 4294967295 134512640 134672761 3221224560 3221222992 134604097 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8852 603 41 0 10118 0 vsize: 40636 [startup+130.004 s] Raw data (loadavg): 1.03 1.02 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9430 0 0 0 12954 46 0 0 25 0 1 0 357746392 41611264 8852 4294967295 134512640 134672761 3221224560 3221223008 134644008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8852 603 41 0 10118 0 vsize: 40636 [startup+140.005 s] Raw data (loadavg): 1.02 1.02 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9435 0 0 0 13954 46 0 0 25 0 1 0 357746392 41611264 8857 4294967295 134512640 134672761 3221224560 3221223056 134644235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8857 603 41 0 10118 0 vsize: 40636 [startup+150.005 s] Raw data (loadavg): 1.02 1.02 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9437 0 0 0 14954 46 0 0 25 0 1 0 357746392 41611264 8859 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8859 603 41 0 10118 0 vsize: 40636 [startup+160.006 s] Raw data (loadavg): 1.02 1.02 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9439 0 0 0 15954 46 0 0 25 0 1 0 357746392 41611264 8861 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8861 603 41 0 10118 0 vsize: 40636 [startup+170.005 s] Raw data (loadavg): 1.01 1.02 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9441 0 0 0 16954 46 0 0 25 0 1 0 357746392 41611264 8863 4294967295 134512640 134672761 3221224560 3221222984 1075353072 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8863 603 41 0 10118 0 vsize: 40636 [startup+180.006 s] Raw data (loadavg): 1.01 1.02 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9443 0 0 0 17954 46 0 0 25 0 1 0 357746392 41611264 8865 4294967295 134512640 134672761 3221224560 3221223072 134606994 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8865 603 41 0 10118 0 vsize: 40636 [startup+190.006 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9446 0 0 0 18954 46 0 0 25 0 1 0 357746392 41611264 8868 4294967295 134512640 134672761 3221224560 3221223056 134644246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8868 603 41 0 10118 0 vsize: 40636 [startup+200.005 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9449 0 0 0 19954 47 0 0 25 0 1 0 357746392 41611264 8871 4294967295 134512640 134672761 3221224560 3221223088 134606977 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8871 603 41 0 10118 0 vsize: 40636 [startup+210.006 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9452 0 0 0 20954 47 0 0 25 0 1 0 357746392 41611264 8874 4294967295 134512640 134672761 3221224560 3221222992 134604052 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8874 603 41 0 10118 0 vsize: 40636 [startup+220.007 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9455 0 0 0 21954 47 0 0 25 0 1 0 357746392 41611264 8877 4294967295 134512640 134672761 3221224560 3221223152 134607861 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10159 8877 603 41 0 10118 0 vsize: 40636 [startup+230.007 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9479 0 0 0 22954 47 0 0 25 0 1 0 357746392 41619456 8855 4294967295 134512640 134672761 3221224560 3221223008 134643996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10161 8855 603 41 0 10120 0 vsize: 40644 [startup+240.007 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9479 0 0 0 23954 47 0 0 25 0 1 0 357746392 41619456 8855 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10161 8855 603 41 0 10120 0 vsize: 40644 [startup+250.007 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 24953 48 0 0 25 0 1 0 357746392 42532864 9106 4294967295 134512640 134672761 3221224560 3221223024 134644240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10384 9106 603 41 0 10343 0 vsize: 41536 [startup+260.007 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 25953 48 0 0 25 0 1 0 357746392 42532864 9106 4294967295 134512640 134672761 3221224560 3221223056 134606420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10384 9106 603 41 0 10343 0 vsize: 41536 [startup+270.007 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 26953 49 0 0 25 0 1 0 357746392 42532864 9106 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10384 9106 603 41 0 10343 0 vsize: 41536 [startup+280.008 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 27953 49 0 0 25 0 1 0 357746392 41226240 8814 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10065 8814 603 41 0 10024 0 vsize: 40260 [startup+290.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 9776 0 0 0 28953 49 0 0 25 0 1 0 357746392 41226240 8814 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10065 8814 603 41 0 10024 0 vsize: 40260 [startup+300.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 10076 0 0 0 29952 50 0 0 25 0 1 0 357746392 42536960 9114 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10385 9114 603 41 0 10344 0 vsize: 41540 [startup+310.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 30932 70 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134643719 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11471 10311 603 41 0 11430 0 vsize: 45884 [startup+320.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 31838 138 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221222840 1075353072 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11471 10311 603 41 0 11430 0 vsize: 45884 [startup+330.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 32838 139 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11471 10311 603 41 0 11430 0 vsize: 45884 [startup+340.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 33838 139 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11471 10311 603 41 0 11430 0 vsize: 45884 [startup+350.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13006 0 0 0 34838 139 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11471 10311 603 41 0 11430 0 vsize: 45884 [startup+360.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13298 0 0 0 35837 140 0 0 25 0 1 0 357746392 49004544 10603 4294967295 134512640 134672761 3221224560 3221222252 134566513 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11964 10603 603 41 0 11923 0 vsize: 47856 [startup+370.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13298 0 0 0 36837 140 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11471 10311 603 41 0 11430 0 vsize: 45884 [startup+380.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13298 0 0 0 37837 140 0 0 25 0 1 0 357746392 46985216 10311 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11471 10311 603 41 0 11430 0 vsize: 45884 [startup+390.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 13620 0 0 0 38836 141 0 0 25 0 1 0 357746392 48365568 10633 4294967295 134512640 134672761 3221224560 3221223600 134613809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11808 10633 603 41 0 11767 0 vsize: 47232 [startup+400.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 14430 0 0 0 39833 144 0 0 25 0 1 0 357746392 51757056 11443 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12636 11443 603 41 0 12595 0 vsize: 50544 [startup+410.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 15420 0 0 0 40831 147 0 0 25 0 1 0 357746392 55787520 12433 4294967295 134512640 134672761 3221224560 3221223760 134610694 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13620 12433 603 41 0 13579 0 vsize: 54480 [startup+420.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 16402 0 0 0 41829 149 0 0 25 0 1 0 357746392 59817984 13415 4294967295 134512640 134672761 3221224560 3221223472 134644251 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14604 13415 603 41 0 14563 0 vsize: 58416 [startup+430.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 16965 0 0 0 42828 150 0 0 25 0 1 0 357746392 62132224 13978 4294967295 134512640 134672761 3221224560 3221223696 134614513 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15169 13978 603 41 0 15128 0 vsize: 60676 [startup+440.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 17625 0 0 0 43826 151 0 0 25 0 1 0 357746392 64864256 14638 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15836 14638 603 41 0 15795 0 vsize: 63344 [startup+450.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 18449 0 0 0 44824 153 0 0 25 0 1 0 357746392 68161536 15462 4294967295 134512640 134672761 3221224560 3221223704 134616183 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16641 15462 603 41 0 16600 0 vsize: 66564 [startup+460.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 18876 0 0 0 45824 154 0 0 25 0 1 0 357746392 69873664 15889 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17059 15889 603 41 0 17018 0 vsize: 68236 [startup+470.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 21803 0 0 0 46802 176 0 0 25 0 1 0 357746392 75255808 17080 4294967295 134512640 134672761 3221224560 3221223104 134621095 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18373 17080 603 41 0 18332 0 vsize: 73492 [startup+480.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 21815 0 0 0 47790 188 0 0 25 0 1 0 357746392 73490432 16789 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17942 16789 603 41 0 17901 0 vsize: 71768 [startup+490.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 21815 0 0 0 48790 188 0 0 25 0 1 0 357746392 73490432 16789 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17942 16789 603 41 0 17901 0 vsize: 71768 [startup+500.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24084 0 0 0 49766 213 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223232 134631080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19359 17095 603 41 0 19318 0 vsize: 77436 [startup+510.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24117 0 0 0 50677 275 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643963 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19359 17095 603 41 0 19318 0 vsize: 77436 [startup+520.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24117 0 0 0 51678 275 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643959 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19359 17095 603 41 0 19318 0 vsize: 77436 [startup+530.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24117 0 0 0 52678 275 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19359 17095 603 41 0 19318 0 vsize: 77436 [startup+540.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24408 0 0 0 53677 276 0 0 25 0 1 0 357746392 81244160 17386 4294967295 134512640 134672761 3221224560 3221223024 134644246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19835 17386 603 41 0 19794 0 vsize: 79340 [startup+550.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24408 0 0 0 54677 276 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643516 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19359 17095 603 41 0 19318 0 vsize: 77436 [startup+560.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24408 0 0 0 55677 276 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223008 134643556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19359 17095 603 41 0 19318 0 vsize: 77436 [startup+570.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24408 0 0 0 56677 277 0 0 25 0 1 0 357746392 79294464 17095 4294967295 134512640 134672761 3221224560 3221223648 1074743855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19359 17095 603 41 0 19318 0 vsize: 77436 [startup+580.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24410 0 0 0 57677 277 0 0 25 0 1 0 357746392 79294464 17097 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19359 17097 603 41 0 19318 0 vsize: 77436 [startup+590.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 24412 0 0 0 58677 277 0 0 25 0 1 0 357746392 79294464 17099 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19359 17099 603 41 0 19318 0 vsize: 77436 [startup+600.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26820 0 0 0 59643 311 0 0 25 0 1 0 357746392 81489920 17437 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19895 17437 603 41 0 19854 0 vsize: 79580 [startup+610.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26820 0 0 0 60643 311 0 0 25 0 1 0 357746392 79466496 17145 4294967295 134512640 134672761 3221224560 3221223008 134643987 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19401 17145 603 41 0 19360 0 vsize: 77604 [startup+620.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26821 0 0 0 61643 311 0 0 25 0 1 0 357746392 79466496 17146 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19401 17146 603 41 0 19360 0 vsize: 77604 [startup+630.013 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26822 0 0 0 62643 311 0 0 25 0 1 0 357746392 79466496 17147 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19401 17147 603 41 0 19360 0 vsize: 77604 [startup+640.013 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 26991 0 0 0 63642 312 0 0 25 0 1 0 357746392 80388096 17316 4294967295 134512640 134672761 3221224560 3221223504 134606869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19626 17316 603 41 0 19585 0 vsize: 78504 [startup+650.013 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 27518 0 0 0 64641 313 0 0 25 0 1 0 357746392 82501632 17843 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20142 17843 603 41 0 20101 0 vsize: 80568 [startup+660.014 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 28356 0 0 0 65641 314 0 0 25 0 1 0 357746392 85876736 18681 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20966 18681 603 41 0 20925 0 vsize: 83864 [startup+670.013 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 28888 0 0 0 66639 315 0 0 25 0 1 0 357746392 88088576 19213 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21506 19213 603 41 0 21465 0 vsize: 86024 [startup+680.014 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 29639 0 0 0 67638 317 0 0 25 0 1 0 357746392 91160576 19964 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22256 19964 603 41 0 22215 0 vsize: 89024 [startup+690.014 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 30510 0 0 0 68636 319 0 0 25 0 1 0 357746392 94679040 20835 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23115 20835 603 41 0 23074 0 vsize: 92460 [startup+700.014 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 31133 0 0 0 69635 320 0 0 25 0 1 0 357746392 97280000 21458 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23750 21458 603 41 0 23709 0 vsize: 95000 [startup+710.014 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 31804 0 0 0 70634 321 0 0 25 0 1 0 357746392 99966976 22129 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24406 22129 603 41 0 24365 0 vsize: 97624 [startup+720.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 32384 0 0 0 71632 323 0 0 25 0 1 0 357746392 102412288 22709 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25003 22709 603 41 0 24962 0 vsize: 100012 [startup+730.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 32766 0 0 0 72630 325 0 0 25 0 1 0 357746392 103968768 23091 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25383 23091 603 41 0 25342 0 vsize: 101532 [startup+740.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 33393 0 0 0 73630 326 0 0 25 0 1 0 357746392 106455040 23718 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25990 23718 603 41 0 25949 0 vsize: 103960 [startup+750.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 33834 0 0 0 74629 327 0 0 25 0 1 0 357746392 108355584 24159 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26454 24159 603 41 0 26413 0 vsize: 105816 [startup+760.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 34194 0 0 0 75628 328 0 0 25 0 1 0 357746392 109801472 24519 4294967295 134512640 134672761 3221224560 3221223704 134616275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26807 24519 603 41 0 26766 0 vsize: 107228 [startup+770.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 34549 0 0 0 76628 328 0 0 25 0 1 0 357746392 111235072 24874 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27157 24874 603 41 0 27116 0 vsize: 108628 [startup+780.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 35204 0 0 0 77627 330 0 0 25 0 1 0 357746392 113946624 25529 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27819 25529 603 41 0 27778 0 vsize: 111276 [startup+790.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 35699 0 0 0 78626 330 0 0 25 0 1 0 357746392 115871744 26024 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28289 26024 603 41 0 28248 0 vsize: 113156 [startup+800.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 36177 0 0 0 79626 331 0 0 25 0 1 0 357746392 117911552 26502 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28787 26502 603 41 0 28746 0 vsize: 115148 [startup+810.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 36734 0 0 0 80625 332 0 0 25 0 1 0 357746392 120123392 27059 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29327 27059 603 41 0 29286 0 vsize: 117308 [startup+820.017 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 37346 0 0 0 81624 334 0 0 25 0 1 0 357746392 122654720 27671 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29945 27671 603 41 0 29904 0 vsize: 119780 [startup+830.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 37876 0 0 0 82623 335 0 0 25 0 1 0 357746392 124751872 28201 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30457 28201 603 41 0 30416 0 vsize: 121828 [startup+840.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 38305 0 0 0 83622 336 0 0 25 0 1 0 357746392 126590976 28630 4294967295 134512640 134672761 3221224560 3221223716 134614480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30906 28630 603 41 0 30865 0 vsize: 123624 [startup+850.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 38989 0 0 0 84620 337 0 0 25 0 1 0 357746392 129331200 29314 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31575 29314 603 41 0 31534 0 vsize: 126300 [startup+860.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 39409 0 0 0 85619 338 0 0 25 0 1 0 357746392 131284992 29734 4294967295 134512640 134672761 3221224560 3221223704 134616123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32052 29734 603 41 0 32011 0 vsize: 128208 [startup+870.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 39777 0 0 0 86619 339 0 0 25 0 1 0 357746392 132820992 30102 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32427 30102 603 41 0 32386 0 vsize: 129708 [startup+880.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 40530 0 0 0 87617 341 0 0 25 0 1 0 357746392 135901184 30855 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33179 30855 603 41 0 33138 0 vsize: 132716 [startup+890.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 41036 0 0 0 88616 342 0 0 25 0 1 0 357746392 137990144 31361 4294967295 134512640 134672761 3221224560 3221223712 134565064 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33689 31361 603 41 0 33648 0 vsize: 134756 [startup+900.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 41672 0 0 0 89614 344 0 0 25 0 1 0 357746392 140591104 31997 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34324 31997 603 41 0 34283 0 vsize: 137296 [startup+910.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 41994 0 0 0 90614 345 0 0 25 0 1 0 357746392 141905920 32319 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34645 32319 603 41 0 34604 0 vsize: 138580 [startup+920.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 42661 0 0 0 91613 346 0 0 25 0 1 0 357746392 144642048 32986 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35313 32986 603 41 0 35272 0 vsize: 141252 [startup+930.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 43326 0 0 0 92611 348 0 0 25 0 1 0 357746392 147341312 33651 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35972 33651 603 41 0 35931 0 vsize: 143888 [startup+940.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 43934 0 0 0 93610 349 0 0 25 0 1 0 357746392 149803008 34259 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36573 34259 603 41 0 36532 0 vsize: 146292 [startup+950.014 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 44339 0 0 0 94610 350 0 0 25 0 1 0 357746392 151486464 34664 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36984 34664 603 41 0 36943 0 vsize: 147936 [startup+960.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 44750 0 0 0 95609 350 0 0 25 0 1 0 357746392 153165824 35075 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37394 35075 603 41 0 37353 0 vsize: 149576 [startup+970.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 45429 0 0 0 96608 352 0 0 25 0 1 0 357746392 155906048 35754 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38063 35754 603 41 0 38022 0 vsize: 152252 [startup+980.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 45770 0 0 0 97607 352 0 0 25 0 1 0 357746392 157339648 36095 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38413 36095 603 41 0 38372 0 vsize: 153652 [startup+990.014 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 46269 0 0 0 98606 354 0 0 25 0 1 0 357746392 159313920 36594 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38895 36594 603 41 0 38854 0 vsize: 155580 [startup+1000.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 46487 0 0 0 99605 355 0 0 25 0 1 0 357746392 160206848 36812 4294967295 134512640 134672761 3221224560 3221223744 134615788 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39113 36812 603 41 0 39072 0 vsize: 156452 [startup+1010.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 47127 0 0 0 100603 357 0 0 25 0 1 0 357746392 162824192 37452 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39752 37452 603 41 0 39711 0 vsize: 159008 [startup+1020.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 47787 0 0 0 101602 359 0 0 25 0 1 0 357746392 165617664 38112 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 40434 38112 603 41 0 40393 0 vsize: 161736 [startup+1030.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 48125 0 0 0 102601 360 0 0 25 0 1 0 357746392 166899712 38450 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 40747 38450 603 41 0 40706 0 vsize: 162988 [startup+1040.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 48561 0 0 0 103600 361 0 0 25 0 1 0 357746392 168693760 38886 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41185 38886 603 41 0 41144 0 vsize: 164740 [startup+1050.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 48730 0 0 0 104599 361 0 0 25 0 1 0 357746392 169472000 39055 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41375 39055 603 41 0 41334 0 vsize: 165500 [startup+1060.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 49025 0 0 0 105599 362 0 0 25 0 1 0 357746392 170618880 39350 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41655 39350 603 41 0 41614 0 vsize: 166620 [startup+1070.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 49388 0 0 0 106598 363 0 0 25 0 1 0 357746392 172171264 39713 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 42034 39713 603 41 0 41993 0 vsize: 168136 [startup+1080.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 49882 0 0 0 107597 364 0 0 25 0 1 0 357746392 174125056 40207 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 42511 40207 603 41 0 42470 0 vsize: 170044 [startup+1090.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 50329 0 0 0 108596 365 0 0 25 0 1 0 357746392 175947776 40654 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 42956 40654 603 41 0 42915 0 vsize: 171824 [startup+1100.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 50673 0 0 0 109596 366 0 0 25 0 1 0 357746392 177307648 40998 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 43288 40998 603 41 0 43247 0 vsize: 173152 [startup+1110.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 51012 0 0 0 110595 367 0 0 25 0 1 0 357746392 178745344 41337 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 43639 41337 603 41 0 43598 0 vsize: 174556 [startup+1120.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 51353 0 0 0 111595 367 0 0 25 0 1 0 357746392 180183040 41678 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 43990 41678 603 41 0 43949 0 vsize: 175960 [startup+1130.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 51589 0 0 0 112594 368 0 0 25 0 1 0 357746392 181100544 41914 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 44214 41914 603 41 0 44173 0 vsize: 176856 [startup+1140.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 51909 0 0 0 113594 369 0 0 25 0 1 0 357746392 182386688 42234 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 44528 42234 603 41 0 44487 0 vsize: 178112 [startup+1150.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 52248 0 0 0 114593 369 0 0 25 0 1 0 357746392 183808000 42573 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 44875 42573 603 41 0 44834 0 vsize: 179500 [startup+1160.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 52568 0 0 0 115593 370 0 0 25 0 1 0 357746392 185126912 42893 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 45197 42893 603 41 0 45156 0 vsize: 180788 [startup+1170.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 52881 0 0 0 116592 371 0 0 25 0 1 0 357746392 186417152 43206 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 45512 43206 603 41 0 45471 0 vsize: 182048 [startup+1180.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 53356 0 0 0 117591 372 0 0 25 0 1 0 357746392 188358656 43681 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 45986 43681 603 41 0 45945 0 vsize: 183944 [startup+1190.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 53956 0 0 0 118590 373 0 0 25 0 1 0 357746392 190803968 44281 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 46583 44281 603 41 0 46542 0 vsize: 186332 [startup+1200.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 54293 0 0 0 119589 374 0 0 25 0 1 0 357746392 192212992 44618 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 46927 44618 603 41 0 46886 0 vsize: 187708 [startup+1210.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 3124 Raw data (stat): 3122 (minisat+) R 3121 30927 30926 0 -1 0 54585 0 0 0 120589 374 0 0 25 0 1 0 357746392 193376256 44910 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 47211 44910 603 41 0 47170 0 vsize: 188844 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1210.18 s] Raw data (loadavg): 1.00 1.00 0.93 1/55 3124 Raw data (stat): 3122 (minisat+) Z 3121 30927 30926 0 -1 12 54586 0 0 0 120589 391 0 0 25 0 1 0 357746392 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1210.18 CPU time (s): 1209.81 CPU user time (s): 1205.9 CPU system time (s): 3.91341 CPU usage (%): 99.9696 Max. virtual memory (Kb): 188844 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####