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 wulflinc2 THE 2005-04-13 21:29:45 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2885 boxname=wulflinc2 idbench=321 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 25457db86ce3cc3b7604dfa37c8096b4 /oldhome/oroussel/tmp/wulflinc2/normalized-frb35-17-3.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc2/normalized-frb35-17-3.opb IDLAUNCH: 2885 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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 : 2 cpu MHz : 451.191 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 909968 kB Buffers: 33696 kB Cached: 70408 kB SwapCached: 4 kB Active: 54792 kB Inactive: 52188 kB HighTotal: 131008 kB HighFree: 56756 kB LowTotal: 903652 kB LowFree: 853212 kB SwapTotal: 2097136 kB SwapFree: 2097132 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6916 kB Slab: 12228 kB Committed_AS: 71664 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 21:49:48 (client local time) WITH STATUS 10 IN 1200.09 SECONDS stats: 2885 7 1200.09 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.91 0.95 0.90 2/54 23099 Raw data (stat): 23099 (runsolver) R 23098 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420980506 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0007 s] Raw data (loadavg): 0.93 0.95 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 2294 0 0 0 992 7 0 0 25 0 1 0 420980506 11612160 2265 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2835 2265 603 41 0 2794 0 vsize: 11340 [startup+20.0018 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 2378 0 0 0 1991 7 0 0 25 0 1 0 420980506 12017664 2349 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2934 2349 603 41 0 2893 0 vsize: 11736 [startup+30.0027 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 2809 0 0 0 2990 9 0 0 25 0 1 0 420980506 13824000 2780 4294967295 134512640 134672761 3221224640 3221223800 134561238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3375 2780 603 41 0 3334 0 vsize: 13500 [startup+40.0029 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 3404 0 0 0 3987 11 0 0 25 0 1 0 420980506 16252928 3375 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3968 3375 603 41 0 3927 0 vsize: 15872 [startup+50.0036 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 3893 0 0 0 4986 12 0 0 25 0 1 0 420980506 18255872 3864 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4457 3864 603 41 0 4416 0 vsize: 17828 [startup+60.0038 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 4262 0 0 0 5984 14 0 0 25 0 1 0 420980506 19730432 4233 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4817 4233 603 41 0 4776 0 vsize: 19268 [startup+70.0049 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 4691 0 0 0 6983 15 0 0 25 0 1 0 420980506 21598208 4662 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5273 4662 603 41 0 5232 0 vsize: 21092 [startup+80.007 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 5058 0 0 0 7981 17 0 0 25 0 1 0 420980506 23060480 5029 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5630 5029 603 41 0 5589 0 vsize: 22520 [startup+90.0074 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 5422 0 0 0 8980 18 0 0 25 0 1 0 420980506 24678400 5393 4294967295 134512640 134672761 3221224640 3221223744 134554677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6025 5393 603 41 0 5984 0 vsize: 24100 [startup+100.007 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 5422 0 0 0 9980 18 0 0 25 0 1 0 420980506 24678400 5393 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6025 5393 603 41 0 5984 0 vsize: 24100 [startup+110.007 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 5422 0 0 0 10979 18 0 0 25 0 1 0 420980506 24678400 5393 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6025 5393 603 41 0 5984 0 vsize: 24100 [startup+120.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 5422 0 0 0 11979 18 0 0 25 0 1 0 420980506 24678400 5393 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6025 5393 603 41 0 5984 0 vsize: 24100 [startup+130.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 5447 0 0 0 12979 19 0 0 25 0 1 0 420980506 24678400 5418 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6025 5418 603 41 0 5984 0 vsize: 24100 [startup+140.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 5858 0 0 0 13976 21 0 0 25 0 1 0 420980506 26415104 5829 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6449 5829 603 41 0 6408 0 vsize: 25796 [startup+150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6177 0 0 0 14976 22 0 0 25 0 1 0 420980506 27738112 6148 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6772 6148 603 41 0 6731 0 vsize: 27088 [startup+160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6465 0 0 0 15975 22 0 0 25 0 1 0 420980506 28930048 6436 4294967295 134512640 134672761 3221224640 3221223744 134560287 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6436 603 41 0 7022 0 vsize: 28252 [startup+170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6465 0 0 0 16975 23 0 0 25 0 1 0 420980506 28930048 6436 4294967295 134512640 134672761 3221224640 3221223744 134560396 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6436 603 41 0 7022 0 vsize: 28252 [startup+180.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6465 0 0 0 17974 23 0 0 25 0 1 0 420980506 28930048 6436 4294967295 134512640 134672761 3221224640 3221223744 134560376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6436 603 41 0 7022 0 vsize: 28252 [startup+190.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6465 0 0 0 18974 23 0 0 25 0 1 0 420980506 28930048 6436 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6436 603 41 0 7022 0 vsize: 28252 [startup+200.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6465 0 0 0 19973 24 0 0 25 0 1 0 420980506 28930048 6436 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6436 603 41 0 7022 0 vsize: 28252 [startup+210.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6465 0 0 0 20973 24 0 0 25 0 1 0 420980506 28930048 6436 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6436 603 41 0 7022 0 vsize: 28252 [startup+220.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6465 0 0 0 21972 24 0 0 25 0 1 0 420980506 28930048 6436 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6436 603 41 0 7022 0 vsize: 28252 [startup+230.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6474 0 0 0 22972 25 0 0 25 0 1 0 420980506 28930048 6445 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6445 603 41 0 7022 0 vsize: 28252 [startup+240.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6477 0 0 0 23972 25 0 0 25 0 1 0 420980506 28930048 6448 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6448 603 41 0 7022 0 vsize: 28252 [startup+250.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 24972 25 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+260.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 25971 25 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+270.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 26971 26 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+280.017 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 27970 26 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+290.017 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 28970 26 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+300.017 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 29970 27 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+310.018 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 30969 27 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+320.018 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 31969 28 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+330.019 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 32969 28 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+340.02 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 33968 28 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+350.019 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 34967 29 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+360.02 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 35967 29 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134561226 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+370.021 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 36967 29 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+380.022 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 37966 30 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+390.022 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 38966 30 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+400.022 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 39966 30 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+410.022 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6481 0 0 0 40965 30 0 0 25 0 1 0 420980506 28930048 6452 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6452 603 41 0 7022 0 vsize: 28252 [startup+420.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6482 0 0 0 41965 30 0 0 25 0 1 0 420980506 28930048 6453 4294967295 134512640 134672761 3221224640 3221223824 134558856 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6453 603 41 0 7022 0 vsize: 28252 [startup+430.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6482 0 0 0 42965 30 0 0 25 0 1 0 420980506 28930048 6453 4294967295 134512640 134672761 3221224640 3221223744 134560224 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6453 603 41 0 7022 0 vsize: 28252 [startup+440.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6482 0 0 0 43966 30 0 0 25 0 1 0 420980506 28930048 6453 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6453 603 41 0 7022 0 vsize: 28252 [startup+450.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6482 0 0 0 44966 30 0 0 25 0 1 0 420980506 28930048 6453 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6453 603 41 0 7022 0 vsize: 28252 [startup+460.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6483 0 0 0 45966 30 0 0 25 0 1 0 420980506 28930048 6454 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6454 603 41 0 7022 0 vsize: 28252 [startup+470.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6483 0 0 0 46966 30 0 0 25 0 1 0 420980506 28930048 6454 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6454 603 41 0 7022 0 vsize: 28252 [startup+480.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6483 0 0 0 47966 30 0 0 25 0 1 0 420980506 28930048 6454 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6454 603 41 0 7022 0 vsize: 28252 [startup+490.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6483 0 0 0 48966 30 0 0 25 0 1 0 420980506 28930048 6454 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6454 603 41 0 7022 0 vsize: 28252 [startup+500.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6483 0 0 0 49967 30 0 0 25 0 1 0 420980506 28930048 6454 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6454 603 41 0 7022 0 vsize: 28252 [startup+510.026 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6486 0 0 0 50967 30 0 0 25 0 1 0 420980506 28930048 6457 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6457 603 41 0 7022 0 vsize: 28252 [startup+520.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6486 0 0 0 51967 30 0 0 25 0 1 0 420980506 28930048 6457 4294967295 134512640 134672761 3221224640 3221223776 134560579 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6457 603 41 0 7022 0 vsize: 28252 [startup+530.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6486 0 0 0 52968 30 0 0 25 0 1 0 420980506 28930048 6457 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6457 603 41 0 7022 0 vsize: 28252 [startup+540.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6486 0 0 0 53968 30 0 0 25 0 1 0 420980506 28930048 6457 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6457 603 41 0 7022 0 vsize: 28252 [startup+550.026 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6486 0 0 0 54968 30 0 0 25 0 1 0 420980506 28930048 6457 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6457 603 41 0 7022 0 vsize: 28252 [startup+560.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6486 0 0 0 55968 30 0 0 25 0 1 0 420980506 28930048 6457 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6457 603 41 0 7022 0 vsize: 28252 [startup+570.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6486 0 0 0 56968 30 0 0 25 0 1 0 420980506 28930048 6457 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6457 603 41 0 7022 0 vsize: 28252 [startup+580.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6486 0 0 0 57968 30 0 0 25 0 1 0 420980506 28930048 6457 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6457 603 41 0 7022 0 vsize: 28252 [startup+590.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6486 0 0 0 58969 30 0 0 25 0 1 0 420980506 28930048 6457 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6457 603 41 0 7022 0 vsize: 28252 [startup+600.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6487 0 0 0 59969 30 0 0 25 0 1 0 420980506 28930048 6458 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6458 603 41 0 7022 0 vsize: 28252 [startup+610.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 60969 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+620.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 61969 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+630.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 62969 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+640.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 63970 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+650.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 64970 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+660.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 65970 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223808 134560954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+670.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 66970 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+680.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 67970 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+690.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 68969 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+700.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6490 0 0 0 69969 31 0 0 25 0 1 0 420980506 29192192 6461 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6461 603 41 0 7086 0 vsize: 28508 [startup+710.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6491 0 0 0 70969 31 0 0 25 0 1 0 420980506 29192192 6462 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6462 603 41 0 7086 0 vsize: 28508 [startup+720.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 71969 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+730.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 72970 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+740.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 73970 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+750.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 74970 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+760.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 75970 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+770.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 76970 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+780.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 77970 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+790.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 78971 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+800.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 79971 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+810.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 80971 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+820.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 81971 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+830.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 82971 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+840.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 83971 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+850.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 84971 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223640 1075350790 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+860.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 85971 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223824 134558941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+870.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 86972 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+880.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 87972 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223824 134559031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+890.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 88972 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+900.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 89972 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+910.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 90972 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+920.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 91973 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+930.029 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 92973 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+940.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 93973 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223796 134565028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+950.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 94973 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+960.031 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 95973 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+970.031 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 96973 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+980.031 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 97974 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+990.031 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 98974 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1000.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 99974 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1010.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 100974 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223744 134560520 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1020.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 101974 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223776 134560673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1030.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 102975 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1040.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 103975 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1050.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 104975 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1060.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 105975 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1070.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 106975 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1080.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 107975 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1090.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 108976 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1100.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 109976 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1110.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 110976 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134559670 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1120.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 111976 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134561025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1130.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 112976 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1140.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 113977 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1150.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 114977 31 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1160.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 115976 32 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1170.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 116975 32 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1180.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 117975 32 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1190.04 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 118975 32 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 [startup+1200.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 23099 Raw data (stat): 23099 (minisat+) R 23098 20937 20936 0 -1 0 6495 0 0 0 119974 33 0 0 25 0 1 0 420980506 29192192 6466 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7127 6466 603 41 0 7086 0 vsize: 28508 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 1.00 0.99 0.91 1/54 23099 Raw data (stat): 23099 (minisat+) Z 23098 20937 20936 0 -1 12 6498 0 0 0 119974 34 0 0 25 0 1 0 420980506 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.09 CPU user time (s): 1199.75 CPU system time (s): 0.345947 CPU usage (%): 100.004 Max. virtual memory (Kb): 28508 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####