Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-5.opb |
MD5SUM | 70070c820bc7d178cc8f33b42e0deead |
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 | 28143 |
Number of constraints which are clauses | 28143 |
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 wulflinc19 THE 2005-04-14 02:50:51 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4459 boxname=wulflinc19 idbench=323 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 70070c820bc7d178cc8f33b42e0deead /oldhome/oroussel/tmp/wulflinc19/normalized-frb35-17-5.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-frb35-17-5.opb /oldhome/oroussel/tmp/wulflinc19/normalized-frb35-17-5.opb IDLAUNCH: 4459 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 878428 kB Buffers: 35420 kB Cached: 86856 kB SwapCached: 56 kB Active: 50148 kB Inactive: 75132 kB HighTotal: 131008 kB HighFree: 40152 kB LowTotal: 903652 kB LowFree: 838276 kB SwapTotal: 2097892 kB SwapFree: 2097836 kB Dirty: 28 kB Writeback: 0 kB Mapped: 7028 kB Slab: 25372 kB Committed_AS: 63708 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 03:10:53 (client local time) WITH STATUS 10 IN 1200.16 SECONDS stats: 4459 7 1200.16 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 28143 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 | 28143 56286 | 9381 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -21[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 | 56290 122394 | 18763 0 0 nan | 0.000 % | c | 100 | 55818 121416 | 20639 78 529 6.8 | 1.319 % | c | 250 | 55350 120416 | 22703 201 1432 7.1 | 2.831 % | c | 475 | 54323 118193 | 24973 376 3383 9.0 | 5.942 % | 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 | 678 | 53263 115977 | 17754 507 5021 9.9 | 5.942 % | c | 778 | 52841 115047 | 19529 588 6229 10.6 | 11.045 % | c | 928 | 52322 113884 | 21482 715 7585 10.6 | 12.707 % | c | 1153 | 51428 111886 | 23630 895 9815 11.0 | 15.557 % | c | 1490 | 49468 107434 | 25993 1105 12672 11.5 | 22.140 % | c | 1996 | 47638 103232 | 28592 1527 18207 11.9 | 28.026 % | c | 2756 | 44784 96705 | 31452 2088 27733 13.3 | 37.330 % | c | 3895 | 41359 88683 | 34597 2945 40667 13.8 | 48.818 % | 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 | 4578 | 40279 86235 | 13426 3372 48651 14.4 | 48.818 % | c | 4678 | 39986 85593 | 14768 3439 49906 14.5 | 53.601 % | c | 4828 | 39929 85464 | 16245 3585 53525 14.9 | 53.786 % | c | 5053 | 39738 84989 | 17870 3769 58890 15.6 | 54.485 % | c | 5390 | 39304 83962 | 19657 3970 63529 16.0 | 55.987 % | c | 5897 | 38689 82488 | 21622 4286 73190 17.1 | 58.330 % | c | 6656 | 37185 78940 | 23784 4674 86185 18.4 | 63.301 % | c | 7795 | 36622 77561 | 26163 5675 129966 22.9 | 65.275 % | c | 9504 | 35725 75401 | 28779 7136 192067 26.9 | 68.457 % | 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 | 10440 | 35152 73982 | 11717 7917 243425 30.7 | 68.457 % | c | 10540 | 35113 73891 | 12888 7988 246532 30.9 | 70.655 % | c | 10690 | 35113 73891 | 14177 8138 257579 31.7 | 70.655 % | c | 10915 | 35077 73801 | 15595 8322 262608 31.6 | 70.789 % | c | 11252 | 34978 73564 | 17154 8601 274225 31.9 | 71.134 % | 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 | 11391 | 34971 73570 | 11657 8688 275965 31.8 | 71.134 % | c | 11491 | 34902 73413 | 12822 8759 278380 31.8 | 71.445 % | c | 11641 | 34902 73413 | 14104 8909 284047 31.9 | 71.446 % | c | 11867 | 34896 73399 | 15515 9119 294059 32.2 | 71.466 % | c | 12204 | 34763 73092 | 17067 9394 321190 34.2 | 71.903 % | c | 12711 | 34609 72711 | 18773 9712 337264 34.7 | 72.472 % | c | 13470 | 34605 72698 | 20651 10457 386838 37.0 | 72.487 % | c | 14610 | 34380 72154 | 22716 11454 436165 38.1 | 73.293 % | c | 16319 | 33765 70670 | 24987 12907 541843 42.0 | 75.434 % | 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 | 16658 | 33651 70365 | 11217 13078 538486 41.2 | 75.434 % | c | 16758 | 33651 70365 | 12338 13178 543720 41.3 | 75.826 % | c | 16908 | 33598 70240 | 13572 13315 549004 41.2 | 76.011 % | c | 17133 | 33492 69992 | 14929 13474 555912 41.3 | 76.371 % | c | 17471 | 33492 69992 | 16422 13812 572516 41.5 | 76.370 % | c | 17978 | 33390 69747 | 18065 14288 590646 41.3 | 76.730 % | c | 18737 | 33266 69453 | 19871 15005 645411 43.0 | 77.151 % | c | 19876 | 33263 69446 | 21858 16138 775398 48.0 | 77.161 % | c | 21586 | 33025 68873 | 24044 17787 883974 49.7 | 78.013 % | c | 24149 | 33025 68873 | 26449 20350 1110021 54.5 | 78.013 % | c | 27994 | 33025 68873 | 29094 24195 1446802 59.8 | 78.013 % | c | 33762 | 32912 68606 | 32003 29913 1976061 66.1 | 78.408 % | c | 42412 | 32688 68047 | 35203 38230 2602127 68.1 | 79.250 % | 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 | 54813 | 32709 68118 | 10903 50607 3631857 71.8 | 79.250 % | c | 54913 | 32665 68010 | 11993 17614 1027595 58.3 | 79.420 % | c | 55063 | 32665 68010 | 13192 17764 1033328 58.2 | 79.420 % | c | 55288 | 32632 67926 | 14511 17973 1042889 58.0 | 79.537 % | c | 55625 | 32632 67926 | 15963 18310 1077898 58.9 | 79.537 % | c | 56133 | 32626 67909 | 17559 18796 1115938 59.4 | 79.563 % | c | 56892 | 32626 67909 | 19315 19555 1163074 59.5 | 79.563 % | c | 58031 | 32585 67812 | 21246 20688 1247141 60.3 | 79.706 % | c | 59739 | 32585 67812 | 23371 22396 1358285 60.6 | 79.706 % | 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 | 61766 | 32459 67492 | 10819 24393 1480169 60.7 | 79.706 % | c | 61866 | 32459 67492 | 11900 24493 1483862 60.6 | 80.152 % | c | 62016 | 32422 67401 | 13090 24627 1493869 60.7 | 80.285 % | c | 62241 | 32400 67340 | 14400 24844 1515014 61.0 | 80.372 % | c | 62579 | 32361 67247 | 15840 25167 1534905 61.0 | 80.510 % | c | 63085 | 32361 67247 | 17424 25673 1569859 61.1 | 80.510 % | c | 63845 | 32361 67247 | 19166 26433 1617338 61.2 | 80.510 % | c | 64985 | 32361 67247 | 21083 27573 1724425 62.5 | 80.510 % | c | 66693 | 32361 67247 | 23191 29281 1823567 62.3 | 80.510 % | c | 69255 | 32361 67247 | 25510 31843 2022398 63.5 | 80.510 % | c | 73099 | 32266 67009 | 28061 35630 2258988 63.4 | 80.852 % | c | 78867 | 32266 67009 | 30867 41398 2541641 61.4 | 80.852 % | c | 87517 | 32261 66998 | 33954 17592 605784 34.4 | 80.868 % | c | 100493 | 32145 66707 | 37350 30555 1527180 50.0 | 81.251 % | c | 119954 | 32136 66686 | 41085 50010 2776028 55.5 | 81.282 % | c | 149146 | 32059 66501 | 45193 39406 2390640 60.7 | 81.558 % | c | 192935 | 32018 66406 | 49713 40611 2365930 58.3 | 81.696 % | 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 | 234340 | 31964 66282 | 10654 33803 1904300 56.3 | 81.696 % | c | 234440 | 31964 66282 | 11719 16070 660384 41.1 | 81.909 % | c | 234590 | 31939 66229 | 12891 16216 667281 41.1 | 81.980 % | c | 234817 | 31939 66229 | 14180 16443 680004 41.4 | 81.980 % | c | 235155 | 31853 66019 | 15598 16755 688813 41.1 | 82.286 % | c | 235661 | 31853 66019 | 17158 17261 714839 41.4 | 82.286 % | c | 236420 | 31848 66006 | 18874 18019 754497 41.9 | 82.307 % | c | 237559 | 31848 66006 | 20761 19158 827477 43.2 | 82.307 % | c | 239268 | 31848 66006 | 22837 20867 941214 45.1 | 82.307 % | c | 241830 | 31845 65999 | 25121 23424 1134066 48.4 | 82.317 % | c | 245674 | 31832 65966 | 27633 27261 1379284 50.6 | 82.368 % | c | 251442 | 31821 65939 | 30397 33025 1770495 53.6 | 82.409 % | c | 260091 | 31723 65693 | 33436 41618 2363593 56.8 | 82.781 % | c | 273065 | 31702 65642 | 36780 21888 1194237 54.6 | 82.858 % | c | 292526 | 31595 65388 | 40458 41329 2455787 59.4 | 83.236 % | c | 321718 | 31590 65375 | 44504 31574 1206245 38.2 | 83.256 % | c | 365507 | 31587 65368 | 48954 33871 1201100 35.5 | 83.266 % | c | 431191 | 31587 65368 | 53850 55118 1835677 33.3 | 83.266 % | c | 529717 | 31516 65201 | 59235 54938 1748182 31.8 | 83.511 % | #### 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.91 2/55 28868 Raw data (stat): 28868 (runsolver) R 28867 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481122040 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0003 s] Raw data (loadavg): 0.93 0.95 0.91 2/55 28868 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 2262 0 0 0 991 6 0 0 25 0 1 0 481122040 11530240 2240 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2815 2240 603 41 0 2774 0 vsize: 11260 [startup+20.0008 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 2383 0 0 0 1990 7 0 0 25 0 1 0 481122040 11943936 2361 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2916 2361 603 41 0 2875 0 vsize: 11664 [startup+30.0014 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 2868 0 0 0 2988 9 0 0 25 0 1 0 481122040 13983744 2846 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3414 2846 603 41 0 3373 0 vsize: 13656 [startup+40.0015 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 3442 0 0 0 3985 11 0 0 25 0 1 0 481122040 16388096 3420 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4001 3420 603 41 0 3960 0 vsize: 16004 [startup+50.0026 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 4029 0 0 0 4984 13 0 0 25 0 1 0 481122040 18796544 4007 4294967295 134512640 134672761 3221224560 3221223744 134558851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4589 4007 603 41 0 4548 0 vsize: 18356 [startup+60.0027 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 4594 0 0 0 5983 14 0 0 25 0 1 0 481122040 21069824 4572 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5144 4572 603 41 0 5103 0 vsize: 20576 [startup+70.0028 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 4983 0 0 0 6982 15 0 0 25 0 1 0 481122040 22806528 4961 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5568 4961 603 41 0 5527 0 vsize: 22272 [startup+80.0034 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 5381 0 0 0 7981 16 0 0 25 0 1 0 481122040 24403968 5359 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5958 5359 603 41 0 5917 0 vsize: 23832 [startup+90.0032 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 5783 0 0 0 8980 17 0 0 25 0 1 0 481122040 26001408 5761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6348 5761 603 41 0 6307 0 vsize: 25392 [startup+100.003 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6191 0 0 0 9978 19 0 0 25 0 1 0 481122040 27607040 6169 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6740 6169 603 41 0 6699 0 vsize: 26960 [startup+110.004 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6299 0 0 0 10978 19 0 0 25 0 1 0 481122040 28106752 6277 4294967295 134512640 134672761 3221224560 3221223628 1075346603 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6862 6277 603 41 0 6821 0 vsize: 27448 [startup+120.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 11978 19 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+130.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 12978 19 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+140.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 13978 20 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+150.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 14978 20 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 15977 20 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+170.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 16977 21 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 17977 21 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 18977 21 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+200.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 19976 22 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 20976 22 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+220.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 21976 22 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6320 0 0 0 22976 22 0 0 25 0 1 0 481122040 28266496 6298 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6298 603 41 0 6860 0 vsize: 27604 [startup+240.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6324 0 0 0 23976 22 0 0 25 0 1 0 481122040 28266496 6302 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6302 603 41 0 6860 0 vsize: 27604 [startup+250.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6327 0 0 0 24976 23 0 0 25 0 1 0 481122040 28266496 6305 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6305 603 41 0 6860 0 vsize: 27604 [startup+260.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6327 0 0 0 25975 23 0 0 25 0 1 0 481122040 28266496 6305 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6901 6305 603 41 0 6860 0 vsize: 27604 [startup+270.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6327 0 0 0 26975 23 0 0 25 0 1 0 481122040 28266496 6305 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6901 6305 603 41 0 6860 0 vsize: 27604 [startup+280.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6327 0 0 0 27975 23 0 0 25 0 1 0 481122040 28266496 6305 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6901 6305 603 41 0 6860 0 vsize: 27604 [startup+290.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6327 0 0 0 28976 23 0 0 25 0 1 0 481122040 28266496 6305 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6901 6305 603 41 0 6860 0 vsize: 27604 [startup+300.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6327 0 0 0 29976 24 0 0 25 0 1 0 481122040 28266496 6305 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6901 6305 603 41 0 6860 0 vsize: 27604 [startup+310.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28870 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6327 0 0 0 30976 24 0 0 25 0 1 0 481122040 28266496 6305 4294967295 134512640 134672761 3221224560 3221223664 134559979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6901 6305 603 41 0 6860 0 vsize: 27604 [startup+320.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6332 0 0 0 31976 24 0 0 25 0 1 0 481122040 28266496 6310 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6901 6310 603 41 0 6860 0 vsize: 27604 [startup+330.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6345 0 0 0 32976 24 0 0 25 0 1 0 481122040 28266496 6323 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6901 6323 603 41 0 6860 0 vsize: 27604 [startup+340.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6361 0 0 0 33976 24 0 0 25 0 1 0 481122040 28413952 6339 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6937 6339 603 41 0 6896 0 vsize: 27748 [startup+350.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6469 0 0 0 34976 24 0 0 25 0 1 0 481122040 28811264 6447 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7034 6447 603 41 0 6993 0 vsize: 28136 [startup+360.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6678 0 0 0 35976 24 0 0 25 0 1 0 481122040 29741056 6656 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7261 6656 603 41 0 7220 0 vsize: 29044 [startup+370.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6678 0 0 0 36976 24 0 0 25 0 1 0 481122040 29741056 6656 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7261 6656 603 41 0 7220 0 vsize: 29044 [startup+380.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6678 0 0 0 37976 24 0 0 25 0 1 0 481122040 29741056 6656 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7261 6656 603 41 0 7220 0 vsize: 29044 [startup+390.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6683 0 0 0 38976 25 0 0 25 0 1 0 481122040 29741056 6661 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7261 6661 603 41 0 7220 0 vsize: 29044 [startup+400.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6691 0 0 0 39976 25 0 0 25 0 1 0 481122040 29741056 6669 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7261 6669 603 41 0 7220 0 vsize: 29044 [startup+410.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6691 0 0 0 40977 25 0 0 25 0 1 0 481122040 29741056 6669 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7261 6669 603 41 0 7220 0 vsize: 29044 [startup+420.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6693 0 0 0 41977 25 0 0 25 0 1 0 481122040 29741056 6671 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7261 6671 603 41 0 7220 0 vsize: 29044 [startup+430.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 6888 0 0 0 42976 25 0 0 25 0 1 0 481122040 30552064 6866 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7459 6866 603 41 0 7418 0 vsize: 29836 [startup+440.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7261 0 0 0 43976 26 0 0 25 0 1 0 481122040 32157696 7239 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7851 7239 603 41 0 7810 0 vsize: 31404 [startup+450.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7599 0 0 0 44975 27 0 0 25 0 1 0 481122040 33492992 7577 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8177 7577 603 41 0 8136 0 vsize: 32708 [startup+460.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 45974 28 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+470.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 46974 28 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+480.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 47975 28 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+490.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 48975 28 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223664 134559922 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+500.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 49975 28 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+510.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 50975 28 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+520.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 51974 28 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+530.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 52974 28 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+540.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 53974 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+550.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28872 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 54975 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223664 134560180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+560.015 s] Raw data (loadavg): 1.30 1.04 0.93 2/55 28925 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 55973 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+570.014 s] Raw data (loadavg): 1.25 1.03 0.93 2/55 28925 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 56973 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+580.015 s] Raw data (loadavg): 1.21 1.03 0.93 2/55 28925 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 57974 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223744 134559596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+590.015 s] Raw data (loadavg): 1.18 1.03 0.93 2/55 28925 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 58974 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+600.015 s] Raw data (loadavg): 1.15 1.03 0.93 2/55 28925 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 59974 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+610.017 s] Raw data (loadavg): 1.13 1.03 0.93 2/55 28925 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 60974 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+620.016 s] Raw data (loadavg): 1.11 1.03 0.93 2/55 28927 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 61974 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+630.016 s] Raw data (loadavg): 1.09 1.03 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 62975 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+640.016 s] Raw data (loadavg): 1.08 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7754 0 0 0 63975 29 0 0 25 0 1 0 481122040 34414592 7732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7732 603 41 0 8361 0 vsize: 33608 [startup+650.016 s] Raw data (loadavg): 1.06 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7755 0 0 0 64975 29 0 0 25 0 1 0 481122040 34414592 7733 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7733 603 41 0 8361 0 vsize: 33608 [startup+660.016 s] Raw data (loadavg): 1.05 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7755 0 0 0 65975 29 0 0 25 0 1 0 481122040 34414592 7733 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7733 603 41 0 8361 0 vsize: 33608 [startup+670.016 s] Raw data (loadavg): 1.04 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7755 0 0 0 66975 29 0 0 25 0 1 0 481122040 34414592 7733 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7733 603 41 0 8361 0 vsize: 33608 [startup+680.017 s] Raw data (loadavg): 1.04 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7755 0 0 0 67975 29 0 0 25 0 1 0 481122040 34414592 7733 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7733 603 41 0 8361 0 vsize: 33608 [startup+690.017 s] Raw data (loadavg): 1.03 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7755 0 0 0 68976 29 0 0 25 0 1 0 481122040 34414592 7733 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7733 603 41 0 8361 0 vsize: 33608 [startup+700.017 s] Raw data (loadavg): 1.03 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7755 0 0 0 69976 29 0 0 25 0 1 0 481122040 34414592 7733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7733 603 41 0 8361 0 vsize: 33608 [startup+710.017 s] Raw data (loadavg): 1.02 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7755 0 0 0 70976 29 0 0 25 0 1 0 481122040 34414592 7733 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7733 603 41 0 8361 0 vsize: 33608 [startup+720.017 s] Raw data (loadavg): 1.02 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7755 0 0 0 71976 29 0 0 25 0 1 0 481122040 34414592 7733 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7733 603 41 0 8361 0 vsize: 33608 [startup+730.017 s] Raw data (loadavg): 1.01 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7755 0 0 0 72976 29 0 0 25 0 1 0 481122040 34414592 7733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7733 603 41 0 8361 0 vsize: 33608 [startup+740.018 s] Raw data (loadavg): 1.01 1.02 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7756 0 0 0 73976 29 0 0 25 0 1 0 481122040 34414592 7734 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7734 603 41 0 8361 0 vsize: 33608 [startup+750.019 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7756 0 0 0 74976 29 0 0 25 0 1 0 481122040 34414592 7734 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7734 603 41 0 8361 0 vsize: 33608 [startup+760.019 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7756 0 0 0 75977 29 0 0 25 0 1 0 481122040 34414592 7734 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7734 603 41 0 8361 0 vsize: 33608 [startup+770.019 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7756 0 0 0 76977 29 0 0 25 0 1 0 481122040 34414592 7734 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7734 603 41 0 8361 0 vsize: 33608 [startup+780.019 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7756 0 0 0 77977 29 0 0 25 0 1 0 481122040 34414592 7734 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7734 603 41 0 8361 0 vsize: 33608 [startup+790.019 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7756 0 0 0 78977 29 0 0 25 0 1 0 481122040 34414592 7734 4294967295 134512640 134672761 3221224560 3221223744 134558651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7734 603 41 0 8361 0 vsize: 33608 [startup+800.02 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7758 0 0 0 79977 29 0 0 25 0 1 0 481122040 34414592 7736 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7736 603 41 0 8361 0 vsize: 33608 [startup+810.019 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 80977 29 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+820.02 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 81977 29 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+830.02 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 82978 30 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+840.02 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 83978 30 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+850.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 84978 30 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+860.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28929 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 85978 30 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+870.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28931 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 86978 30 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+880.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28931 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 87978 30 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+890.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28931 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 88978 30 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+900.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28931 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7759 0 0 0 89978 30 0 0 25 0 1 0 481122040 34414592 7737 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7737 603 41 0 8361 0 vsize: 33608 [startup+910.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28931 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7761 0 0 0 90978 30 0 0 25 0 1 0 481122040 34414592 7739 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7739 603 41 0 8361 0 vsize: 33608 [startup+920.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 91978 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+930.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 92979 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+940.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 93979 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223696 134560703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+950.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 94979 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+960.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 95979 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+970.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 96979 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+980.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 97979 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+990.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 98979 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1000.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 99980 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1010.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 100980 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1020.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 101980 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1030.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 102980 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1040.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 103980 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1050.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 104980 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1060.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 105981 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1070.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 106981 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1080.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 107981 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1090.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 108981 30 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1100.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 109981 31 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1110.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 110981 31 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1120.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 111981 31 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1130.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7763 0 0 0 112981 31 0 0 25 0 1 0 481122040 34414592 7741 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7741 603 41 0 8361 0 vsize: 33608 [startup+1140.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7765 0 0 0 113981 31 0 0 25 0 1 0 481122040 34414592 7743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7743 603 41 0 8361 0 vsize: 33608 [startup+1150.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7768 0 0 0 114981 31 0 0 25 0 1 0 481122040 34414592 7746 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7746 603 41 0 8361 0 vsize: 33608 [startup+1160.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7768 0 0 0 115981 31 0 0 25 0 1 0 481122040 34414592 7746 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7746 603 41 0 8361 0 vsize: 33608 [startup+1170.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7768 0 0 0 116981 31 0 0 25 0 1 0 481122040 34414592 7746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7746 603 41 0 8361 0 vsize: 33608 [startup+1180.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7768 0 0 0 117981 31 0 0 25 0 1 0 481122040 34414592 7746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7746 603 41 0 8361 0 vsize: 33608 [startup+1190.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7768 0 0 0 118982 31 0 0 25 0 1 0 481122040 34414592 7746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7746 603 41 0 8361 0 vsize: 33608 [startup+1200.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28933 Raw data (stat): 28868 (minisat+) R 28867 22929 22928 0 -1 0 7768 0 0 0 119982 31 0 0 25 0 1 0 481122040 34414592 7746 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8402 7746 603 41 0 8361 0 vsize: 33608 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 1.00 1.00 0.93 1/55 28933 Raw data (stat): 28868 (minisat+) Z 28867 22929 22928 0 -1 12 7771 0 0 0 119982 33 0 0 25 0 1 0 481122040 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.05 CPU time (s): 1200.16 CPU user time (s): 1199.83 CPU system time (s): 0.333949 CPU usage (%): 100.009 Max. virtual memory (Kb): 33608 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####