Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-3.opb |
MD5SUM | 25457db86ce3cc3b7604dfa37c8096b4 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -28 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 595 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 595 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 595 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 595 |
Total number of constraints | 27931 |
Number of constraints which are clauses | 27931 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc25 THE 2005-04-14 02:45:59 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4457 boxname=wulflinc25 idbench=321 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 25457db86ce3cc3b7604dfa37c8096b4 /oldhome/oroussel/tmp/wulflinc25/normalized-frb35-17-3.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-frb35-17-3.opb /oldhome/oroussel/tmp/wulflinc25/normalized-frb35-17-3.opb IDLAUNCH: 4457 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 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.220 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 873232 kB Buffers: 34956 kB Cached: 91352 kB SwapCached: 36 kB Active: 50584 kB Inactive: 78592 kB HighTotal: 131008 kB HighFree: 35980 kB LowTotal: 903652 kB LowFree: 837252 kB SwapTotal: 2097892 kB SwapFree: 2097856 kB Dirty: 44 kB Writeback: 0 kB Mapped: 6920 kB Slab: 26516 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 03:06:02 (client local time) WITH STATUS 10 IN 1200.22 SECONDS stats: 4457 7 1200.22 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 27931 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 | 27931 55862 | 9310 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -25[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:26814 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 56226 122317 | 18742 0 0 nan | 0.000 % | c | 100 | 56017 121884 | 20616 93 1165 12.5 | 0.585 % | c | 250 | 55219 120180 | 22677 215 2505 11.7 | 2.925 % | c | 475 | 54050 117632 | 24945 366 4294 11.7 | 6.485 % | c | 813 | 52427 114064 | 27440 604 7515 12.4 | 11.657 % | c ============================================================================== c [1mFound solution: -26[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1312 | 49748 108075 | 16582 973 13038 13.4 | 11.657 % | c | 1412 | 49314 107081 | 18240 1047 14480 13.8 | 21.494 % | c | 1562 | 48109 104346 | 20064 1117 15274 13.7 | 25.435 % | c | 1787 | 46873 101501 | 22070 1273 17136 13.5 | 29.543 % | c | 2124 | 45440 98214 | 24277 1530 19819 13.0 | 34.301 % | c | 2630 | 43350 93367 | 26705 1845 25665 13.9 | 41.215 % | c | 3389 | 41978 90084 | 29376 2483 31539 12.7 | 45.869 % | c ============================================================================== c [1mFound solution: -27[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3553 | 41830 89810 | 13943 2628 34703 13.2 | 45.869 % | c | 3653 | 41490 88994 | 15337 2682 35918 13.4 | 47.845 % | c | 3803 | 41155 88218 | 16871 2808 38474 13.7 | 48.966 % | c | 4028 | 40908 87625 | 18558 2975 42154 14.2 | 49.830 % | c | 4365 | 40256 86118 | 20413 3168 49450 15.6 | 52.022 % | c | 4871 | 39264 83777 | 22455 3528 61471 17.4 | 55.427 % | c ============================================================================== c [1mFound solution: -28[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5253 | 38681 82397 | 12893 3832 66544 17.4 | 55.427 % | c | 5354 | 38557 82103 | 14182 3922 71658 18.3 | 57.906 % | c | 5504 | 38289 81462 | 15600 4018 73309 18.2 | 58.842 % | c | 5730 | 38127 81078 | 17160 4185 78516 18.8 | 59.413 % | c | 6067 | 37939 80622 | 18876 4417 84596 19.2 | 60.102 % | c | 6574 | 37077 78579 | 20764 4679 91036 19.5 | 63.065 % | c | 7334 | 36460 77108 | 22840 5284 107904 20.4 | 65.312 % | c | 8474 | 35325 74406 | 25124 6063 138814 22.9 | 69.098 % | c ============================================================================== c [1mFound solution: -29[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9550 | 35051 73788 | 11683 7007 181532 25.9 | 69.098 % | c | 9650 | 35051 73788 | 12851 7107 185723 26.1 | 70.086 % | c | 9800 | 35044 73773 | 14136 7237 189597 26.2 | 70.106 % | c | 10025 | 35044 73773 | 15550 7462 206968 27.7 | 70.106 % | c | 10362 | 34754 73089 | 17105 7671 217020 28.3 | 71.113 % | c ============================================================================== c [1mFound solution: -30[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10418 | 34746 73026 | 11582 7715 217249 28.2 | 71.113 % | c | 10519 | 34708 72936 | 12740 7766 220611 28.4 | 71.286 % | c | 10669 | 34561 72582 | 14014 7879 225784 28.7 | 71.809 % | c | 10895 | 34561 72582 | 15415 8105 234073 28.9 | 71.809 % | c | 11232 | 34503 72446 | 16957 8415 250564 29.8 | 72.010 % | c | 11738 | 34040 71355 | 18652 8744 269440 30.8 | 73.746 % | c | 12497 | 33540 70146 | 20518 9112 292045 32.1 | 75.384 % | c | 13637 | 33245 69430 | 22570 10095 339815 33.7 | 76.437 % | c | 15346 | 33103 69093 | 24827 11789 430037 36.5 | 76.935 % | c | 17908 | 32838 68436 | 27309 14169 571943 40.4 | 77.900 % | c | 21752 | 32406 67389 | 30040 17744 810159 45.7 | 79.467 % | c ============================================================================== c [1mFound solution: -31[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25513 | 32400 67391 | 10800 21435 1132948 52.9 | 79.467 % | c | 25613 | 32400 67391 | 11880 21535 1137302 52.8 | 79.580 % | c | 25763 | 32297 67128 | 13068 21449 1138247 53.1 | 79.974 % | c | 25988 | 32297 67128 | 14374 21674 1153380 53.2 | 79.973 % | c | 26325 | 32226 66949 | 15812 21871 1164442 53.2 | 80.245 % | c | 26832 | 32226 66949 | 17393 22378 1189285 53.1 | 80.245 % | c | 27591 | 32203 66890 | 19132 23072 1220699 52.9 | 80.337 % | c | 28731 | 32203 66890 | 21046 24212 1292326 53.4 | 80.337 % | c | 30439 | 32177 66823 | 23150 25888 1432498 55.3 | 80.439 % | c | 33002 | 32174 66816 | 25465 28443 1544015 54.3 | 80.449 % | c | 36846 | 32165 66795 | 28012 32086 1770438 55.2 | 80.480 % | c | 42612 | 32165 66795 | 30813 37852 2233106 59.0 | 80.480 % | c ============================================================================== c [1mFound solution: -32[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49852 | 32020 66434 | 10673 44908 2776824 61.8 | 80.480 % | c | 49952 | 32020 66434 | 11740 16606 965248 58.1 | 81.008 % | c | 50103 | 32020 66434 | 12914 16757 968861 57.8 | 81.008 % | c | 50328 | 32020 66434 | 14205 16982 978993 57.6 | 81.008 % | c | 50665 | 32020 66434 | 15626 17319 1003362 57.9 | 81.008 % | c | 51172 | 32020 66434 | 17188 17826 1036082 58.1 | 81.008 % | c | 51931 | 31991 66359 | 18907 18574 1086045 58.5 | 81.121 % | c | 53070 | 31649 65547 | 20798 19664 1187670 60.4 | 82.297 % | c | 54779 | 31649 65547 | 22878 21373 1349706 63.2 | 82.297 % | c | 57343 | 31614 65464 | 25166 23929 1562175 65.3 | 82.420 % | c | 61188 | 31576 65372 | 27683 27752 1803243 65.0 | 82.553 % | c | 66954 | 31574 65368 | 30451 33497 2289530 68.4 | 82.558 % | c | 75604 | 31532 65264 | 33496 42137 3056028 72.5 | 82.716 % | c | 88578 | 31532 65264 | 36846 21336 1265506 59.3 | 82.716 % | c | 108040 | 31529 65257 | 40530 40797 2591421 63.5 | 82.727 % | c | 137232 | 31529 65257 | 44583 29377 1221521 41.6 | 82.727 % | c ============================================================================== c [1mFound solution: -33[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 148357 | 31547 65303 | 10515 40502 1622760 40.1 | 82.727 % | c | 148458 | 31547 65303 | 11566 17946 543672 30.3 | 82.688 % | c | 148609 | 31547 65303 | 12723 18097 548810 30.3 | 82.688 % | c | 148834 | 31547 65303 | 13995 18322 556443 30.4 | 82.688 % | c | 149172 | 31547 65303 | 15395 18660 571214 30.6 | 82.688 % | c | 149678 | 31547 65303 | 16934 19166 590946 30.8 | 82.688 % | c | 150437 | 31509 65208 | 18627 19917 627694 31.5 | 82.826 % | c | 151576 | 31503 65192 | 20490 21053 676051 32.1 | 82.852 % | c | 153284 | 31462 65089 | 22539 22760 774749 34.0 | 83.010 % | c | 155846 | 31462 65089 | 24793 25322 914275 36.1 | 83.010 % | c | 159690 | 31462 65089 | 27273 29166 1077698 37.0 | 83.010 % | c | 165456 | 31450 65059 | 30000 34929 1306380 37.4 | 83.056 % | c | 174105 | 31447 65052 | 33000 43576 1753198 40.2 | 83.066 % | c | 187079 | 31420 64985 | 36300 24815 994131 40.1 | 83.168 % | c | 206540 | 31420 64985 | 39930 44276 1745057 39.4 | 83.168 % | c | 235733 | 31410 64963 | 43923 34580 1120114 32.4 | 83.199 % | c | 279522 | 31398 64933 | 48316 36368 1076415 29.6 | 83.245 % | c | 345206 | 31387 64906 | 53147 56897 1731001 30.4 | 83.286 % | c ============================================================================== c [1mFound solution: -34[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 407607 | 31371 64837 | 10457 69202 2220207 32.1 | 83.286 % | c | 407708 | 31371 64837 | 11502 21207 509732 24.0 | 83.349 % | c | 407858 | 31371 64837 | 12652 21357 514760 24.1 | 83.349 % | c | 408084 | 31371 64837 | 13918 21583 523197 24.2 | 83.349 % | c | 408421 | 31371 64837 | 15310 21920 537769 24.5 | 83.349 % | c | 408927 | 31371 64837 | 16841 22426 560502 25.0 | 83.349 % | c | 409687 | 31341 64767 | 18525 23178 592062 25.5 | 83.446 % | c | 410826 | 31341 64767 | 20377 24317 636022 26.2 | 83.446 % | c | 412534 | 31341 64767 | 22415 26025 707984 27.2 | 83.446 % | c | 415097 | 31341 64767 | 24657 28588 779097 27.3 | 83.446 % | c | 418942 | 31341 64767 | 27122 32433 897343 27.7 | 83.446 % | c | 424708 | 31341 64767 | 29835 38199 1050979 27.5 | 83.446 % | c | 433357 | 31341 64767 | 32818 46848 1391591 29.7 | 83.446 % | c | 446331 | 31332 64746 | 36100 27082 843797 31.2 | 83.476 % | c | 465792 | 31329 64739 | 39710 46542 1633843 35.1 | 83.487 % | c | 494985 | 31256 64553 | 43681 39503 1039816 26.3 | 83.767 % | c | 538775 | 31101 64220 | 48049 32061 824480 25.7 | 83.982 % | c | 604460 | 30912 63770 | 52854 25803 577004 22.4 | 84.630 % | #### 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.91 0.90 2/54 1313 Raw data (stat): 1313 (runsolver) R 1311 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481107367 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.001 s] Raw data (loadavg): 0.87 0.91 0.90 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 2266 0 0 0 991 7 0 0 25 0 1 0 481107367 11571200 2237 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2825 2237 603 41 0 2784 0 vsize: 11300 [startup+20.0016 s] Raw data (loadavg): 0.89 0.91 0.90 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 2357 0 0 0 1990 8 0 0 25 0 1 0 481107367 11927552 2328 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2912 2328 603 41 0 2871 0 vsize: 11648 [startup+30.0023 s] Raw data (loadavg): 0.90 0.91 0.90 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 2796 0 0 0 2989 10 0 0 25 0 1 0 481107367 13664256 2767 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3336 2767 603 41 0 3295 0 vsize: 13344 [startup+40.0029 s] Raw data (loadavg): 0.92 0.92 0.90 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 3401 0 0 0 3985 13 0 0 25 0 1 0 481107367 16171008 3372 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3948 3372 603 41 0 3907 0 vsize: 15792 [startup+50.0035 s] Raw data (loadavg): 0.93 0.92 0.90 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 3893 0 0 0 4983 15 0 0 25 0 1 0 481107367 18173952 3864 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4437 3864 603 41 0 4396 0 vsize: 17748 [startup+60.0037 s] Raw data (loadavg): 0.94 0.92 0.90 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 4258 0 0 0 5982 16 0 0 25 0 1 0 481107367 19648512 4229 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4797 4229 603 41 0 4756 0 vsize: 19188 [startup+70.0036 s] Raw data (loadavg): 0.95 0.92 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 4688 0 0 0 6980 18 0 0 25 0 1 0 481107367 21499904 4659 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5249 4659 603 41 0 5208 0 vsize: 20996 [startup+80.0043 s] Raw data (loadavg): 0.96 0.92 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5055 0 0 0 7979 20 0 0 25 0 1 0 481107367 23097344 5026 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5639 5026 603 41 0 5598 0 vsize: 22556 [startup+90.0049 s] Raw data (loadavg): 0.96 0.93 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5400 0 0 0 8977 21 0 0 25 0 1 0 481107367 24596480 5371 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6005 5371 603 41 0 5964 0 vsize: 24020 [startup+100.004 s] Raw data (loadavg): 0.97 0.93 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5400 0 0 0 9977 21 0 0 25 0 1 0 481107367 24596480 5371 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6005 5371 603 41 0 5964 0 vsize: 24020 [startup+110.005 s] Raw data (loadavg): 0.97 0.93 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5400 0 0 0 10977 22 0 0 25 0 1 0 481107367 24596480 5371 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6005 5371 603 41 0 5964 0 vsize: 24020 [startup+120.004 s] Raw data (loadavg): 0.98 0.93 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5400 0 0 0 11976 22 0 0 25 0 1 0 481107367 24596480 5371 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6005 5371 603 41 0 5964 0 vsize: 24020 [startup+130.005 s] Raw data (loadavg): 0.98 0.93 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5476 0 0 0 12976 23 0 0 25 0 1 0 481107367 24866816 5447 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6071 5447 603 41 0 6030 0 vsize: 24284 [startup+140.006 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 5869 0 0 0 13974 25 0 0 25 0 1 0 481107367 26468352 5840 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6462 5840 603 41 0 6421 0 vsize: 25848 [startup+150.005 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6191 0 0 0 14973 26 0 0 25 0 1 0 481107367 27787264 6162 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6784 6162 603 41 0 6743 0 vsize: 27136 [startup+160.006 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 15971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223516 1075350660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7043 6414 603 41 0 7002 0 vsize: 28172 [startup+170.007 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 16971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7043 6414 603 41 0 7002 0 vsize: 28172 [startup+180.007 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 17971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6414 603 41 0 7002 0 vsize: 28172 [startup+190.007 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 18971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6414 603 41 0 7002 0 vsize: 28172 [startup+200.006 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 19971 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6414 603 41 0 7002 0 vsize: 28172 [startup+210.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 20972 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6414 603 41 0 7002 0 vsize: 28172 [startup+220.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6443 0 0 0 21972 28 0 0 25 0 1 0 481107367 28848128 6414 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6414 603 41 0 7002 0 vsize: 28172 [startup+230.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6447 0 0 0 22972 28 0 0 25 0 1 0 481107367 28848128 6418 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6418 603 41 0 7002 0 vsize: 28172 [startup+240.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6450 0 0 0 23972 28 0 0 25 0 1 0 481107367 28848128 6421 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6421 603 41 0 7002 0 vsize: 28172 [startup+250.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 24972 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+260.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 25973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+270.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 26973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+280.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 27973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+290.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 28973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+300.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 29973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+310.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 30973 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+320.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 31974 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+330.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 32974 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+340.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 33974 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+350.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 34974 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+360.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 35975 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+370.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 36975 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+380.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6459 0 0 0 37975 28 0 0 25 0 1 0 481107367 28848128 6430 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6430 603 41 0 7002 0 vsize: 28172 [startup+390.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 38975 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+400.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 39975 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+410.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 40975 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+420.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 41975 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+430.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 42976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+440.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 43976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223744 134559599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+450.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 44976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+460.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 45976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+470.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 46976 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+480.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 47977 28 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+490.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6462 0 0 0 48977 29 0 0 25 0 1 0 481107367 28848128 6433 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6433 603 41 0 7002 0 vsize: 28172 [startup+500.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6463 0 0 0 49977 29 0 0 25 0 1 0 481107367 28848128 6434 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6434 603 41 0 7002 0 vsize: 28172 [startup+510.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 50977 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6436 603 41 0 7002 0 vsize: 28172 [startup+520.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 51977 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223664 134559941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6436 603 41 0 7002 0 vsize: 28172 [startup+530.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 52977 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6436 603 41 0 7002 0 vsize: 28172 [startup+540.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 53977 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6436 603 41 0 7002 0 vsize: 28172 [startup+550.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 54978 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6436 603 41 0 7002 0 vsize: 28172 [startup+560.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 55978 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6436 603 41 0 7002 0 vsize: 28172 [startup+570.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 56978 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6436 603 41 0 7002 0 vsize: 28172 [startup+580.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6465 0 0 0 57978 29 0 0 25 0 1 0 481107367 28848128 6436 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6436 603 41 0 7002 0 vsize: 28172 [startup+590.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6466 0 0 0 58979 29 0 0 25 0 1 0 481107367 28848128 6437 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7043 6437 603 41 0 7002 0 vsize: 28172 [startup+600.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 59979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+610.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 60979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+620.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 61979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+630.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 62979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223744 134559512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+640.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 63979 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+650.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 64980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+660.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 65980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+670.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 66980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+680.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 67980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+690.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6469 0 0 0 68980 29 0 0 25 0 1 0 481107367 29110272 6440 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6440 603 41 0 7066 0 vsize: 28428 [startup+700.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6470 0 0 0 69980 29 0 0 25 0 1 0 481107367 29110272 6441 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6441 603 41 0 7066 0 vsize: 28428 [startup+710.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6473 0 0 0 70980 29 0 0 25 0 1 0 481107367 29110272 6444 4294967295 134512640 134672761 3221224560 3221223656 1075347344 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6444 603 41 0 7066 0 vsize: 28428 [startup+720.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 71981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+730.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 72981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+740.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 73981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+750.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 74981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+760.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 75981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+770.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 76981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+780.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 77982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+790.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 78982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+800.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 79982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+810.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 80982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+820.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 81982 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223712 134565212 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+830.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 82981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+840.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1313 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 83981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223696 134560716 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+850.01 s] Raw data (loadavg): 1.07 0.99 0.91 2/56 1361 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 84981 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+860.031 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 1367 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 85984 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+870.031 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 1367 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 86984 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+880.031 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 1367 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 87984 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134554910 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+890.032 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 1367 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 88984 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+900.031 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 1367 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 89985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+910.031 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 1367 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 90985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223744 134559514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+920.03 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 91985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+930.031 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 92985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+940.031 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 93985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+950.03 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 94985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+960.03 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 95985 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560492 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+970.03 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 96986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+980.03 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 97986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+990.031 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 98986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1000.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 99986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560483 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1010.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 100986 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1020.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 101987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1030.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 102987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1040.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 103987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1050.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 104987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1060.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 105987 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1070.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 106988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1080.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 107988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1090.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 108988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1100.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 109988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1110.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 110988 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1120.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 111989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1130.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 112989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1140.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 113989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1150.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 114989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1160.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 115989 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1170.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 116990 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1180.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 117990 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1190.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1369 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 118990 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 [startup+1200.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1371 Raw data (stat): 1313 (minisat+) R 1311 28099 28098 0 -1 0 6474 0 0 0 119990 29 0 0 25 0 1 0 481107367 29110272 6445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6445 603 41 0 7066 0 vsize: 28428 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 1.00 0.99 0.91 1/54 1371 Raw data (stat): 1313 (minisat+) Z 1311 28099 28098 0 -1 12 6477 0 0 0 119990 31 0 0 25 0 1 0 481107367 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.05 CPU time (s): 1200.22 CPU user time (s): 1199.91 CPU system time (s): 0.310952 CPU usage (%): 100.014 Max. virtual memory (Kb): 28428 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####