Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-sentoy.opb |
MD5SUM | 4df3e7eb358d27d446e34b975724a6c1 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -7772 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 60 |
Biggest coefficient in the objective function | 974 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 9460 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 6000 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 26162 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.01784 |
Number of variables | 60 |
Total number of constraints | 90 |
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 | 30 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 60 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc19 THE 2005-05-27 06:54:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23300 boxname=wulflinc19 idbench=944 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4df3e7eb358d27d446e34b975724a6c1 /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-sentoy.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-sentoy.opb IDLAUNCH: 23300 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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.037 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: 913696 kB Buffers: 22060 kB Cached: 73072 kB SwapCached: 748 kB Active: 16076 kB Inactive: 81348 kB HighTotal: 131008 kB HighFree: 55076 kB LowTotal: 903652 kB LowFree: 858620 kB SwapTotal: 2097892 kB SwapFree: 2096428 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5412 kB Slab: 17736 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 07:15:27 (client local time) WITH STATUS 152 IN 1230.14 SECONDS stats: 23300 7 1230.14 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 30 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 29]---> BDD-cost:72336 c ---[ 28]---> BDD-cost:37152 c ---[ 27]---> BDD-cost:65344 c ---[ 26]---> BDD-cost:70690 c ---[ 25]---> BDD-cost:61701 c ---[ 24]---> BDD-cost:69736 c ---[ 23]---> BDD-cost:70681 c ---[ 22]---> BDD-cost:60569 c ---[ 21]---> BDD-cost:59590 c ---[ 20]---> BDD-cost:68898 c ---[ 19]---> BDD-cost:51292 c ---[ 18]---> BDD-cost:68218 c ---[ 17]---> BDD-cost:44969 c ---[ 16]---> BDD-cost:66420 c ---[ 15]---> BDD-cost:66330 c ---[ 14]---> BDD-cost:57913 c ---[ 13]---> BDD-cost:62873 c ---[ 12]---> BDD-cost:56928 c ---[ 11]---> BDD-cost:71330 c ---[ 10]---> BDD-cost:72214 c ---[ 9]---> BDD-cost:59705 c ---[ 8]---> BDD-cost:66833 c ---[ 7]---> BDD-cost:69775 c ---[ 6]---> BDD-cost:33741 c ---[ 5]---> BDD-cost:61412 c ---[ 4]---> BDD-cost:55558 c ---[ 3]---> BDD-cost:67780 c ---[ 2]---> BDD-cost:57716 c ---[ 1]---> BDD-cost:60300 c ---[ 0]---> BDD-cost:58322 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 5120745 15004487 | 1706915 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -74[0m c ---[ 0]---> Sorter-cost: 4579 Base: 3 5 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 5126230 15017358 | 1708743 0 0 nan | 0.000 % | c | 101 | 5126230 15017358 | 1879617 101 2767 27.4 | 0.002 % | c ============================================================================== c [1mFound solution: -2115[0m c ---[ 0]---> Sorter-cost: 6379 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 109 | 5142900 15056363 | 1714300 109 2842 26.1 | 0.002 % | c ============================================================================== c [1mFound solution: -2148[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 110 | 5143019 15056682 | 1714339 110 2994 27.2 | 0.002 % | c ============================================================================== c [1mFound solution: -2167[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115 | 5143186 15057132 | 1714395 115 3310 28.8 | 0.002 % | c ============================================================================== c [1mFound solution: -2223[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 116 | 5143272 15057360 | 1714424 116 3332 28.7 | 0.002 % | c ============================================================================== c [1mFound solution: -4014[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 164 | 5143329 15057503 | 1714443 164 5234 31.9 | 0.002 % | c ============================================================================== c [1mFound solution: -4018[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 245 | 5143340 15057543 | 1714446 245 10867 44.4 | 0.002 % | c ============================================================================== c [1mFound solution: -4303[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 246 | 5143370 15057624 | 1714456 246 10881 44.2 | 0.002 % | c ============================================================================== c [1mFound solution: -4314[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 248 | 5143377 15057647 | 1714459 248 11251 45.4 | 0.002 % | c ============================================================================== c [1mFound solution: -4476[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 249 | 5143454 15057851 | 1714484 249 11297 45.4 | 0.002 % | c ============================================================================== c [1mFound solution: -4498[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 251 | 5143464 15057887 | 1714488 251 11645 46.4 | 0.002 % | c ============================================================================== c [1mFound solution: -4799[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 255 | 5143484 15057940 | 1714494 255 12355 48.5 | 0.002 % | c ============================================================================== c [1mFound solution: -5339[0m c ---[ 0]---> Sorter-cost: 2 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 261 | 5143509 15058007 | 1714503 261 12475 47.8 | 0.002 % | c | 361 | 5143509 15058007 | 1885953 361 19045 52.8 | 0.002 % | c | 511 | 5143509 15058007 | 2074548 511 25704 50.3 | 0.002 % | c ============================================================================== c [1mFound solution: -5739[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 711 | 5143535 15058072 | 1714511 711 31763 44.7 | 0.002 % | c ============================================================================== c [1mFound solution: -5742[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 720 | 5143544 15058096 | 1714514 720 32506 45.1 | 0.002 % | c ============================================================================== c [1mFound solution: -5748[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 721 | 5143553 15058117 | 1714517 721 32518 45.1 | 0.002 % | c ============================================================================== c [1mFound solution: -5753[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 724 | 5143562 15058138 | 1714520 724 32925 45.5 | 0.002 % | c | 824 | 5143562 15058138 | 1885972 824 38956 47.3 | 0.003 % | c | 976 | 5143562 15058138 | 2074569 976 42516 43.6 | 0.003 % | c ============================================================================== c [1mFound solution: -6174[0m c ---[ 0]---> Sorter-cost: 2 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1150 | 5143570 15058158 | 1714523 1150 46885 40.8 | 0.003 % | c | 1251 | 5143570 15058158 | 1885975 1251 49317 39.4 | 0.003 % | c ============================================================================== c [1mFound solution: -6182[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1278 | 5143580 15058181 | 1714526 1278 50102 39.2 | 0.003 % | c | 1378 | 5143580 15058181 | 1885978 1378 53005 38.5 | 0.003 % | c | 1529 | 5143580 15058181 | 2074576 1529 56946 37.2 | 0.003 % | c | 1756 | 5143580 15058181 | 2282034 1756 65379 37.2 | 0.003 % | c ============================================================================== c [1mFound solution: -6198[0m c ---[ 0]---> Sorter-cost: 2 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1783 | 5143586 15058194 | 1714528 1783 66361 37.2 | 0.003 % | c | 1889 | 5143586 15058194 | 1885980 1889 69160 36.6 | 0.003 % | c | 2040 | 5143586 15058194 | 2074578 2040 75368 36.9 | 0.003 % | c ============================================================================== c [1mFound solution: -6456[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2175 | 5143613 15058263 | 1714537 2175 82741 38.0 | 0.003 % | c ============================================================================== c [1mFound solution: -6468[0m c ---[ 0]---> Sorter-cost: 2 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2217 | 5143617 15058277 | 1714539 2217 85055 38.4 | 0.003 % | c | 2318 | 5143617 15058277 | 1885992 2318 88469 38.2 | 0.003 % | c | 2468 | 5143617 15058277 | 2074592 2468 92790 37.6 | 0.003 % | c | 2693 | 5143617 15058277 | 2282051 2693 102057 37.9 | 0.003 % | c | 3030 | 5143617 15058277 | 2510256 3030 117955 38.9 | 0.003 % | c ============================================================================== c [1mFound solution: -6540[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3096 | 5143627 15058304 | 1714542 3096 120680 39.0 | 0.003 % | c | 3196 | 5143627 15058304 | 1885996 3196 126137 39.5 | 0.003 % | c ============================================================================== c [1mFound solution: -6569[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3238 | 5143633 15058318 | 1714544 3238 128108 39.6 | 0.003 % | c ============================================================================== c [1mFound solution: -6629[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3244 | 5143641 15058337 | 1714547 3244 128712 39.7 | 0.003 % | c ============================================================================== c [1mFound solution: -6683[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3337 | 5143649 15058355 | 1714549 3337 133758 40.1 | 0.003 % | c ============================================================================== c [1mFound solution: -6803[0m c ---[ 0]---> Sorter-cost: 3 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3404 | 5143664 15058394 | 1714554 3404 136067 40.0 | 0.003 % | c | 3507 | 5143664 15058394 | 1886009 3507 140200 40.0 | 0.003 % | c ============================================================================== c [1mFound solution: -6989[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3547 | 5143672 15058415 | 1714557 3547 141592 39.9 | 0.003 % | c ============================================================================== c [1mFound solution: -6993[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3577 | 5143680 15058434 | 1714560 3577 142953 40.0 | 0.003 % | c | 3677 | 5143680 15058434 | 1886016 3677 147101 40.0 | 0.003 % | c ============================================================================== c [1mFound solution: -7017[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3789 | 5143685 15058445 | 1714561 3789 151268 39.9 | 0.003 % | c ============================================================================== c [1mFound solution: -7018[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3794 | 5143690 15058456 | 1714563 3794 151798 40.0 | 0.003 % | c ============================================================================== c [1mFound solution: -7024[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3823 | 5143697 15058475 | 1714565 3823 153501 40.2 | 0.003 % | c ============================================================================== c [1mFound solution: -7073[0m c ---[ 0]---> Sorter-cost: 2 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3848 | 5143700 15058482 | 1714566 3848 154397 40.1 | 0.003 % | c ============================================================================== c [1mFound solution: -7080[0m c ---[ 0]---> Sorter-cost: 2 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3854 | 5143703 15058489 | 1714567 3854 154517 40.1 | 0.003 % | c ============================================================================== c [1mFound solution: -7083[0m c ---[ 0]---> Sorter-cost: 2 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3861 | 5143706 15058496 | 1714568 3861 155514 40.3 | 0.003 % | c ============================================================================== c [1mFound solution: -7084[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3869 | 5143715 15058518 | 1714571 3869 155912 40.3 | 0.003 % | c ============================================================================== c [1mFound solution: -7122[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3873 | 5143721 15058532 | 1714573 3873 156187 40.3 | 0.003 % | c | 3974 | 5143721 15058532 | 1886030 3974 161884 40.7 | 0.004 % | c | 4125 | 5143721 15058532 | 2074633 4125 166558 40.4 | 0.004 % | c ============================================================================== c [1mFound solution: -7136[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4140 | 5143728 15058549 | 1714576 4140 167891 40.6 | 0.004 % | c | 4240 | 5143728 15058549 | 1886033 4240 171154 40.4 | 0.004 % | c | 4390 | 5143728 15058549 | 2074636 4390 176368 40.2 | 0.004 % | c ============================================================================== c [1mFound solution: -7289[0m c ---[ 0]---> Sorter-cost: 1 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4553 | 5143742 15058585 | 1714580 4553 184434 40.5 | 0.004 % | c | 4653 | 5143742 15058585 | 1886038 4653 187269 40.2 | 0.004 % | c ============================================================================== c [1mFound solution: -7296[0m c ---[ 0]---> Sorter-cost: 3 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4759 | 5143747 15058601 | 1714582 4759 190059 39.9 | 0.004 % | c ============================================================================== c [1mFound solution: -7345[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4770 | 5143754 15058618 | 1714584 4770 191193 40.1 | 0.004 % | c ============================================================================== c [1mFound solution: -7351[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4780 | 5143761 15058636 | 1714587 4780 191588 40.1 | 0.004 % | c | 4881 | 5143761 15058636 | 1886045 4881 194680 39.9 | 0.004 % | c | 5032 | 5143761 15058636 | 2074650 5032 200411 39.8 | 0.004 % | c | 5259 | 5143761 15058636 | 2282115 5259 208312 39.6 | 0.004 % | c ============================================================================== c [1mFound solution: -7367[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5376 | 5143767 15058650 | 1714589 5376 214197 39.8 | 0.004 % | c | 5476 | 5143767 15058650 | 1886047 5476 217837 39.8 | 0.004 % | c | 5626 | 5143767 15058650 | 2074652 5626 226727 40.3 | 0.004 % | c ============================================================================== c [1mFound solution: -7377[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5813 | 5143776 15058671 | 1714592 5813 235166 40.5 | 0.004 % | c | 5913 | 5143776 15058671 | 1886051 5913 241541 40.8 | 0.004 % | c | 6063 | 5143776 15058671 | 2074656 6063 247268 40.8 | 0.004 % | c | 6289 | 5143776 15058671 | 2282121 6289 254345 40.4 | 0.004 % | c ============================================================================== c [1mFound solution: -7500[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 2 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6310 | 5143782 15058685 | 1714594 6310 254903 40.4 | 0.004 % | c | 6412 | 5143782 15058685 | 1886053 6412 260396 40.6 | 0.004 % | c | 6562 | 5143782 15058685 | 2074658 6562 268270 40.9 | 0.004 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 2073 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.92 0.95 0.90 2/54 2069 Raw data (stat): 2069 (runsolver) R 2068 10795 10794 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 854154165 1052672 97 4294967295 134512640 135381576 3221224464 3221219892 135011375 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 97 215 215 0 42 0 vsize: 1028 [startup+10.0009 s] Raw data (loadavg): 1.01 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0013 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0027 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0033 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0038 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0039 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0047 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0052 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0058 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/55 2073 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.02 s] Raw data (loadavg): 1.16 1.00 0.92 2/57 2105 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.021 s] Raw data (loadavg): 1.13 1.00 0.92 2/55 2126 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.022 s] Raw data (loadavg): 1.11 1.00 0.92 2/55 2126 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.022 s] Raw data (loadavg): 1.10 1.00 0.92 2/55 2126 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.022 s] Raw data (loadavg): 1.08 1.00 0.92 2/55 2126 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.023 s] Raw data (loadavg): 1.07 1.00 0.92 2/55 2126 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.023 s] Raw data (loadavg): 1.06 1.00 0.92 2/55 2126 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.024 s] Raw data (loadavg): 1.05 1.00 0.92 2/55 2126 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.025 s] Raw data (loadavg): 1.04 1.00 0.92 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.024 s] Raw data (loadavg): 1.03 1.00 0.92 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.025 s] Raw data (loadavg): 1.03 1.00 0.92 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.024 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.026 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.026 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.027 s] Raw data (loadavg): 1.01 1.00 0.92 3/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.028 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.028 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.029 s] Raw data (loadavg): 1.08 1.02 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.03 s] Raw data (loadavg): 1.07 1.02 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.03 s] Raw data (loadavg): 1.06 1.01 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.036 s] Raw data (loadavg): 1.05 1.01 0.93 3/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.036 s] Raw data (loadavg): 1.04 1.01 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.037 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.036 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.036 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.037 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.044 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.052 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.052 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.051 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.051 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 2128 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.052 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.053 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.059 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.165 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.165 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.165 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.166 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.168 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.167 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.168 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.176 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.177 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.279 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.297 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.306 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.306 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.307 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.307 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.307 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.308 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.309 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.31 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.309 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.309 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.31 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.31 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.311 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.312 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.311 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.312 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.312 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.313 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.313 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.313 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.314 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.314 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.315 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.315 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.32 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1230.18 s] Raw data (loadavg): 1.00 1.00 0.93 1/53 2130 Raw data (stat): 2069 (minisat+_script) S 2068 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854154165 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1230.18 CPU time (s): 1230.14 CPU user time (s): 1225.9 CPU system time (s): 4.23935 CPU usage (%): 99.997 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####