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 wulflinc24 THE 2005-05-27 05:30:38 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23075 boxname=wulflinc24 idbench=321 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 25457db86ce3cc3b7604dfa37c8096b4 /oldhome/oroussel/tmp/wulflinc24/normalized-frb35-17-3.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-frb35-17-3.opb IDLAUNCH: 23075 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 868192 kB Buffers: 33416 kB Cached: 111284 kB SwapCached: 616 kB Active: 53380 kB Inactive: 93364 kB HighTotal: 131008 kB HighFree: 40628 kB LowTotal: 903652 kB LowFree: 827564 kB SwapTotal: 2097892 kB SwapFree: 2096416 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5168 kB Slab: 14108 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 05:51:08 (client local time) WITH STATUS 152 IN 1229.84 SECONDS stats: 23075 7 1229.84 152 #### 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 379 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.95 0.90 2/54 375 Raw data (stat): 375 (runsolver) R 374 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853653440 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 0.93 0.95 0.90 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0008 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0022 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0027 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0032 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0034 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0045 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0046 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0048 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.71 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 379 Raw data (stat): 375 (minisat+_script) S 374 4613 4612 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853653440 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.71 CPU time (s): 1229.84 CPU user time (s): 1229.56 CPU system time (s): 0.285956 CPU usage (%): 100.011 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####