Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-4.opb |
MD5SUM | 615f734b8951521e89cf22f42d6d26cc |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -30 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 450 |
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 | 450 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 450 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.05084 |
Number of variables | 450 |
Total number of constraints | 17831 |
Number of constraints which are clauses | 17831 |
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 wulflinc9 THE 2005-04-14 04:33:29 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4829 boxname=wulflinc9 idbench=317 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 615f734b8951521e89cf22f42d6d26cc /oldhome/oroussel/tmp/wulflinc9/normalized-frb30-15-4.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc9/normalized-frb30-15-4.opb /oldhome/oroussel/tmp/wulflinc9/normalized-frb30-15-4.opb IDLAUNCH: 4829 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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: 888496 kB Buffers: 36600 kB Cached: 89044 kB SwapCached: 564 kB Active: 54940 kB Inactive: 74168 kB HighTotal: 131008 kB HighFree: 38024 kB LowTotal: 903652 kB LowFree: 850472 kB SwapTotal: 2097136 kB SwapFree: 2096572 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 11420 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 04:53:41 (client local time) WITH STATUS 10 IN 1209.96 SECONDS stats: 4829 7 1209.96 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 17831 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 | 17831 35662 | 5943 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -22[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:16912 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 52019 115771 | 17339 0 0 nan | 0.000 % | c | 100 | 51519 114636 | 19072 83 569 6.9 | 1.596 % | c | 250 | 50271 111802 | 20980 194 1293 6.7 | 4.362 % | c | 475 | 48358 107437 | 23078 369 3275 8.9 | 9.245 % | c ============================================================================== c [1mFound solution: -23[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 | 773 | 46950 104312 | 15650 607 5979 9.9 | 9.245 % | c | 873 | 45521 101018 | 17215 668 6806 10.2 | 17.705 % | c | 1025 | 44598 98886 | 18936 796 8486 10.7 | 20.161 % | c | 1250 | 43104 95436 | 20830 966 9892 10.2 | 24.158 % | c | 1587 | 40405 89151 | 22913 1175 13250 11.3 | 31.685 % | c | 2093 | 36538 80178 | 25204 1515 18247 12.0 | 41.888 % | c | 2852 | 33640 73384 | 27724 2064 24505 11.9 | 50.178 % | c | 3991 | 30079 65045 | 30497 2904 38939 13.4 | 60.474 % | c ============================================================================== c [1mFound solution: -24[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 | 4098 | 29253 63066 | 9751 2891 38642 13.4 | 60.474 % | c | 4198 | 29028 62535 | 10726 2980 40140 13.5 | 63.520 % | c | 4348 | 28037 60215 | 11798 2983 41845 14.0 | 66.382 % | c | 4573 | 27892 59877 | 12978 3165 44262 14.0 | 66.772 % | c | 4910 | 27892 59877 | 14276 3502 53627 15.3 | 66.771 % | c | 5416 | 27793 59647 | 15704 3969 66696 16.8 | 67.051 % | c ============================================================================== c [1mFound solution: -25[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 | 5746 | 27665 59362 | 9221 4250 76780 18.1 | 67.051 % | c | 5847 | 27659 59348 | 10143 4346 78774 18.1 | 67.599 % | c | 5998 | 27586 59178 | 11157 4484 81221 18.1 | 67.810 % | c | 6223 | 27570 59140 | 12273 4705 89755 19.1 | 67.861 % | c | 6560 | 27308 58522 | 13500 4945 103445 20.9 | 68.613 % | c | 7066 | 27019 57835 | 14850 5349 115694 21.6 | 69.491 % | 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 | 7303 | 26724 57117 | 8908 5505 125234 22.7 | 69.491 % | c | 7403 | 26586 56791 | 9798 5593 129533 23.2 | 70.687 % | c | 7555 | 26586 56791 | 10778 5745 136110 23.7 | 70.687 % | c | 7781 | 26582 56782 | 11856 5968 146214 24.5 | 70.695 % | c | 8118 | 25801 54946 | 13042 5969 150835 25.3 | 72.993 % | 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 | 8536 | 25888 55171 | 8629 6387 174079 27.3 | 72.993 % | c | 8636 | 25819 55007 | 9491 6471 176118 27.2 | 73.206 % | c | 8786 | 25698 54726 | 10441 6479 179794 27.8 | 73.533 % | c | 9011 | 25226 53608 | 11485 6591 183992 27.9 | 74.975 % | c | 9348 | 25216 53585 | 12633 6920 196171 28.3 | 75.000 % | c | 9854 | 25216 53585 | 13897 7426 225313 30.3 | 75.000 % | c | 10614 | 25206 53562 | 15286 8179 258486 31.6 | 75.025 % | c | 11754 | 24582 52100 | 16815 8924 296829 33.3 | 76.878 % | c | 13465 | 24011 50754 | 18497 10225 377735 36.9 | 78.571 % | c | 16027 | 23884 50455 | 20346 12688 534488 42.1 | 78.949 % | c | 19871 | 23838 50347 | 22381 16443 704895 42.9 | 79.083 % | c | 25637 | 23621 49836 | 24619 22126 972380 43.9 | 79.737 % | c | 34288 | 23318 49115 | 27081 30477 1323824 43.4 | 80.710 % | c | 47262 | 23276 49017 | 29789 21542 792092 36.8 | 80.827 % | 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 | 56388 | 23254 48945 | 7751 30665 1113463 36.3 | 80.827 % | c | 56489 | 23254 48945 | 8526 15162 455183 30.0 | 80.889 % | c | 56639 | 23254 48945 | 9378 15312 459283 30.0 | 80.889 % | c | 56864 | 23254 48945 | 10316 15537 466427 30.0 | 80.889 % | c | 57201 | 23254 48945 | 11348 15874 479204 30.2 | 80.889 % | c | 57707 | 23248 48931 | 12483 16376 493517 30.1 | 80.906 % | c | 58466 | 23248 48931 | 13731 17135 518587 30.3 | 80.906 % | c | 59605 | 23201 48821 | 15104 18267 551224 30.2 | 81.048 % | c | 61313 | 23201 48821 | 16614 19975 593871 29.7 | 81.048 % | c | 63875 | 23201 48821 | 18276 22537 667223 29.6 | 81.048 % | c | 67720 | 23027 48410 | 20104 26334 871844 33.1 | 81.593 % | c | 73486 | 23027 48410 | 22114 16850 569285 33.8 | 81.593 % | c | 82135 | 22975 48287 | 24325 25485 894618 35.1 | 81.752 % | c | 95109 | 22969 48273 | 26758 19203 511484 26.6 | 81.769 % | c | 114570 | 22969 48273 | 29434 18246 466877 25.6 | 81.769 % | c ============================================================================== c [1mFound solution: -29[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:12846 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 137455 | 43385 96013 | 14461 24890 966876 38.8 | 81.769 % | c | 137555 | 43385 96013 | 15907 12545 412381 32.9 | 53.716 % | c | 137705 | 43385 96013 | 17497 12695 419114 33.0 | 53.716 % | c | 137930 | 43385 96013 | 19247 12920 427539 33.1 | 53.716 % | c | 138267 | 43385 96013 | 21172 13257 443447 33.5 | 53.716 % | c | 138775 | 43385 96013 | 23289 13765 459548 33.4 | 53.716 % | c | 139534 | 43330 95885 | 25618 14518 489011 33.7 | 53.814 % | c | 140673 | 43330 95885 | 28180 15657 526636 33.6 | 53.814 % | c | 142381 | 43303 95825 | 30998 17364 586979 33.8 | 53.850 % | c | 144943 | 43207 95608 | 34098 19918 687613 34.5 | 53.989 % | c | 148787 | 43207 95608 | 37508 23762 815394 34.3 | 53.989 % | c | 154554 | 43150 95472 | 41258 29517 1001742 33.9 | 54.103 % | c | 163203 | 43103 95366 | 45384 38165 1250686 32.8 | 54.170 % | c | 176177 | 42479 93940 | 49923 51122 1703422 33.3 | 55.138 % | c | 195639 | 42432 93838 | 54915 25328 652896 25.8 | 55.216 % | c | 224831 | 42209 93338 | 60407 54502 1893898 34.7 | 55.566 % | c | 268623 | 41957 92767 | 66447 43906 1668331 38.0 | 55.989 % | c | 334307 | 41744 92285 | 73092 52501 1525564 29.1 | 56.314 % | c | 432833 | 41261 91190 | 80401 83434 2599920 31.2 | 57.066 % | #### 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.88 0.97 0.91 2/54 4306 Raw data (stat): 4306 (runsolver) R 4305 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423521486 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0003 s] Raw data (loadavg): 0.90 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 1627 0 0 0 995 3 0 0 25 0 1 0 423521486 8572928 1605 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2093 1605 603 41 0 2052 0 vsize: 8372 [startup+20.0016 s] Raw data (loadavg): 0.91 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 2168 0 0 0 1993 5 0 0 25 0 1 0 423521486 10809344 2146 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2639 2146 603 41 0 2598 0 vsize: 10556 [startup+30.0028 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 2633 0 0 0 2990 7 0 0 25 0 1 0 423521486 12795904 2611 4294967295 134512640 134672761 3221224560 3221223744 134559334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3124 2611 603 41 0 3083 0 vsize: 12496 [startup+40.0026 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 2966 0 0 0 3989 8 0 0 25 0 1 0 423521486 14143488 2944 4294967295 134512640 134672761 3221224560 3221223800 134558237 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3453 2944 603 41 0 3412 0 vsize: 13812 [startup+50.0029 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3336 0 0 0 4987 10 0 0 25 0 1 0 423521486 15736832 3314 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3842 3314 603 41 0 3801 0 vsize: 15368 [startup+60.0031 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3567 0 0 0 5986 11 0 0 25 0 1 0 423521486 16674816 3545 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3545 603 41 0 4030 0 vsize: 16284 [startup+70.0049 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3567 0 0 0 6986 11 0 0 25 0 1 0 423521486 16674816 3545 4294967295 134512640 134672761 3221224560 3221223744 134559321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3545 603 41 0 4030 0 vsize: 16284 [startup+80.0052 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3572 0 0 0 7985 12 0 0 25 0 1 0 423521486 16674816 3550 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3550 603 41 0 4030 0 vsize: 16284 [startup+90.0054 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3573 0 0 0 8985 12 0 0 25 0 1 0 423521486 16674816 3551 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3551 603 41 0 4030 0 vsize: 16284 [startup+100.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3574 0 0 0 9985 12 0 0 25 0 1 0 423521486 16674816 3552 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3552 603 41 0 4030 0 vsize: 16284 [startup+110.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3574 0 0 0 10984 13 0 0 25 0 1 0 423521486 16674816 3552 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3552 603 41 0 4030 0 vsize: 16284 [startup+120.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3574 0 0 0 11984 13 0 0 25 0 1 0 423521486 16674816 3552 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3552 603 41 0 4030 0 vsize: 16284 [startup+130.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3574 0 0 0 12983 14 0 0 25 0 1 0 423521486 16674816 3552 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3552 603 41 0 4030 0 vsize: 16284 [startup+140.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3580 0 0 0 13983 14 0 0 25 0 1 0 423521486 16674816 3558 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3558 603 41 0 4030 0 vsize: 16284 [startup+150.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3589 0 0 0 14983 14 0 0 25 0 1 0 423521486 16674816 3567 4294967295 134512640 134672761 3221224560 3221223664 134560250 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4071 3567 603 41 0 4030 0 vsize: 16284 [startup+160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3593 0 0 0 15982 15 0 0 25 0 1 0 423521486 16838656 3571 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4111 3571 603 41 0 4070 0 vsize: 16444 [startup+170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3594 0 0 0 16981 15 0 0 25 0 1 0 423521486 16838656 3572 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4111 3572 603 41 0 4070 0 vsize: 16444 [startup+180.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3594 0 0 0 17981 15 0 0 25 0 1 0 423521486 16838656 3572 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4111 3572 603 41 0 4070 0 vsize: 16444 [startup+190.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3594 0 0 0 18981 16 0 0 25 0 1 0 423521486 16838656 3572 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4111 3572 603 41 0 4070 0 vsize: 16444 [startup+200.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 19980 16 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4418 3834 603 41 0 4377 0 vsize: 17672 [startup+210.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 20980 16 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4418 3834 603 41 0 4377 0 vsize: 17672 [startup+220.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 21980 17 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4418 3834 603 41 0 4377 0 vsize: 17672 [startup+230.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 22979 17 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4418 3834 603 41 0 4377 0 vsize: 17672 [startup+240.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3859 0 0 0 23979 17 0 0 25 0 1 0 423521486 18096128 3834 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4418 3834 603 41 0 4377 0 vsize: 17672 [startup+250.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 3864 0 0 0 24978 18 0 0 25 0 1 0 423521486 18227200 3839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4450 3839 603 41 0 4409 0 vsize: 17800 [startup+260.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4000 0 0 0 25977 18 0 0 25 0 1 0 423521486 18755584 3975 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4579 3975 603 41 0 4538 0 vsize: 18316 [startup+270.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4154 0 0 0 26977 19 0 0 25 0 1 0 423521486 19288064 4129 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4709 4129 603 41 0 4668 0 vsize: 18836 [startup+280.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4305 0 0 0 27976 20 0 0 25 0 1 0 423521486 19951616 4280 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4871 4280 603 41 0 4830 0 vsize: 19484 [startup+290.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4434 0 0 0 28975 21 0 0 25 0 1 0 423521486 20484096 4409 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5001 4409 603 41 0 4960 0 vsize: 20004 [startup+300.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4557 0 0 0 29974 21 0 0 25 0 1 0 423521486 21008384 4532 4294967295 134512640 134672761 3221224560 3221223696 134560606 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5129 4532 603 41 0 5088 0 vsize: 20516 [startup+310.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4664 0 0 0 30974 22 0 0 25 0 1 0 423521486 21405696 4639 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5226 4639 603 41 0 5185 0 vsize: 20904 [startup+320.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4774 0 0 0 31973 23 0 0 25 0 1 0 423521486 21803008 4749 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5323 4749 603 41 0 5282 0 vsize: 21292 [startup+330.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4880 0 0 0 32972 24 0 0 25 0 1 0 423521486 22204416 4855 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5421 4855 603 41 0 5380 0 vsize: 21684 [startup+340.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4941 0 0 0 33971 24 0 0 25 0 1 0 423521486 22466560 4916 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5485 4916 603 41 0 5444 0 vsize: 21940 [startup+350.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4946 0 0 0 34971 25 0 0 25 0 1 0 423521486 22466560 4921 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5485 4921 603 41 0 5444 0 vsize: 21940 [startup+360.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4953 0 0 0 35970 25 0 0 25 0 1 0 423521486 22630400 4928 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5525 4928 603 41 0 5484 0 vsize: 22100 [startup+370.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4953 0 0 0 36970 26 0 0 25 0 1 0 423521486 22630400 4928 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5525 4928 603 41 0 5484 0 vsize: 22100 [startup+380.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4953 0 0 0 37970 26 0 0 25 0 1 0 423521486 22630400 4928 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5525 4928 603 41 0 5484 0 vsize: 22100 [startup+390.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4969 0 0 0 38969 26 0 0 25 0 1 0 423521486 22630400 4944 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5525 4944 603 41 0 5484 0 vsize: 22100 [startup+400.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4970 0 0 0 39969 27 0 0 25 0 1 0 423521486 22630400 4945 4294967295 134512640 134672761 3221224560 3221223560 1075349878 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5525 4945 603 41 0 5484 0 vsize: 22100 [startup+410.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4972 0 0 0 40968 27 0 0 25 0 1 0 423521486 22630400 4947 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5525 4947 603 41 0 5484 0 vsize: 22100 [startup+420.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4972 0 0 0 41968 27 0 0 25 0 1 0 423521486 22630400 4947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5525 4947 603 41 0 5484 0 vsize: 22100 [startup+430.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 4972 0 0 0 42968 28 0 0 25 0 1 0 423521486 22630400 4947 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5525 4947 603 41 0 5484 0 vsize: 22100 [startup+440.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5105 0 0 0 43967 28 0 0 25 0 1 0 423521486 23158784 5080 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5654 5080 603 41 0 5613 0 vsize: 22616 [startup+450.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5237 0 0 0 44966 29 0 0 25 0 1 0 423521486 23949312 5212 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5847 5212 603 41 0 5806 0 vsize: 23388 [startup+460.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5351 0 0 0 45965 30 0 0 25 0 1 0 423521486 24481792 5326 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5977 5326 603 41 0 5936 0 vsize: 23908 [startup+470.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5463 0 0 0 46965 30 0 0 25 0 1 0 423521486 24875008 5438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6073 5438 603 41 0 6032 0 vsize: 24292 [startup+480.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 47965 31 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223360 134565745 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5523 603 41 0 6129 0 vsize: 24680 [startup+490.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 48964 31 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5523 603 41 0 6129 0 vsize: 24680 [startup+500.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 49964 31 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5523 603 41 0 6129 0 vsize: 24680 [startup+510.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 50964 31 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5523 603 41 0 6129 0 vsize: 24680 [startup+520.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 51963 32 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5523 603 41 0 6129 0 vsize: 24680 [startup+530.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 52963 32 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5523 603 41 0 6129 0 vsize: 24680 [startup+540.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 53962 32 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5523 603 41 0 6129 0 vsize: 24680 [startup+550.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5548 0 0 0 54963 32 0 0 25 0 1 0 423521486 25272320 5523 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5523 603 41 0 6129 0 vsize: 24680 [startup+560.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5552 0 0 0 55962 33 0 0 25 0 1 0 423521486 25272320 5527 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5527 603 41 0 6129 0 vsize: 24680 [startup+570.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5552 0 0 0 56962 33 0 0 25 0 1 0 423521486 25272320 5527 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5527 603 41 0 6129 0 vsize: 24680 [startup+580.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5556 0 0 0 57961 33 0 0 25 0 1 0 423521486 25272320 5531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5531 603 41 0 6129 0 vsize: 24680 [startup+590.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5561 0 0 0 58961 33 0 0 25 0 1 0 423521486 25272320 5536 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5536 603 41 0 6129 0 vsize: 24680 [startup+600.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5561 0 0 0 59961 34 0 0 25 0 1 0 423521486 25272320 5536 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6170 5536 603 41 0 6129 0 vsize: 24680 [startup+610.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5575 0 0 0 60961 34 0 0 25 0 1 0 423521486 25427968 5550 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6208 5550 603 41 0 6167 0 vsize: 24832 [startup+620.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5657 0 0 0 61960 34 0 0 25 0 1 0 423521486 25694208 5632 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6273 5632 603 41 0 6232 0 vsize: 25092 [startup+630.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5762 0 0 0 62960 35 0 0 25 0 1 0 423521486 26087424 5737 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6369 5737 603 41 0 6328 0 vsize: 25476 [startup+640.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5869 0 0 0 63959 36 0 0 25 0 1 0 423521486 26628096 5844 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6501 5844 603 41 0 6460 0 vsize: 26004 [startup+650.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5970 0 0 0 64958 36 0 0 25 0 1 0 423521486 27021312 5945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6597 5945 603 41 0 6556 0 vsize: 26388 [startup+660.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5980 0 0 0 65957 37 0 0 25 0 1 0 423521486 27021312 5955 4294967295 134512640 134672761 3221224560 3221223744 134559514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6597 5955 603 41 0 6556 0 vsize: 26388 [startup+670.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5980 0 0 0 66957 37 0 0 25 0 1 0 423521486 27021312 5955 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6597 5955 603 41 0 6556 0 vsize: 26388 [startup+680.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5981 0 0 0 67957 38 0 0 25 0 1 0 423521486 27021312 5956 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6597 5956 603 41 0 6556 0 vsize: 26388 [startup+690.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5981 0 0 0 68956 38 0 0 25 0 1 0 423521486 27021312 5956 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6597 5956 603 41 0 6556 0 vsize: 26388 [startup+700.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5991 0 0 0 69956 38 0 0 25 0 1 0 423521486 27021312 5966 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6597 5966 603 41 0 6556 0 vsize: 26388 [startup+710.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5992 0 0 0 70956 38 0 0 25 0 1 0 423521486 27021312 5967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6597 5967 603 41 0 6556 0 vsize: 26388 [startup+720.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5992 0 0 0 71956 38 0 0 25 0 1 0 423521486 27021312 5967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6597 5967 603 41 0 6556 0 vsize: 26388 [startup+730.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 5993 0 0 0 72956 38 0 0 25 0 1 0 423521486 27021312 5968 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6597 5968 603 41 0 6556 0 vsize: 26388 [startup+740.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6004 0 0 0 73955 39 0 0 25 0 1 0 423521486 27181056 5979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6636 5979 603 41 0 6595 0 vsize: 26544 [startup+750.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6005 0 0 0 74955 39 0 0 25 0 1 0 423521486 27181056 5980 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6636 5980 603 41 0 6595 0 vsize: 26544 [startup+760.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6017 0 0 0 75954 39 0 0 25 0 1 0 423521486 27181056 5992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6636 5992 603 41 0 6595 0 vsize: 26544 [startup+770.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6017 0 0 0 76954 39 0 0 25 0 1 0 423521486 27181056 5992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6636 5992 603 41 0 6595 0 vsize: 26544 [startup+780.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6029 0 0 0 77954 40 0 0 25 0 1 0 423521486 27344896 6004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6004 603 41 0 6635 0 vsize: 26704 [startup+790.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6030 0 0 0 78954 40 0 0 25 0 1 0 423521486 27344896 6005 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6005 603 41 0 6635 0 vsize: 26704 [startup+800.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6032 0 0 0 79954 40 0 0 25 0 1 0 423521486 27344896 6007 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6007 603 41 0 6635 0 vsize: 26704 [startup+810.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6034 0 0 0 80953 40 0 0 25 0 1 0 423521486 27344896 6009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6009 603 41 0 6635 0 vsize: 26704 [startup+820.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6037 0 0 0 81953 40 0 0 25 0 1 0 423521486 27344896 6012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6012 603 41 0 6635 0 vsize: 26704 [startup+830.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6041 0 0 0 82953 41 0 0 25 0 1 0 423521486 27344896 6016 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6016 603 41 0 6635 0 vsize: 26704 [startup+840.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6043 0 0 0 83953 41 0 0 25 0 1 0 423521486 27344896 6018 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6018 603 41 0 6635 0 vsize: 26704 [startup+850.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 84952 41 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+860.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 85952 42 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+870.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 86952 42 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+880.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 87952 42 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+890.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 88951 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223696 134560611 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+900.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 89951 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+910.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 90951 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+920.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 91951 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+930.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 92950 43 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223664 134559916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+940.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 93950 44 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+950.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 94950 44 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+960.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 95949 44 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+970.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 96949 44 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+980.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 97949 45 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+990.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6044 0 0 0 98948 45 0 0 25 0 1 0 423521486 27344896 6019 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6019 603 41 0 6635 0 vsize: 26704 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6054 0 0 0 99948 45 0 0 25 0 1 0 423521486 27344896 6029 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6029 603 41 0 6635 0 vsize: 26704 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6054 0 0 0 100948 46 0 0 25 0 1 0 423521486 27344896 6029 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6029 603 41 0 6635 0 vsize: 26704 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6056 0 0 0 101948 46 0 0 25 0 1 0 423521486 27344896 6031 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6031 603 41 0 6635 0 vsize: 26704 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6057 0 0 0 102947 46 0 0 25 0 1 0 423521486 27344896 6032 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6676 6032 603 41 0 6635 0 vsize: 26704 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6155 0 0 0 103946 47 0 0 25 0 1 0 423521486 27738112 6130 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6772 6130 603 41 0 6731 0 vsize: 27088 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6276 0 0 0 104946 47 0 0 25 0 1 0 423521486 28270592 6251 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6902 6251 603 41 0 6861 0 vsize: 27608 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6282 0 0 0 105946 47 0 0 25 0 1 0 423521486 28270592 6257 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6902 6257 603 41 0 6861 0 vsize: 27608 [startup+1070.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6285 0 0 0 106946 47 0 0 25 0 1 0 423521486 28270592 6260 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6902 6260 603 41 0 6861 0 vsize: 27608 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6288 0 0 0 107945 48 0 0 25 0 1 0 423521486 28270592 6263 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6902 6263 603 41 0 6861 0 vsize: 27608 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6288 0 0 0 108944 49 0 0 25 0 1 0 423521486 28270592 6263 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6902 6263 603 41 0 6861 0 vsize: 27608 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6294 0 0 0 109944 49 0 0 25 0 1 0 423521486 28270592 6269 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6902 6269 603 41 0 6861 0 vsize: 27608 [startup+1110.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6294 0 0 0 110945 49 0 0 25 0 1 0 423521486 28270592 6269 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6902 6269 603 41 0 6861 0 vsize: 27608 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6295 0 0 0 111944 50 0 0 25 0 1 0 423521486 28270592 6270 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6902 6270 603 41 0 6861 0 vsize: 27608 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6299 0 0 0 112944 50 0 0 25 0 1 0 423521486 28270592 6274 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6902 6274 603 41 0 6861 0 vsize: 27608 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6305 0 0 0 113944 51 0 0 25 0 1 0 423521486 28430336 6280 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6941 6280 603 41 0 6900 0 vsize: 27764 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6311 0 0 0 114943 51 0 0 25 0 1 0 423521486 28430336 6286 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6941 6286 603 41 0 6900 0 vsize: 27764 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6311 0 0 0 115943 51 0 0 25 0 1 0 423521486 28430336 6286 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6941 6286 603 41 0 6900 0 vsize: 27764 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6317 0 0 0 116943 51 0 0 25 0 1 0 423521486 28430336 6292 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6941 6292 603 41 0 6900 0 vsize: 27764 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6322 0 0 0 117942 52 0 0 25 0 1 0 423521486 28430336 6297 4294967295 134512640 134672761 3221224560 3221223712 134565213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6941 6297 603 41 0 6900 0 vsize: 27764 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6327 0 0 0 118942 52 0 0 25 0 1 0 423521486 28430336 6302 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6941 6302 603 41 0 6900 0 vsize: 27764 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6332 0 0 0 119942 52 0 0 25 0 1 0 423521486 28594176 6307 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6981 6307 603 41 0 6940 0 vsize: 27924 [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4306 Raw data (stat): 4306 (minisat+) R 4305 30854 30853 0 -1 0 6346 0 0 0 120941 53 0 0 25 0 1 0 423521486 28594176 6321 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6981 6321 603 41 0 6940 0 vsize: 27924 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 4306 Raw data (stat): 4306 (minisat+) Z 4305 30854 30853 0 -1 12 6349 0 0 0 120941 54 0 0 25 0 1 0 423521486 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1210.09 CPU time (s): 1209.96 CPU user time (s): 1209.42 CPU system time (s): 0.544917 CPU usage (%): 99.9893 Max. virtual memory (Kb): 27924 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####