Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare2.opb |
MD5SUM | 111dddb6adf389a5275ab413feff6076 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 429056 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 210 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 7516192761 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 7516192761 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1201.36 |
Number of variables | 270 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 7 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 90 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-05-27 07:32:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23397 boxname=wulflinc22 idbench=1041 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 111dddb6adf389a5275ab413feff6076 /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-markshare2.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-markshare2.opb IDLAUNCH: 23397 /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: 883092 kB Buffers: 33356 kB Cached: 96072 kB SwapCached: 384 kB Active: 23148 kB Inactive: 108568 kB HighTotal: 131008 kB HighFree: 57848 kB LowTotal: 903652 kB LowFree: 825244 kB SwapTotal: 2097892 kB SwapFree: 2096800 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5532 kB Slab: 14136 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 07:53:00 (client local time) WITH STATUS 152 IN 1229.88 SECONDS stats: 23397 7 1229.88 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 14 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 12]---> BDD-cost:33300 c ---[ 10]---> BDD-cost:39181 c ---[ 8]---> BDD-cost:34989 c ---[ 6]---> BDD-cost:41590 c ---[ 4]---> BDD-cost:41670 c ---[ 2]---> BDD-cost:41238 c ---[ 0]---> BDD-cost:35327 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 774421 2270408 | 258140 0 0 nan | 0.000 % | c | 100 | 774421 2270408 | 283954 100 10529 105.3 | 0.026 % | c ============================================================================== c [1mFound solution: 8321024[0m c ---[ 0]---> Sorter-cost: 2158 Base: 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 | 101 | 779941 2283300 | 259980 101 10563 104.6 | 0.026 % | c ============================================================================== c [1mFound solution: 8070144[0m c ---[ 0]---> Sorter-cost: 12 Base: 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 | 103 | 779972 2283416 | 259990 103 10593 102.8 | 0.026 % | c ============================================================================== c [1mFound solution: 7919616[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 103 | 779984 2283446 | 259994 103 10593 102.8 | 0.026 % | c ============================================================================== c [1mFound solution: 7883776[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 103 | 779998 2283478 | 259999 103 10593 102.8 | 0.026 % | c ============================================================================== c [1mFound solution: 7766016[0m c ---[ 0]---> Sorter-cost: 11 Base: 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 | 195 | 780011 2283508 | 260003 195 17056 87.5 | 0.026 % | c ============================================================================== c [1mFound solution: 7600128[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 195 | 780017 2283523 | 260005 195 17056 87.5 | 0.026 % | c ============================================================================== c [1mFound solution: 7581696[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 210 | 780028 2283551 | 260009 210 17898 85.2 | 0.026 % | c ============================================================================== c [1mFound solution: 7541760[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 289 | 780041 2283581 | 260013 289 22921 79.3 | 0.026 % | c | 389 | 780041 2283581 | 286014 389 28159 72.4 | 0.029 % | c | 542 | 780041 2283581 | 314615 542 36432 67.2 | 0.029 % | c ============================================================================== c [1mFound solution: 7353344[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 611 | 780051 2283603 | 260017 611 40926 67.0 | 0.029 % | c | 711 | 780051 2283603 | 286018 711 45549 64.1 | 0.029 % | c | 861 | 780051 2283603 | 314620 861 53044 61.6 | 0.029 % | c | 1088 | 780051 2283603 | 346082 1088 68036 62.5 | 0.029 % | c | 1425 | 780051 2283603 | 380690 1425 89057 62.5 | 0.029 % | c ============================================================================== c [1mFound solution: 7134208[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 1552 | 780074 2283662 | 260024 1552 96231 62.0 | 0.029 % | c ============================================================================== c [1mFound solution: 7091200[0m c ---[ 0]---> Sorter-cost: 4 Base: 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 | 1588 | 780084 2283688 | 260028 1588 98169 61.8 | 0.029 % | c ============================================================================== c [1mFound solution: 6865920[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 1629 | 780095 2283714 | 260031 1629 100375 61.6 | 0.029 % | c | 1730 | 780095 2283714 | 286034 1730 105382 60.9 | 0.030 % | c ============================================================================== c [1mFound solution: 6863872[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 1870 | 780107 2283742 | 260035 1870 113202 60.5 | 0.030 % | c | 1970 | 780107 2283742 | 286038 1970 117506 59.6 | 0.031 % | c | 2120 | 780107 2283742 | 314642 2120 124851 58.9 | 0.031 % | c ============================================================================== c [1mFound solution: 6833152[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 2280 | 780117 2283765 | 260039 2280 133876 58.7 | 0.031 % | c | 2380 | 780117 2283765 | 286042 2380 138500 58.2 | 0.031 % | c | 2530 | 780117 2283765 | 314647 2530 147991 58.5 | 0.031 % | c | 2755 | 780117 2283765 | 346111 2755 162068 58.8 | 0.031 % | c ============================================================================== c [1mFound solution: 6819840[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 3070 | 780129 2283792 | 260043 3070 178746 58.2 | 0.031 % | c ============================================================================== c [1mFound solution: 6724608[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 3123 | 780139 2283816 | 260046 3123 181367 58.1 | 0.031 % | c | 3223 | 780139 2283816 | 286050 3223 188180 58.4 | 0.032 % | c | 3374 | 780139 2283816 | 314655 3374 196412 58.2 | 0.032 % | c ============================================================================== c [1mFound solution: 6516736[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 3454 | 780148 2283838 | 260049 3454 201541 58.4 | 0.032 % | c ============================================================================== c [1mFound solution: 6364160[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 3517 | 780157 2283858 | 260052 3517 205162 58.3 | 0.032 % | c | 3618 | 780157 2283858 | 286057 3618 211177 58.4 | 0.033 % | c | 3769 | 780157 2283858 | 314662 3769 217893 57.8 | 0.033 % | c | 3994 | 780157 2283858 | 346129 3994 227695 57.0 | 0.033 % | c ============================================================================== c [1mFound solution: 6243328[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 4031 | 780166 2283883 | 260055 4031 229780 57.0 | 0.033 % | c | 4131 | 780166 2283883 | 286060 4131 234574 56.8 | 0.033 % | c | 4285 | 780166 2283883 | 314666 4285 242550 56.6 | 0.033 % | c ============================================================================== c [1mFound solution: 5986304[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 4421 | 780176 2283908 | 260058 4421 249628 56.5 | 0.033 % | c | 4521 | 780176 2283908 | 286063 4521 255299 56.5 | 0.033 % | c | 4672 | 780176 2283908 | 314670 4672 264929 56.7 | 0.033 % | c ============================================================================== c [1mFound solution: 5938176[0m c ---[ 0]---> Sorter-cost: 4 Base: 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 | 4877 | 780183 2283925 | 260061 4877 273374 56.1 | 0.033 % | c | 4980 | 780183 2283925 | 286067 4980 278523 55.9 | 0.034 % | c ============================================================================== c [1mFound solution: 5903360[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 5049 | 780192 2283946 | 260064 5049 282254 55.9 | 0.034 % | c | 5149 | 780192 2283946 | 286070 5149 287079 55.8 | 0.034 % | c | 5299 | 780192 2283946 | 314677 5299 295239 55.7 | 0.034 % | c ============================================================================== c [1mFound solution: 5857280[0m c ---[ 0]---> Sorter-cost: 9 Base: 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 | 5385 | 780205 2283977 | 260068 5385 300440 55.8 | 0.034 % | c | 5486 | 780205 2283977 | 286074 5486 305598 55.7 | 0.035 % | c | 5636 | 780205 2283977 | 314682 5636 313066 55.5 | 0.035 % | c | 5863 | 780205 2283977 | 346150 5863 324692 55.4 | 0.035 % | c | 6200 | 780205 2283977 | 380765 6200 347453 56.0 | 0.035 % | c ============================================================================== c [1mFound solution: 5834752[0m c ---[ 0]---> Sorter-cost: 10 Base: 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 | 6661 | 780219 2284009 | 260073 6661 378987 56.9 | 0.035 % | c | 6761 | 780219 2284009 | 286080 6761 384193 56.8 | 0.035 % | c | 6911 | 780219 2284009 | 314688 6911 393158 56.9 | 0.035 % | c ============================================================================== c [1mFound solution: 5734400[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 7077 | 780224 2284023 | 260074 7077 402215 56.8 | 0.035 % | c | 7177 | 780224 2284023 | 286081 7177 407628 56.8 | 0.035 % | c | 7328 | 780224 2284023 | 314689 7328 415420 56.7 | 0.035 % | c | 7554 | 780224 2284023 | 346158 7554 427298 56.6 | 0.035 % | c ============================================================================== c [1mFound solution: 5697536[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 7670 | 780232 2284043 | 260077 7670 433847 56.6 | 0.035 % | c | 7770 | 780232 2284043 | 286084 7770 439094 56.5 | 0.036 % | c | 7920 | 780232 2284043 | 314693 7920 447260 56.5 | 0.036 % | c | 8146 | 780232 2284043 | 346162 8146 459809 56.4 | 0.036 % | c ============================================================================== c [1mFound solution: 5468160[0m c ---[ 0]---> Sorter-cost: 2 Base: 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 | 8426 | 780238 2284056 | 260079 8426 473802 56.2 | 0.036 % | c | 8527 | 780238 2284056 | 286086 8527 477769 56.0 | 0.036 % | c | 8677 | 780238 2284056 | 314695 8677 487858 56.2 | 0.036 % | c | 8902 | 780238 2284056 | 346165 8902 499073 56.1 | 0.036 % | c | 9240 | 780238 2284056 | 380781 9240 518923 56.2 | 0.036 % | c | 9746 | 780238 2284056 | 418859 9746 545702 56.0 | 0.036 % | c | 10505 | 780238 2284056 | 460745 10505 592588 56.4 | 0.036 % | c | 11645 | 780238 2284056 | 506820 11645 666340 57.2 | 0.036 % | c ============================================================================== c [1mFound solution: 5413888[0m c ---[ 0]---> Sorter-cost: 3 Base: 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 | 11919 | 780242 2284065 | 260080 11919 681943 57.2 | 0.036 % | c | 12019 | 780242 2284065 | 286088 12019 686729 57.1 | 0.036 % | c | 12169 | 780242 2284065 | 314696 12169 695133 57.1 | 0.036 % | c | 12394 | 780242 2284065 | 346166 12394 708680 57.2 | 0.036 % | c | 12731 | 780242 2284065 | 380783 12731 730101 57.3 | 0.036 % | c | 13238 | 780242 2284065 | 418861 13238 763643 57.7 | 0.036 % | c ============================================================================== c [1mFound solution: 5405696[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 13777 | 780252 2284088 | 260084 13777 795945 57.8 | 0.036 % | c | 13878 | 780252 2284088 | 286092 13878 802651 57.8 | 0.037 % | c ============================================================================== c [1mFound solution: 5364736[0m c ---[ 0]---> Sorter-cost: 6 Base: 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 | 14021 | 780259 2284104 | 260086 14021 812373 57.9 | 0.037 % | c | 14121 | 780259 2284104 | 286094 14121 817922 57.9 | 0.037 % | c | 14273 | 780259 2284104 | 314704 14273 826360 57.9 | 0.037 % | c | 14498 | 780259 2284104 | 346174 14498 838932 57.9 | 0.037 % | c | 14835 | 780259 2284104 | 380791 14835 857354 57.8 | 0.037 % | c ============================================================================== c [1mFound solution: 5243904[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 15330 | 780268 2284123 | 260089 15330 887315 57.9 | 0.037 % | c ============================================================================== c [1mFound solution: 5239808[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 15423 | 780279 2284155 | 260093 15423 893070 57.9 | 0.037 % | c | 15523 | 780279 2284155 | 286102 15523 899973 58.0 | 0.038 % | c | 15673 | 780279 2284155 | 314712 15673 908713 58.0 | 0.038 % | c ============================================================================== c [1mFound solution: 5169152[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 15833 | 780287 2284178 | 260095 15833 916731 57.9 | 0.038 % | c | 15935 | 780287 2284178 | 286104 15935 920864 57.8 | 0.038 % | c | 16086 | 780287 2284178 | 314714 16086 931652 57.9 | 0.038 % | c ============================================================================== c [1mFound solution: 5128192[0m c ---[ 0]---> Sorter-cost: 8 Base: 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 | 16122 | 780297 2284203 | 260099 16122 933881 57.9 | 0.038 % | c | 16222 | 780297 2284203 | 286108 16222 939703 57.9 | 0.039 % | c | 16372 | 780297 2284203 | 314719 16372 946289 57.8 | 0.039 % | c | 16597 | 780297 2284203 | 346191 16597 961057 57.9 | 0.039 % | c ============================================================================== c [1mFound solution: 4799488[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 16734 | 780307 2284226 | 260102 16734 967493 57.8 | 0.039 % | c | 16837 | 780307 2284226 | 286112 16837 971971 57.7 | 0.039 % | c | 16990 | 780307 2284226 | 314723 16990 978660 57.6 | 0.039 % | c | 17215 | 780307 2284226 | 346195 17215 989567 57.5 | 0.039 % | c ============================================================================== c [1mFound solution: 4767744[0m c ---[ 0]---> Sorter-cost: 7 Base: 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 | 17378 | 780316 2284247 | 260105 17378 996586 57.3 | 0.039 % | c | 17478 | 780316 2284247 | 286115 17478 1001832 57.3 | 0.039 % | c | 17629 | 780316 2284247 | 314727 17629 1007314 57.1 | 0.039 % | c | 17856 | 780316 2284247 | 346199 17856 1021289 57.2 | 0.039 % | c | 18193 | 780316 2284247 | 380819 18193 1034294 56.9 | 0.039 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 15849 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.90 0.95 0.92 2/54 15845 Raw data (stat): 15845 (runsolver) R 15844 23310 23309 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854386068 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99996 s] Raw data (loadavg): 0.91 0.95 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.001 s] Raw data (loadavg): 0.93 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0019 s] Raw data (loadavg): 0.94 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0022 s] Raw data (loadavg): 0.95 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0033 s] Raw data (loadavg): 0.95 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0028 s] Raw data (loadavg): 0.96 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0031 s] Raw data (loadavg): 0.97 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0033 s] Raw data (loadavg): 0.97 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0037 s] Raw data (loadavg): 0.97 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.003 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.73 s] Raw data (loadavg): 0.99 0.97 0.92 1/53 15849 Raw data (stat): 15845 (minisat+_script) S 15844 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854386068 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.73 CPU time (s): 1229.88 CPU user time (s): 1229.17 CPU system time (s): 0.711891 CPU usage (%): 100.012 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####