Name | normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cmb.opb |
MD5SUM | a8596c98551f801a6658f1ce91b33278 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1053 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 304 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 12887 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 12887 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.97785 |
Number of variables | 304 |
Total number of constraints | 671 |
Number of constraints which are clauses | 671 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 28 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc32 THE 2005-04-14 02:31:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4389 boxname=wulflinc32 idbench=253 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a8596c98551f801a6658f1ce91b33278 /oldhome/oroussel/tmp/wulflinc32/normalized-cmb.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc32/normalized-cmb.opb /oldhome/oroussel/tmp/wulflinc32/normalized-cmb.opb IDLAUNCH: 4389 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.085 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.085 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: 1034724 kB MemFree: 704988 kB Buffers: 35212 kB Cached: 182876 kB SwapCached: 1212 kB Active: 146536 kB Inactive: 151964 kB HighTotal: 131072 kB HighFree: 256 kB LowTotal: 903652 kB LowFree: 704732 kB SwapTotal: 2097892 kB SwapFree: 2096680 kB Dirty: 2340 kB Writeback: 0 kB Mapped: 81768 kB Slab: 25296 kB Committed_AS: 174000 kB PageTables: 432 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 02:51:38 (client local time) WITH STATUS 10 IN 1200.3 SECONDS stats: 4389 7 1200.3 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 667 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 667 3359 | 222 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 1524[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:43621 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 105121 247278 | 35040 0 0 nan | 0.000 % | c | 103 | 104168 245118 | 38544 97 4313 44.5 | 0.665 % | c | 253 | 103349 243238 | 42398 229 8034 35.1 | 1.287 % | c | 479 | 103349 243238 | 46638 455 17849 39.2 | 1.287 % | c | 816 | 103349 243238 | 51302 792 23717 29.9 | 1.287 % | c | 1322 | 103349 243238 | 56432 1298 40177 31.0 | 1.287 % | c | 2083 | 103122 242717 | 62075 2058 75941 36.9 | 1.487 % | c | 3222 | 102780 241953 | 68283 3169 126886 40.0 | 1.754 % | c | 4932 | 102722 241821 | 75111 4870 197921 40.6 | 1.797 % | c | 7495 | 102722 241821 | 82622 7433 294908 39.7 | 1.797 % | c ============================================================================== c [1mFound solution: 1514[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:36082 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8239 | 189796 445156 | 63265 8177 316528 38.7 | 1.797 % | c | 8339 | 189796 445156 | 69591 8277 322185 38.9 | 1.049 % | c | 8490 | 189796 445156 | 76550 8428 326473 38.7 | 1.049 % | c | 8715 | 189774 445107 | 84205 8650 331229 38.3 | 1.059 % | c | 9052 | 189647 444838 | 92626 8982 333087 37.1 | 1.125 % | c | 9558 | 189568 444660 | 101888 9486 337879 35.6 | 1.152 % | c ============================================================================== c [1mFound solution: 1498[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9601 | 189573 444797 | 63191 9529 339448 35.6 | 1.152 % | c ============================================================================== c [1mFound solution: 1490[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9608 | 189907 445610 | 63302 9536 339814 35.6 | 1.152 % | c ============================================================================== c [1mFound solution: 1450[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9611 | 189928 445664 | 63309 9539 340630 35.7 | 1.152 % | c ============================================================================== c [1mFound solution: 1416[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9623 | 190264 446559 | 63421 9551 341049 35.7 | 1.152 % | c | 9724 | 190264 446559 | 69763 9652 348331 36.1 | 1.152 % | c | 9874 | 190264 446559 | 76739 9802 364696 37.2 | 1.152 % | c | 10099 | 190252 446532 | 84413 10026 380599 38.0 | 1.157 % | c | 10439 | 190252 446532 | 92854 10366 387470 37.4 | 1.157 % | c | 10945 | 190252 446532 | 102140 10872 406819 37.4 | 1.157 % | c ============================================================================== c [1mFound solution: 1326[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11585 | 190286 446619 | 63428 11512 555064 48.2 | 1.157 % | c | 11686 | 190286 446619 | 69770 11613 558245 48.1 | 1.158 % | c | 11839 | 190286 446619 | 76747 11766 566083 48.1 | 1.158 % | c | 12064 | 190286 446619 | 84422 11991 577304 48.1 | 1.158 % | c | 12402 | 190286 446619 | 92864 12329 581418 47.2 | 1.158 % | c | 12908 | 190258 446556 | 102151 12834 604153 47.1 | 1.167 % | c | 13667 | 190204 446436 | 112366 13589 636533 46.8 | 1.190 % | c | 14806 | 190153 446322 | 123603 14720 668941 45.4 | 1.212 % | c | 16514 | 189969 445907 | 135963 16409 754857 46.0 | 1.289 % | c | 19076 | 189969 445907 | 149559 18971 880480 46.4 | 1.289 % | c | 22921 | 189969 445907 | 164515 22816 1083581 47.5 | 1.289 % | c | 28688 | 189969 445907 | 180967 28583 1429962 50.0 | 1.289 % | c | 37340 | 189969 445907 | 199064 37235 2157656 57.9 | 1.289 % | c | 50318 | 189969 445907 | 218970 50213 4133473 82.3 | 1.289 % | c | 69780 | 189969 445907 | 240867 69675 7316398 105.0 | 1.289 % | c | 98972 | 189969 445907 | 264954 98867 9521248 96.3 | 1.289 % | #### 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.84 0.95 0.93 2/53 14360 Raw data (stat): 14360 (runsolver) R 14359 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481006773 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0013 s] Raw data (loadavg): 0.87 0.95 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 3685 0 0 0 989 9 0 0 25 0 1 0 481006773 17952768 3535 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4383 3535 603 41 0 4342 0 vsize: 17532 [startup+20.0021 s] Raw data (loadavg): 0.89 0.95 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 3815 0 0 0 1989 9 0 0 25 0 1 0 481006773 18513920 3665 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4520 3665 603 41 0 4479 0 vsize: 18080 [startup+30.0031 s] Raw data (loadavg): 0.90 0.95 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 3967 0 0 0 2989 10 0 0 25 0 1 0 481006773 19050496 3817 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4651 3817 603 41 0 4610 0 vsize: 18604 [startup+40.0036 s] Raw data (loadavg): 0.92 0.95 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6419 0 0 0 3983 15 0 0 25 0 1 0 481006773 32186368 6269 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7858 6269 603 41 0 7817 0 vsize: 31432 [startup+50.0053 s] Raw data (loadavg): 0.93 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6549 0 0 0 4982 16 0 0 25 0 1 0 481006773 32739328 6399 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7993 6399 603 41 0 7952 0 vsize: 31972 [startup+60.0064 s] Raw data (loadavg): 0.94 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6729 0 0 0 5981 17 0 0 25 0 1 0 481006773 33431552 6579 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8162 6579 603 41 0 8121 0 vsize: 32648 [startup+70.0069 s] Raw data (loadavg): 0.95 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6799 0 0 0 6980 18 0 0 25 0 1 0 481006773 33665024 6649 4294967295 134512640 134672761 3221224560 3221223708 1074723737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8219 6649 603 41 0 8178 0 vsize: 32876 [startup+80.0077 s] Raw data (loadavg): 0.96 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6867 0 0 0 7980 18 0 0 25 0 1 0 481006773 33935360 6717 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8285 6717 603 41 0 8244 0 vsize: 33140 [startup+90.0084 s] Raw data (loadavg): 0.96 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6931 0 0 0 8980 18 0 0 25 0 1 0 481006773 34205696 6781 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8351 6781 603 41 0 8310 0 vsize: 33404 [startup+100.009 s] Raw data (loadavg): 0.97 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7008 0 0 0 9980 18 0 0 25 0 1 0 481006773 34607104 6858 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8449 6858 603 41 0 8408 0 vsize: 33796 [startup+110.01 s] Raw data (loadavg): 0.97 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7072 0 0 0 10980 19 0 0 25 0 1 0 481006773 34873344 6922 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8514 6922 603 41 0 8473 0 vsize: 34056 [startup+120.011 s] Raw data (loadavg): 0.98 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7133 0 0 0 11980 19 0 0 25 0 1 0 481006773 35139584 6983 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8579 6983 603 41 0 8538 0 vsize: 34316 [startup+130.013 s] Raw data (loadavg): 0.98 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7185 0 0 0 12979 19 0 0 25 0 1 0 481006773 35274752 7035 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8612 7035 603 41 0 8571 0 vsize: 34448 [startup+140.013 s] Raw data (loadavg): 0.98 0.96 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7250 0 0 0 13979 19 0 0 25 0 1 0 481006773 35540992 7100 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8677 7100 603 41 0 8636 0 vsize: 34708 [startup+150.014 s] Raw data (loadavg): 0.98 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7321 0 0 0 14979 20 0 0 25 0 1 0 481006773 35946496 7171 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8776 7171 603 41 0 8735 0 vsize: 35104 [startup+160.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7406 0 0 0 15978 20 0 0 25 0 1 0 481006773 36208640 7256 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8840 7256 603 41 0 8799 0 vsize: 35360 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7488 0 0 0 16978 20 0 0 25 0 1 0 481006773 36605952 7338 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8937 7338 603 41 0 8896 0 vsize: 35748 [startup+180.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7564 0 0 0 17978 20 0 0 25 0 1 0 481006773 36872192 7414 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9002 7414 603 41 0 8961 0 vsize: 36008 [startup+190.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7676 0 0 0 18978 21 0 0 25 0 1 0 481006773 37273600 7526 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9100 7526 603 41 0 9059 0 vsize: 36400 [startup+200.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7778 0 0 0 19978 21 0 0 25 0 1 0 481006773 37675008 7628 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9198 7628 603 41 0 9157 0 vsize: 36792 [startup+210.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7853 0 0 0 20977 22 0 0 25 0 1 0 481006773 38072320 7703 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9295 7703 603 41 0 9254 0 vsize: 37180 [startup+220.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7928 0 0 0 21977 22 0 0 25 0 1 0 481006773 38334464 7778 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9359 7778 603 41 0 9318 0 vsize: 37436 [startup+230.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8013 0 0 0 22977 22 0 0 25 0 1 0 481006773 38735872 7863 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9457 7863 603 41 0 9416 0 vsize: 37828 [startup+240.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8090 0 0 0 23977 22 0 0 25 0 1 0 481006773 39006208 7940 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9523 7940 603 41 0 9482 0 vsize: 38092 [startup+250.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8161 0 0 0 24977 23 0 0 25 0 1 0 481006773 39272448 8011 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9588 8011 603 41 0 9547 0 vsize: 38352 [startup+260.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8237 0 0 0 25977 23 0 0 25 0 1 0 481006773 39669760 8087 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9685 8087 603 41 0 9644 0 vsize: 38740 [startup+270.024 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8300 0 0 0 26977 24 0 0 25 0 1 0 481006773 39936000 8150 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9750 8150 603 41 0 9709 0 vsize: 39000 [startup+280.025 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8375 0 0 0 27977 24 0 0 25 0 1 0 481006773 40333312 8225 4294967295 134512640 134672761 3221224560 3221223744 134559594 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9847 8225 603 41 0 9806 0 vsize: 39388 [startup+290.026 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8443 0 0 0 28977 24 0 0 25 0 1 0 481006773 40603648 8293 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9913 8293 603 41 0 9872 0 vsize: 39652 [startup+300.026 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8505 0 0 0 29977 24 0 0 25 0 1 0 481006773 40869888 8355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9978 8355 603 41 0 9937 0 vsize: 39912 [startup+310.027 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8575 0 0 0 30977 24 0 0 25 0 1 0 481006773 41132032 8425 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10042 8425 603 41 0 10001 0 vsize: 40168 [startup+320.028 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8643 0 0 0 31976 25 0 0 25 0 1 0 481006773 41394176 8493 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10106 8493 603 41 0 10065 0 vsize: 40424 [startup+330.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8711 0 0 0 32976 25 0 0 25 0 1 0 481006773 41664512 8561 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10172 8561 603 41 0 10131 0 vsize: 40688 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8777 0 0 0 33977 25 0 0 25 0 1 0 481006773 41934848 8627 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10238 8627 603 41 0 10197 0 vsize: 40952 [startup+350.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8874 0 0 0 34977 25 0 0 25 0 1 0 481006773 42332160 8724 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10335 8724 603 41 0 10294 0 vsize: 41340 [startup+360.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8979 0 0 0 35977 25 0 0 25 0 1 0 481006773 42737664 8829 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10434 8829 603 41 0 10393 0 vsize: 41736 [startup+370.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9090 0 0 0 36976 26 0 0 25 0 1 0 481006773 43143168 8940 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10533 8940 603 41 0 10492 0 vsize: 42132 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9190 0 0 0 37976 26 0 0 25 0 1 0 481006773 43540480 9040 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10630 9040 603 41 0 10589 0 vsize: 42520 [startup+390.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9340 0 0 0 38976 27 0 0 25 0 1 0 481006773 44212224 9190 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10794 9190 603 41 0 10753 0 vsize: 43176 [startup+400.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9486 0 0 0 39975 28 0 0 25 0 1 0 481006773 44740608 9336 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10923 9336 603 41 0 10882 0 vsize: 43692 [startup+410.035 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9636 0 0 0 40975 28 0 0 25 0 1 0 481006773 45404160 9486 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11085 9486 603 41 0 11044 0 vsize: 44340 [startup+420.043 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9758 0 0 0 41976 28 0 0 25 0 1 0 481006773 45940736 9608 4294967295 134512640 134672761 3221224560 3221223696 134565134 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11216 9609 603 41 0 11175 0 vsize: 44864 [startup+430.049 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9895 0 0 0 42976 29 0 0 25 0 1 0 481006773 46469120 9745 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11345 9745 603 41 0 11304 0 vsize: 45380 [startup+440.06 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10032 0 0 0 43976 29 0 0 25 0 1 0 481006773 47009792 9882 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11477 9882 603 41 0 11436 0 vsize: 45908 [startup+450.061 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10194 0 0 0 44976 30 0 0 25 0 1 0 481006773 47673344 10044 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11639 10044 603 41 0 11598 0 vsize: 46556 [startup+460.062 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10348 0 0 0 45976 30 0 0 25 0 1 0 481006773 48345088 10198 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11803 10198 603 41 0 11762 0 vsize: 47212 [startup+470.062 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10522 0 0 0 46976 31 0 0 25 0 1 0 481006773 49025024 10372 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11969 10372 603 41 0 11928 0 vsize: 47876 [startup+480.063 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10671 0 0 0 47975 32 0 0 25 0 1 0 481006773 49565696 10521 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12101 10521 603 41 0 12060 0 vsize: 48404 [startup+490.064 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10805 0 0 0 48974 33 0 0 25 0 1 0 481006773 50241536 10655 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12266 10655 603 41 0 12225 0 vsize: 49064 [startup+500.066 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10882 0 0 0 49975 33 0 0 25 0 1 0 481006773 50511872 10732 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12332 10732 603 41 0 12291 0 vsize: 49328 [startup+510.067 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10973 0 0 0 50974 33 0 0 25 0 1 0 481006773 50913280 10823 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12430 10823 603 41 0 12389 0 vsize: 49720 [startup+520.067 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11108 0 0 0 51974 34 0 0 25 0 1 0 481006773 51445760 10958 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12560 10958 603 41 0 12519 0 vsize: 50240 [startup+530.068 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11277 0 0 0 52974 34 0 0 25 0 1 0 481006773 52109312 11127 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12722 11127 603 41 0 12681 0 vsize: 50888 [startup+540.069 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11381 0 0 0 53974 34 0 0 25 0 1 0 481006773 52514816 11231 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12821 11231 603 41 0 12780 0 vsize: 51284 [startup+550.082 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11477 0 0 0 54975 34 0 0 25 0 1 0 481006773 52916224 11327 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12919 11327 603 41 0 12878 0 vsize: 51676 [startup+560.083 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11574 0 0 0 55975 35 0 0 25 0 1 0 481006773 53317632 11424 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13017 11424 603 41 0 12976 0 vsize: 52068 [startup+570.084 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11706 0 0 0 56975 35 0 0 25 0 1 0 481006773 53846016 11556 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13146 11556 603 41 0 13105 0 vsize: 52584 [startup+580.085 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11840 0 0 0 57975 36 0 0 25 0 1 0 481006773 54378496 11690 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13276 11690 603 41 0 13235 0 vsize: 53104 [startup+590.086 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11974 0 0 0 58975 36 0 0 25 0 1 0 481006773 54919168 11824 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13408 11824 603 41 0 13367 0 vsize: 53632 [startup+600.087 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12124 0 0 0 59975 36 0 0 25 0 1 0 481006773 55578624 11974 4294967295 134512640 134672761 3221224560 3221223728 134564448 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13569 11974 603 41 0 13528 0 vsize: 54276 [startup+610.087 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12275 0 0 0 60975 37 0 0 25 0 1 0 481006773 56115200 12125 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13700 12125 603 41 0 13659 0 vsize: 54800 [startup+620.088 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12405 0 0 0 61975 37 0 0 25 0 1 0 481006773 56651776 12255 4294967295 134512640 134672761 3221224560 3221223664 134560039 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13831 12255 603 41 0 13790 0 vsize: 55324 [startup+630.089 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12569 0 0 0 62975 37 0 0 25 0 1 0 481006773 57352192 12419 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14002 12419 603 41 0 13961 0 vsize: 56008 [startup+640.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12716 0 0 0 63974 38 0 0 25 0 1 0 481006773 58019840 12566 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14165 12566 603 41 0 14124 0 vsize: 56660 [startup+650.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12825 0 0 0 64974 39 0 0 25 0 1 0 481006773 58417152 12675 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14262 12675 603 41 0 14221 0 vsize: 57048 [startup+660.091 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12985 0 0 0 65973 39 0 0 25 0 1 0 481006773 59084800 12835 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14425 12835 603 41 0 14384 0 vsize: 57700 [startup+670.092 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13161 0 0 0 66974 39 0 0 25 0 1 0 481006773 59760640 13011 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14590 13011 603 41 0 14549 0 vsize: 58360 [startup+680.093 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13324 0 0 0 67973 40 0 0 25 0 1 0 481006773 60690432 13174 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14817 13174 603 41 0 14776 0 vsize: 59268 [startup+690.093 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13484 0 0 0 68973 40 0 0 25 0 1 0 481006773 61362176 13334 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14981 13334 603 41 0 14940 0 vsize: 59924 [startup+700.094 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13639 0 0 0 69973 41 0 0 25 0 1 0 481006773 62038016 13489 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15146 13489 603 41 0 15105 0 vsize: 60584 [startup+710.095 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13763 0 0 0 70973 41 0 0 25 0 1 0 481006773 62562304 13613 4294967295 134512640 134672761 3221224560 3221223664 134559966 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15274 13613 603 41 0 15233 0 vsize: 61096 [startup+720.096 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13921 0 0 0 71973 41 0 0 25 0 1 0 481006773 63217664 13771 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15434 13771 603 41 0 15393 0 vsize: 61736 [startup+730.097 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14069 0 0 0 72972 42 0 0 25 0 1 0 481006773 63758336 13919 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15566 13919 603 41 0 15525 0 vsize: 62264 [startup+740.098 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14138 0 0 0 73972 42 0 0 25 0 1 0 481006773 64028672 13988 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15632 13988 603 41 0 15591 0 vsize: 62528 [startup+750.099 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14193 0 0 0 74972 43 0 0 25 0 1 0 481006773 64294912 14043 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15697 14043 603 41 0 15656 0 vsize: 62788 [startup+760.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14243 0 0 0 75972 43 0 0 25 0 1 0 481006773 64430080 14093 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15730 14093 603 41 0 15689 0 vsize: 62920 [startup+770.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14294 0 0 0 76972 43 0 0 25 0 1 0 481006773 64696320 14144 4294967295 134512640 134672761 3221224560 3221223696 134560585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15795 14144 603 41 0 15754 0 vsize: 63180 [startup+780.101 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14354 0 0 0 77972 43 0 0 25 0 1 0 481006773 64966656 14204 4294967295 134512640 134672761 3221224560 3221223744 134559159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15861 14204 603 41 0 15820 0 vsize: 63444 [startup+790.102 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14418 0 0 0 78972 43 0 0 25 0 1 0 481006773 65228800 14268 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15925 14268 603 41 0 15884 0 vsize: 63700 [startup+800.103 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14461 0 0 0 79972 43 0 0 25 0 1 0 481006773 65359872 14311 4294967295 134512640 134672761 3221224560 3221223760 134557811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15957 14311 603 41 0 15916 0 vsize: 63828 [startup+810.104 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14526 0 0 0 80972 44 0 0 25 0 1 0 481006773 65622016 14376 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16021 14376 603 41 0 15980 0 vsize: 64084 [startup+820.104 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14577 0 0 0 81972 44 0 0 25 0 1 0 481006773 65884160 14427 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16085 14427 603 41 0 16044 0 vsize: 64340 [startup+830.105 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14630 0 0 0 82972 44 0 0 25 0 1 0 481006773 66015232 14480 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16117 14480 603 41 0 16076 0 vsize: 64468 [startup+840.106 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14685 0 0 0 83972 44 0 0 25 0 1 0 481006773 66293760 14535 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16185 14535 603 41 0 16144 0 vsize: 64740 [startup+850.108 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14729 0 0 0 84972 45 0 0 25 0 1 0 481006773 66424832 14579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16217 14579 603 41 0 16176 0 vsize: 64868 [startup+860.108 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14803 0 0 0 85972 45 0 0 25 0 1 0 481006773 66826240 14653 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16315 14653 603 41 0 16274 0 vsize: 65260 [startup+870.109 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14862 0 0 0 86972 45 0 0 25 0 1 0 481006773 66957312 14712 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16347 14712 603 41 0 16306 0 vsize: 65388 [startup+880.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14912 0 0 0 87973 45 0 0 25 0 1 0 481006773 67227648 14762 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16413 14762 603 41 0 16372 0 vsize: 65652 [startup+890.111 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14963 0 0 0 88973 45 0 0 25 0 1 0 481006773 67362816 14813 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16446 14813 603 41 0 16405 0 vsize: 65784 [startup+900.111 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15018 0 0 0 89973 46 0 0 25 0 1 0 481006773 67633152 14868 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16512 14868 603 41 0 16471 0 vsize: 66048 [startup+910.112 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15067 0 0 0 90972 46 0 0 25 0 1 0 481006773 67895296 14917 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16576 14917 603 41 0 16535 0 vsize: 66304 [startup+920.113 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15112 0 0 0 91972 46 0 0 25 0 1 0 481006773 68030464 14962 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16609 14962 603 41 0 16568 0 vsize: 66436 [startup+930.114 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15163 0 0 0 92973 46 0 0 25 0 1 0 481006773 68165632 15013 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16642 15013 603 41 0 16601 0 vsize: 66568 [startup+940.114 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15203 0 0 0 93973 46 0 0 25 0 1 0 481006773 68431872 15053 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16707 15053 603 41 0 16666 0 vsize: 66828 [startup+950.115 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15247 0 0 0 94973 47 0 0 25 0 1 0 481006773 68567040 15097 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16740 15097 603 41 0 16699 0 vsize: 66960 [startup+960.116 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15291 0 0 0 95973 47 0 0 25 0 1 0 481006773 68706304 15141 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16774 15141 603 41 0 16733 0 vsize: 67096 [startup+970.117 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15366 0 0 0 96973 47 0 0 25 0 1 0 481006773 69103616 15216 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16871 15216 603 41 0 16830 0 vsize: 67484 [startup+980.117 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15421 0 0 0 97973 47 0 0 25 0 1 0 481006773 69234688 15271 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16903 15271 603 41 0 16862 0 vsize: 67612 [startup+990.118 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15471 0 0 0 98973 47 0 0 25 0 1 0 481006773 69496832 15321 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16967 15321 603 41 0 16926 0 vsize: 67868 [startup+1000.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15526 0 0 0 99973 48 0 0 25 0 1 0 481006773 69632000 15376 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17000 15376 603 41 0 16959 0 vsize: 68000 [startup+1010.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15582 0 0 0 100973 48 0 0 25 0 1 0 481006773 69894144 15432 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17064 15432 603 41 0 17023 0 vsize: 68256 [startup+1020.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15641 0 0 0 101973 48 0 0 25 0 1 0 481006773 70164480 15491 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17130 15491 603 41 0 17089 0 vsize: 68520 [startup+1030.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15705 0 0 0 102974 48 0 0 25 0 1 0 481006773 70430720 15555 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17195 15555 603 41 0 17154 0 vsize: 68780 [startup+1040.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15769 0 0 0 103974 48 0 0 25 0 1 0 481006773 70701056 15619 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17261 15619 603 41 0 17220 0 vsize: 69044 [startup+1050.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15840 0 0 0 104974 48 0 0 25 0 1 0 481006773 70967296 15690 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17326 15690 603 41 0 17285 0 vsize: 69304 [startup+1060.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15922 0 0 0 105974 49 0 0 25 0 1 0 481006773 71364608 15772 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17423 15772 603 41 0 17382 0 vsize: 69692 [startup+1070.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15981 0 0 0 106974 49 0 0 25 0 1 0 481006773 71495680 15831 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17455 15831 603 41 0 17414 0 vsize: 69820 [startup+1080.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16038 0 0 0 107974 49 0 0 25 0 1 0 481006773 71761920 15888 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17520 15888 603 41 0 17479 0 vsize: 70080 [startup+1090.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16100 0 0 0 108974 49 0 0 25 0 1 0 481006773 72032256 15950 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17586 15950 603 41 0 17545 0 vsize: 70344 [startup+1100.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16163 0 0 0 109974 49 0 0 25 0 1 0 481006773 72298496 16013 4294967295 134512640 134672761 3221224560 3221223760 134557820 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17651 16013 603 41 0 17610 0 vsize: 70604 [startup+1110.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16221 0 0 0 110974 49 0 0 25 0 1 0 481006773 72564736 16071 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17716 16071 603 41 0 17675 0 vsize: 70864 [startup+1120.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16281 0 0 0 111974 50 0 0 25 0 1 0 481006773 72826880 16131 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17780 16131 603 41 0 17739 0 vsize: 71120 [startup+1130.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16336 0 0 0 112974 50 0 0 25 0 1 0 481006773 72962048 16186 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17813 16186 603 41 0 17772 0 vsize: 71252 [startup+1140.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16393 0 0 0 113974 50 0 0 25 0 1 0 481006773 73224192 16243 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17877 16243 603 41 0 17836 0 vsize: 71508 [startup+1150.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16450 0 0 0 114974 51 0 0 25 0 1 0 481006773 73490432 16300 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17942 16300 603 41 0 17901 0 vsize: 71768 [startup+1160.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16502 0 0 0 115974 51 0 0 25 0 1 0 481006773 73621504 16352 4294967295 134512640 134672761 3221224560 3221223696 134560637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17974 16352 603 41 0 17933 0 vsize: 71896 [startup+1170.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16558 0 0 0 116974 51 0 0 25 0 1 0 481006773 73887744 16408 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18039 16408 603 41 0 17998 0 vsize: 72156 [startup+1180.13 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16620 0 0 0 117974 51 0 0 25 0 1 0 481006773 74182656 16470 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18111 16470 603 41 0 18070 0 vsize: 72444 [startup+1190.14 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16672 0 0 0 118974 51 0 0 25 0 1 0 481006773 74317824 16522 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18144 16522 603 41 0 18103 0 vsize: 72576 [startup+1200.14 s] Raw data (loadavg): 0.99 0.97 0.93 2/53 14360 Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16722 0 0 0 119974 52 0 0 25 0 1 0 481006773 74579968 16572 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18208 16572 603 41 0 18167 0 vsize: 72832 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.18 s] Raw data (loadavg): 0.99 0.97 0.93 1/53 14360 Raw data (stat): 14360 (minisat+) Z 14359 7987 7986 0 -1 12 16725 0 0 0 119974 55 0 0 25 0 1 0 481006773 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.18 CPU time (s): 1200.3 CPU user time (s): 1199.74 CPU system time (s): 0.554915 CPU usage (%): 100.01 Max. virtual memory (Kb): 72832 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####