Name | normalized-opb/mps-v2-13-7/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-13-7-nazareth.opb |
MD5SUM | 25b0f49e8e3ab43f9f405cabc9317ea8 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -1048575 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 55 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 3162109 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 5244800 |
Number of bits of the biggest number in a constraint | 23 |
Biggest sum of numbers in a constraint | 19924855 |
Number of bits of the biggest sum of numbers | 25 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.008998 |
Number of variables | 55 |
Total number of constraints | 3 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 3 |
Minimum length of a constraint | 14 |
Maximum length of a constraint | 41 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-04-20 21:56:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=20397 boxname=wulflinc22 idbench=1569 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 25b0f49e8e3ab43f9f405cabc9317ea8 /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-nazareth.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-nazareth.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-nazareth.opb IDLAUNCH: 20397 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 470872 kB Buffers: 35960 kB Cached: 481972 kB SwapCached: 3696 kB Active: 177032 kB Inactive: 347400 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 470620 kB SwapTotal: 2097892 kB SwapFree: 2094184 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 33788 kB Committed_AS: 63488 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-20 21:56:02 (client local time) WITH STATUS 30 IN 0.430933 SECONDS stats: 20397 0 0.430933 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 3 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 2]---> BDD-cost: 13 c ---[ 1]---> BDD-cost: 157 c ---[ 0]---> Sorter-cost: 439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1757 4394 | 585 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 134488[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 392 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 2817 6902 | 939 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 16382[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3 | 2883 7072 | 961 3 10 3.3 | 0.000 % | c ============================================================================== c [1mFound solution: 16380[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7 | 2909 7144 | 969 7 27 3.9 | 0.000 % | c ============================================================================== c [1mFound solution: 8187[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10 | 2935 7214 | 978 10 37 3.7 | 0.000 % | c ============================================================================== c [1mFound solution: -13072[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 47 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13 | 2967 7302 | 989 13 44 3.4 | 0.000 % | c ============================================================================== c [1mFound solution: -717317[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 40 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17 | 2959 7290 | 986 16 56 3.5 | 0.000 % | c ============================================================================== c [1mFound solution: -790658[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 41 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17 | 2912 7188 | 970 16 56 3.5 | 0.000 % | c ============================================================================== c [1mFound solution: -828040[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20 | 2937 7251 | 979 19 70 3.7 | 0.000 % | c ============================================================================== c [1mFound solution: -839942[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23 | 2979 7356 | 993 22 84 3.8 | 0.000 % | c ============================================================================== c [1mFound solution: -864515[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28 | 3010 7435 | 1003 27 102 3.8 | 0.000 % | c ============================================================================== c [1mFound solution: -865044[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29 | 3042 7515 | 1014 28 104 3.7 | 0.000 % | c ============================================================================== c [1mFound solution: -893192[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31 | 3061 7564 | 1020 30 117 3.9 | 0.000 % | c ============================================================================== c [1mFound solution: -895763[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32 | 3093 7644 | 1031 31 123 4.0 | 0.000 % | c ============================================================================== c [1mFound solution: -897285[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32 | 3116 7705 | 1038 31 123 4.0 | 0.000 % | c ============================================================================== c [1mFound solution: -897286[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33 | 3123 7724 | 1041 32 128 4.0 | 0.000 % | c ============================================================================== c [1mFound solution: -899331[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34 | 3136 7759 | 1045 33 144 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -899859[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35 | 3144 7781 | 1048 34 147 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -899860[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36 | 3156 7813 | 1052 35 150 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -899861[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38 | 3183 7882 | 1061 37 157 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -899875[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38 | 3209 7948 | 1069 37 157 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -899876[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 38 | 3235 8014 | 1078 37 157 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -899877[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39 | 3261 8080 | 1087 38 161 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -946963[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 36 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 42 | 3189 7921 | 1063 38 165 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -947987[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 44 | 3214 7982 | 1071 40 173 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -960019[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 44 | 3231 8025 | 1077 40 173 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -964115[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 44 | 3241 8051 | 1080 40 173 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -964117[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 44 | 3258 8094 | 1086 40 173 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -966163[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 47 | 3266 8116 | 1088 43 183 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -992787[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 32 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 47 | 3152 7852 | 1050 39 164 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -992789[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49 | 3168 7892 | 1056 41 170 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1009171[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 50 | 3175 7909 | 1058 42 174 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1025555[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 54 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 52 | 3119 7785 | 1039 40 167 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1033747[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 65 | 2962 7421 | 987 50 224 4.5 | 0.000 % | c ============================================================================== c [1mFound solution: -1034003[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 65 | 2969 7438 | 989 50 224 4.5 | 0.000 % | c ============================================================================== c [1mFound solution: -1034005[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 65 | 2980 7465 | 993 50 224 4.5 | 0.000 % | c ============================================================================== c [1mFound solution: -1034019[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 65 | 2991 7492 | 997 50 224 4.5 | 0.000 % | c ============================================================================== c [1mFound solution: -1034021[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 65 | 3002 7519 | 1000 50 224 4.5 | 0.000 % | c ============================================================================== c [1mFound solution: -1034195[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 66 | 3020 7565 | 1006 51 233 4.6 | 0.000 % | c ============================================================================== c [1mFound solution: -1034198[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 67 | 3044 7625 | 1014 52 243 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1034199[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 68 | 3071 7692 | 1023 53 248 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1035462[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69 | 3094 7749 | 1031 54 252 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1035478[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69 | 3113 7796 | 1037 54 252 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1035479[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69 | 3132 7843 | 1044 54 252 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1035494[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69 | 3155 7900 | 1051 54 252 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1035495[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69 | 3178 7957 | 1059 54 252 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1035510[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 71 | 3198 8007 | 1066 56 263 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1035511[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 72 | 3218 8057 | 1072 57 268 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1035974[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 72 | 3233 8094 | 1077 57 268 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1035975[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 75 | 3255 8148 | 1085 60 287 4.8 | 0.000 % | c ============================================================================== c [1mFound solution: -1036186[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 83 | 3280 8211 | 1093 68 324 4.8 | 0.000 % | c ============================================================================== c [1mFound solution: -1037847[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 85 | 3297 8254 | 1099 70 329 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1037851[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 85 | 3322 8317 | 1107 70 329 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1037879[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86 | 3342 8367 | 1114 71 336 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1038231[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86 | 3359 8410 | 1119 71 336 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1038239[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86 | 3381 8466 | 1127 71 336 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1038240[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86 | 3402 8519 | 1134 71 336 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1038743[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 88 | 3416 8555 | 1138 73 347 4.8 | 0.000 % | c ============================================================================== c [1mFound solution: -1038839[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 90 | 3429 8588 | 1143 75 353 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1039351[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 90 | 3441 8618 | 1147 75 353 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1039359[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 115 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 90 | 3959 10076 | 1319 75 353 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1041399[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 102 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 108 | 4238 10954 | 1412 79 372 4.7 | 0.000 % | c ============================================================================== c [1mFound solution: -1041402[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 174 | 4253 10993 | 1417 145 647 4.5 | 0.000 % | c ============================================================================== c [1mFound solution: -1044410[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 178 | 4268 11032 | 1422 149 659 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1044411[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 112 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 180 | 4778 12486 | 1592 151 665 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1046458[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 197 | 4342 11369 | 1447 164 720 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1046459[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 208 | 4343 11370 | 1447 169 752 4.4 | 0.000 % | c ============================================================================== c [1mFound solution: -1047420[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 222 | 4040 10561 | 1346 162 701 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1047483[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 227 | 4046 10577 | 1348 167 723 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1047995[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 233 | 3580 9367 | 1193 162 693 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1048243[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 52 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 239 | 3394 8936 | 1131 150 641 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1048251[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 243 | 3385 8911 | 1128 147 631 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: -1048379[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 245 | 2988 7878 | 996 134 562 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1048435[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 245 | 3018 7962 | 1006 134 562 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1048443[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 245 | 3048 8046 | 1016 134 562 4.2 | 0.000 % | c ============================================================================== c [1mFound solution: -1048499[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 0 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 249 | 2584 6816 | 861 123 499 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1048507[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 0 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 250 | 2536 6685 | 845 116 477 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1048531[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 250 | 2104 5540 | 701 101 411 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1048539[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 250 | 2110 5556 | 703 101 411 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1048563[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 0 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 250 | 1207 3162 | 402 58 238 4.1 | 0.000 % | c ============================================================================== c [1mFound solution: -1048571[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 0 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 250 | 563 1480 | 187 9 32 3.6 | 0.000 % | c ============================================================================== c [1mFound solution: -1048572[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 250 | 587 1546 | 195 9 32 3.6 | 0.000 % | c ============================================================================== c [1mFound solution: -1048573[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 0 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 250 | 153 405 | 51 2 8 4.0 | 0.000 % | c ============================================================================== c [1mFound solution: -1048574[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 251 | 0 0 | 0 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -1048575[0m c [1mOptimal solution: -1048575[0m s OPTIMUM FOUND v -CLNAM1_bit_7 -CLNAM1_bit_6 -CLNAM1_bit_5 -CLNAM1_bit_4 -CLNAM1_bit_3 -CLNAM1_bit_2 -CLNAM1_bit_1 -CLNAM1_bit0 -CLNAM1_bit1 -CLNAM1_bit2 -CLNAM1_bit3 -CLNAM1_bit4 -CLNAM1_bit5 -CLNAM1_bit6 CLNAM2_bit_7 CLNAM2_bit_6 CLNAM2_bit_5 CLNAM2_bit_4 CLNAM2_bit_3 CLNAM2_bit_2 CLNAM2_bit_1 CLNAM2_bit0 CLNAM2_bit1 CLNAM2_bit2 CLNAM2_bit3 CLNAM2_bit4 CLNAM2_bit5 CLNAM2_bit6 CLNAM2_bit7 CLNAM2_bit8 CLNAM2_bit9 CLNAM2_bit10 CLNAM2_bit11 CLNAM2_bit12 -CLNAM3_bit_7 -CLNAM3_bit_6 -CLNAM3_bit_5 -CLNAM3_bit_4 -CLNAM3_bit_3 -CLNAM3_bit_2 -CLNAM3_bit_1 -CLNAM3_bit0 -CLNAM3_bit1 -CLNAM3_bit2 -CLNAM3_bit3 -CLNAM3_bit4 -CLNAM3_bit5 -CLNAM3_bit6 -CLNAM3_bit7 -CLNAM3_bit8 -CLNAM3_bit9 -CLNAM3_bit10 -CLNAM3_bit11 -CLNAM3_bit12 -CLNAM3_bit13 c _______________________________________________________________________________ c c restarts : 84 c conflicts : 251 (605 /sec) c decisions : 3718 (8960 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 0.414936 s 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): 0.72 0.92 0.89 2/54 21370 Raw data (stat): 21370 (runsolver) R 21369 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539844195 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+0.443199 s] Raw data (loadavg): 0.72 0.92 0.89 1/53 21370 Raw data (stat): 21370 (runsolver) R 21369 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539844195 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 0 Child status: 30 Real time (s): 0.44291 CPU time (s): 0.430933 CPU user time (s): 0.415936 CPU system time (s): 0.014997 CPU usage (%): 97.2958 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK -1048575 #### END VERIFIER DATA ####