Name | normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:100.opb |
MD5SUM | b2c6bc03457d15976fdaf81252d9cdae |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 435 |
Biggest coefficient in the objective function | 282 |
Number of bits for the biggest coefficient in the objective function | 9 |
Sum of the numbers in the objective function | 1168 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 282 |
Number of bits of the biggest number in a constraint | 9 |
Biggest sum of numbers in a constraint | 1168 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02284 |
Number of variables | 435 |
Total number of constraints | 935 |
Number of constraints which are clauses | 403 |
Number of constraints which are cardinality constraints (but not clauses) | 532 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 16 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc8 THE 2005-04-14 03:13:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4501 boxname=wulflinc8 idbench=365 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b2c6bc03457d15976fdaf81252d9cdae /oldhome/oroussel/tmp/wulflinc8/normalized-10:10:4.5:0.95:100.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc8/normalized-10:10:4.5:0.95:100.opb /oldhome/oroussel/tmp/wulflinc8/normalized-10:10:4.5:0.95:100.opb IDLAUNCH: 4501 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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.007 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: 876696 kB Buffers: 37556 kB Cached: 99056 kB SwapCached: 0 kB Active: 76416 kB Inactive: 64864 kB HighTotal: 131008 kB HighFree: 26292 kB LowTotal: 903652 kB LowFree: 850404 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6932 kB Slab: 11084 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 03:33:38 (client local time) WITH STATUS 10 IN 1200.21 SECONDS stats: 4501 7 1200.21 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 500 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[ 97]---> BDD-cost: 5 c ---[ 96]---> BDD-cost: 5 c ---[ 95]---> BDD-cost: 8 c ---[ 94]---> BDD-cost: 8 c ---[ 93]---> BDD-cost: 11 c ---[ 92]---> BDD-cost: 11 c ---[ 91]---> BDD-cost: 7 c ---[ 90]---> BDD-cost: 3 c ---[ 89]---> BDD-cost: 8 c ---[ 88]---> BDD-cost: 11 c ---[ 87]---> BDD-cost: 17 c ---[ 86]---> BDD-cost: 8 c ---[ 85]---> BDD-cost: 14 c ---[ 84]---> BDD-cost: 14 c ---[ 83]---> BDD-cost: 7 c ---[ 82]---> BDD-cost: 3 c ---[ 81]---> BDD-cost: 7 c ---[ 79]---> BDD-cost: 14 c ---[ 78]---> BDD-cost: 17 c ---[ 77]---> BDD-cost: 20 c ---[ 76]---> BDD-cost: 20 c ---[ 75]---> BDD-cost: 26 c ---[ 74]---> BDD-cost: 7 c ---[ 73]---> BDD-cost: 23 c ---[ 72]---> BDD-cost: 7 c ---[ 71]---> BDD-cost: 9 c ---[ 70]---> BDD-cost: 7 c ---[ 69]---> BDD-cost: 17 c ---[ 68]---> BDD-cost: 20 c ---[ 67]---> BDD-cost: 26 c ---[ 66]---> BDD-cost: 29 c ---[ 65]---> BDD-cost: 38 c ---[ 64]---> BDD-cost: 32 c ---[ 63]---> BDD-cost: 29 c ---[ 62]---> BDD-cost: 20 c ---[ 61]---> BDD-cost: 15 c ---[ 60]---> BDD-cost: 9 c ---[ 59]---> BDD-cost: 20 c ---[ 58]---> BDD-cost: 26 c ---[ 57]---> BDD-cost: 32 c ---[ 56]---> BDD-cost: 35 c ---[ 55]---> BDD-cost: 38 c ---[ 54]---> BDD-cost: 38 c ---[ 53]---> BDD-cost: 27 c ---[ 52]---> BDD-cost: 20 c ---[ 51]---> BDD-cost: 17 c ---[ 50]---> BDD-cost: 17 c ---[ 49]---> BDD-cost: 17 c ---[ 48]---> BDD-cost: 26 c ---[ 47]---> BDD-cost: 26 c ---[ 46]---> BDD-cost: 32 c ---[ 45]---> BDD-cost: 41 c ---[ 44]---> BDD-cost: 38 c ---[ 43]---> BDD-cost: 26 c ---[ 42]---> BDD-cost: 20 c ---[ 41]---> BDD-cost: 17 c ---[ 40]---> BDD-cost: 11 c ---[ 39]---> BDD-cost: 14 c ---[ 38]---> BDD-cost: 20 c ---[ 37]---> BDD-cost: 29 c ---[ 36]---> BDD-cost: 32 c ---[ 35]---> BDD-cost: 35 c ---[ 34]---> BDD-cost: 38 c ---[ 33]---> BDD-cost: 29 c ---[ 32]---> BDD-cost: 23 c ---[ 31]---> BDD-cost: 20 c ---[ 30]---> BDD-cost: 14 c ---[ 29]---> BDD-cost: 17 c ---[ 28]---> BDD-cost: 23 c ---[ 27]---> BDD-cost: 26 c ---[ 26]---> BDD-cost: 26 c ---[ 25]---> BDD-cost: 32 c ---[ 24]---> BDD-cost: 38 c ---[ 23]---> BDD-cost: 29 c ---[ 22]---> BDD-cost: 26 c ---[ 21]---> BDD-cost: 23 c ---[ 20]---> BDD-cost: 17 c ---[ 19]---> BDD-cost: 15 c ---[ 18]---> BDD-cost: 23 c ---[ 17]---> BDD-cost: 23 c ---[ 16]---> BDD-cost: 23 c ---[ 15]---> BDD-cost: 26 c ---[ 14]---> BDD-cost: 29 c ---[ 13]---> BDD-cost: 20 c ---[ 12]---> BDD-cost: 26 c ---[ 11]---> BDD-cost: 20 c ---[ 10]---> BDD-cost: 14 c ---[ 9]---> BDD-cost: 8 c ---[ 8]---> BDD-cost: 17 c ---[ 7]---> BDD-cost: 14 c ---[ 6]---> BDD-cost: 20 c ---[ 5]---> BDD-cost: 17 c ---[ 4]---> BDD-cost: 20 c ---[ 3]---> BDD-cost: 17 c ---[ 2]---> BDD-cost: 20 c ---[ 1]---> BDD-cost: 14 c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 4866 13838 | 1622 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 402[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:24587 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 46776 111909 | 15592 0 0 nan | 0.000 % | c | 100 | 46317 110889 | 17151 88 633 7.2 | 1.179 % | c ============================================================================== c [1mFound solution: 137[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 212 | 47625 114092 | 15875 200 1276 6.4 | 1.179 % | c | 312 | 47613 114068 | 17462 299 3874 13.0 | 1.213 % | c ============================================================================== c [1mFound solution: 25[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 449 | 47950 114922 | 15983 435 7059 16.2 | 1.213 % | c | 551 | 47904 114825 | 17581 535 8543 16.0 | 1.379 % | c | 702 | 47840 114679 | 19339 682 12843 18.8 | 1.468 % | c | 928 | 47588 114125 | 21273 900 16398 18.2 | 2.001 % | c | 1265 | 47588 114125 | 23400 1237 27463 22.2 | 2.001 % | c | 1771 | 47588 114125 | 25740 1743 41226 23.7 | 2.001 % | c | 2530 | 47390 113674 | 28314 2498 55997 22.4 | 2.327 % | c | 3669 | 47390 113674 | 31146 3637 114150 31.4 | 2.327 % | c ============================================================================== c [1mFound solution: 24[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4447 | 47386 113668 | 15795 4413 134651 30.5 | 2.327 % | c | 4547 | 47378 113650 | 17374 4512 137187 30.4 | 2.357 % | c | 4697 | 46743 112215 | 19111 4639 139085 30.0 | 3.410 % | c | 4922 | 46743 112215 | 21023 4864 142152 29.2 | 3.410 % | c | 5259 | 46743 112215 | 23125 5201 148530 28.6 | 3.410 % | c | 5765 | 46731 112187 | 25438 5705 191550 33.6 | 3.427 % | c | 6526 | 46731 112187 | 27981 6466 304263 47.1 | 3.427 % | c | 7665 | 46615 111930 | 30779 7597 411451 54.2 | 3.630 % | c | 9373 | 46448 111543 | 33857 9289 486526 52.4 | 3.909 % | c | 11935 | 46448 111543 | 37243 11851 1029192 86.8 | 3.909 % | c | 15781 | 46448 111543 | 40968 15697 1265497 80.6 | 3.909 % | c ============================================================================== c [1mFound solution: 21[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21427 | 46469 111611 | 15489 21338 2516856 118.0 | 3.909 % | c | 21528 | 46469 111611 | 17037 10770 1498101 139.1 | 3.919 % | c | 21680 | 46469 111611 | 18741 10922 1501083 137.4 | 3.919 % | c | 21906 | 46435 111537 | 20615 11147 1506104 135.1 | 4.003 % | c | 22243 | 46435 111537 | 22677 11484 1511405 131.6 | 4.003 % | c | 22749 | 46431 111528 | 24945 11989 1525371 127.2 | 4.007 % | c | 23511 | 46431 111528 | 27439 12751 1545253 121.2 | 4.007 % | c | 24652 | 46358 111366 | 30183 13873 1579719 113.9 | 4.193 % | c | 26362 | 46358 111366 | 33202 15583 1610608 103.4 | 4.193 % | c | 28924 | 46358 111366 | 36522 18145 1783147 98.3 | 4.193 % | c | 32768 | 46358 111366 | 40174 21989 1925348 87.6 | 4.193 % | c | 38535 | 46358 111366 | 44191 27756 2700233 97.3 | 4.193 % | c ============================================================================== c [1mFound solution: 15[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39790 | 46280 111212 | 15426 28997 2781549 95.9 | 4.193 % | c | 39890 | 46280 111212 | 16968 13562 1053546 77.7 | 4.441 % | c | 40042 | 46280 111212 | 18665 13714 1056755 77.1 | 4.441 % | c ============================================================================== c [1mFound solution: 7[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40213 | 46330 111350 | 15443 13885 1063634 76.6 | 4.441 % | c | 40314 | 46326 111342 | 16987 13983 1065435 76.2 | 4.447 % | c | 40465 | 46326 111342 | 18686 14134 1069173 75.6 | 4.447 % | c | 40690 | 46326 111342 | 20554 14359 1073625 74.8 | 4.447 % | c | 41027 | 46326 111342 | 22610 14696 1080691 73.5 | 4.447 % | c | 41533 | 46326 111342 | 24871 15202 1103496 72.6 | 4.447 % | c | 42292 | 46326 111342 | 27358 15961 1147233 71.9 | 4.447 % | c | 43431 | 46326 111342 | 30094 17100 1187597 69.5 | 4.447 % | c | 45139 | 46326 111342 | 33103 18808 1251452 66.5 | 4.447 % | c | 47705 | 46274 111223 | 36413 21358 1329833 62.3 | 4.523 % | c | 51551 | 46274 111223 | 40055 25204 1603868 63.6 | 4.523 % | c | 57319 | 46274 111223 | 44060 30972 2046499 66.1 | 4.523 % | c | 65969 | 46274 111223 | 48466 39622 3306985 83.5 | 4.523 % | c | 78943 | 46274 111223 | 53313 52596 4889094 93.0 | 4.523 % | c | 98404 | 46274 111223 | 58644 24048 4042609 168.1 | 4.523 % | c | 127597 | 46125 110880 | 64509 53233 8062774 151.5 | 4.818 % | c | 171387 | 46125 110880 | 70960 37694 8220398 218.1 | 4.818 % | c | 237072 | 46123 110876 | 78056 40578 10599055 261.2 | 4.823 % | #### 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.85 0.97 0.91 2/54 357 Raw data (stat): 357 (runsolver) R 356 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 409477504 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0004 s] Raw data (loadavg): 0.87 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 2458 0 0 0 992 6 0 0 25 0 1 0 409477504 12083200 2380 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2950 2380 603 41 0 2909 0 vsize: 11800 [startup+20.0006 s] Raw data (loadavg): 0.89 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 2939 0 0 0 1988 9 0 0 25 0 1 0 409477504 14004224 2861 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3419 2861 603 41 0 3378 0 vsize: 13676 [startup+30.0012 s] Raw data (loadavg): 0.91 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 3438 0 0 0 2986 10 0 0 25 0 1 0 409477504 16023552 3360 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3912 3360 603 41 0 3871 0 vsize: 15648 [startup+40.0005 s] Raw data (loadavg): 0.92 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 4010 0 0 0 3985 12 0 0 25 0 1 0 409477504 18440192 3932 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4502 3932 603 41 0 4461 0 vsize: 18008 [startup+50.0017 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 4621 0 0 0 4983 14 0 0 25 0 1 0 409477504 20869120 4543 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5095 4543 603 41 0 5054 0 vsize: 20380 [startup+60.0015 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 4879 0 0 0 5982 15 0 0 25 0 1 0 409477504 21950464 4801 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5359 4801 603 41 0 5318 0 vsize: 21436 [startup+70.0009 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 4879 0 0 0 6982 15 0 0 25 0 1 0 409477504 21950464 4801 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5359 4801 603 41 0 5318 0 vsize: 21436 [startup+80.002 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 4882 0 0 0 7982 15 0 0 25 0 1 0 409477504 21950464 4804 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5359 4804 603 41 0 5318 0 vsize: 21436 [startup+90.0018 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 5190 0 0 0 8981 16 0 0 25 0 1 0 409477504 23154688 5112 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5653 5112 603 41 0 5612 0 vsize: 22612 [startup+100.002 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 5256 0 0 0 9981 17 0 0 25 0 1 0 409477504 23527424 5178 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5744 5178 603 41 0 5703 0 vsize: 22976 [startup+110.004 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 5256 0 0 0 10980 17 0 0 25 0 1 0 409477504 23527424 5178 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5744 5178 603 41 0 5703 0 vsize: 22976 [startup+120.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 5256 0 0 0 11980 17 0 0 25 0 1 0 409477504 23527424 5178 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5744 5178 603 41 0 5703 0 vsize: 22976 [startup+130.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 5259 0 0 0 12980 17 0 0 25 0 1 0 409477504 23527424 5181 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5744 5181 603 41 0 5703 0 vsize: 22976 [startup+140.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 5294 0 0 0 13980 17 0 0 25 0 1 0 409477504 23789568 5216 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5808 5216 603 41 0 5767 0 vsize: 23232 [startup+150.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 5572 0 0 0 14980 18 0 0 25 0 1 0 409477504 24858624 5494 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6069 5494 603 41 0 6028 0 vsize: 24276 [startup+160.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 5991 0 0 0 15978 19 0 0 25 0 1 0 409477504 26591232 5913 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6492 5913 603 41 0 6451 0 vsize: 25968 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 6366 0 0 0 16977 21 0 0 25 0 1 0 409477504 28065792 6288 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6852 6288 603 41 0 6811 0 vsize: 27408 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 6833 0 0 0 17976 22 0 0 25 0 1 0 409477504 30072832 6755 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7342 6755 603 41 0 7301 0 vsize: 29368 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 7202 0 0 0 18975 24 0 0 25 0 1 0 409477504 31539200 7124 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7700 7124 603 41 0 7659 0 vsize: 30800 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 7516 0 0 0 19975 24 0 0 25 0 1 0 409477504 32747520 7438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7995 7438 603 41 0 7954 0 vsize: 31980 [startup+210.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 7841 0 0 0 20974 25 0 0 25 0 1 0 409477504 34091008 7763 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8323 7763 603 41 0 8282 0 vsize: 33292 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 8238 0 0 0 21973 26 0 0 25 0 1 0 409477504 35696640 8160 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8715 8160 603 41 0 8674 0 vsize: 34860 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 8652 0 0 0 22972 27 0 0 25 0 1 0 409477504 37441536 8574 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9141 8574 603 41 0 9100 0 vsize: 36564 [startup+240.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9040 0 0 0 23971 28 0 0 25 0 1 0 409477504 39034880 8962 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9530 8962 603 41 0 9489 0 vsize: 38120 [startup+250.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9438 0 0 0 24970 29 0 0 25 0 1 0 409477504 40644608 9360 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9923 9360 603 41 0 9882 0 vsize: 39692 [startup+260.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 25970 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+270.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 26970 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+280.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 27971 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223696 134565213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+290.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 28971 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+300.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 29971 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+310.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 30971 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+320.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 31971 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+330.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 32971 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+340.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 33971 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+350.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 34972 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+360.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9500 0 0 0 35972 29 0 0 25 0 1 0 409477504 40910848 9422 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9988 9422 603 41 0 9947 0 vsize: 39952 [startup+370.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 9809 0 0 0 36972 29 0 0 25 0 1 0 409477504 42110976 9731 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10281 9731 603 41 0 10240 0 vsize: 41124 [startup+380.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 10165 0 0 0 37971 30 0 0 25 0 1 0 409477504 43585536 10087 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10641 10087 603 41 0 10600 0 vsize: 42564 [startup+390.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 10391 0 0 0 38971 31 0 0 25 0 1 0 409477504 44527616 10313 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10871 10313 603 41 0 10830 0 vsize: 43484 [startup+400.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 10717 0 0 0 39970 32 0 0 25 0 1 0 409477504 45862912 10639 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11197 10639 603 41 0 11156 0 vsize: 44788 [startup+410.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 11015 0 0 0 40969 33 0 0 25 0 1 0 409477504 47071232 10937 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11492 10937 603 41 0 11451 0 vsize: 45968 [startup+420.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 11405 0 0 0 41967 35 0 0 25 0 1 0 409477504 48685056 11327 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11886 11327 603 41 0 11845 0 vsize: 47544 [startup+430.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 11862 0 0 0 42965 37 0 0 25 0 1 0 409477504 50565120 11784 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12345 11784 603 41 0 12304 0 vsize: 49380 [startup+440.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 12327 0 0 0 43965 38 0 0 25 0 1 0 409477504 52428800 12249 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12800 12249 603 41 0 12759 0 vsize: 51200 [startup+450.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 12772 0 0 0 44964 39 0 0 25 0 1 0 409477504 54300672 12694 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13257 12694 603 41 0 13216 0 vsize: 53028 [startup+460.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 13196 0 0 0 45964 39 0 0 25 0 1 0 409477504 56025088 13118 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13678 13118 603 41 0 13637 0 vsize: 54712 [startup+470.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 13641 0 0 0 46962 41 0 0 25 0 1 0 409477504 57884672 13563 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14132 13563 603 41 0 14091 0 vsize: 56528 [startup+480.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 14086 0 0 0 47961 42 0 0 25 0 1 0 409477504 59871232 14008 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14617 14008 603 41 0 14576 0 vsize: 58468 [startup+490.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 14543 0 0 0 48960 43 0 0 25 0 1 0 409477504 61734912 14465 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15072 14465 603 41 0 15031 0 vsize: 60288 [startup+500.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 14939 0 0 0 49959 44 0 0 25 0 1 0 409477504 63455232 14861 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15492 14861 603 41 0 15451 0 vsize: 61968 [startup+510.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 15377 0 0 0 50959 45 0 0 25 0 1 0 409477504 65200128 15299 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15918 15299 603 41 0 15877 0 vsize: 63672 [startup+520.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 15748 0 0 0 51958 46 0 0 25 0 1 0 409477504 66662400 15670 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16275 15670 603 41 0 16234 0 vsize: 65100 [startup+530.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16130 0 0 0 52957 47 0 0 25 0 1 0 409477504 68263936 16052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16666 16052 603 41 0 16625 0 vsize: 66664 [startup+540.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16480 0 0 0 53956 49 0 0 25 0 1 0 409477504 69742592 16402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16402 603 41 0 16986 0 vsize: 68108 [startup+550.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16480 0 0 0 54956 49 0 0 25 0 1 0 409477504 69742592 16402 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16402 603 41 0 16986 0 vsize: 68108 [startup+560.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16480 0 0 0 55956 49 0 0 25 0 1 0 409477504 69742592 16402 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16402 603 41 0 16986 0 vsize: 68108 [startup+570.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16480 0 0 0 56956 49 0 0 25 0 1 0 409477504 69742592 16402 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16402 603 41 0 16986 0 vsize: 68108 [startup+580.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16480 0 0 0 57957 49 0 0 25 0 1 0 409477504 69742592 16402 4294967295 134512640 134672761 3221224544 3221223648 134559838 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16402 603 41 0 16986 0 vsize: 68108 [startup+590.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16481 0 0 0 58957 49 0 0 25 0 1 0 409477504 69742592 16403 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16403 603 41 0 16986 0 vsize: 68108 [startup+600.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16482 0 0 0 59957 49 0 0 25 0 1 0 409477504 69742592 16404 4294967295 134512640 134672761 3221224544 3221223648 134555093 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16404 603 41 0 16986 0 vsize: 68108 [startup+610.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16482 0 0 0 60957 49 0 0 25 0 1 0 409477504 69742592 16404 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16404 603 41 0 16986 0 vsize: 68108 [startup+620.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16482 0 0 0 61957 49 0 0 25 0 1 0 409477504 69742592 16404 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16404 603 41 0 16986 0 vsize: 68108 [startup+630.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 62958 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+640.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 63958 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+650.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 64958 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+660.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 65958 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+670.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 66957 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+680.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 67956 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+690.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 68956 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+700.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 69957 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223464 1075351210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+710.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 70957 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+720.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 71957 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+730.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 72957 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+740.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 73957 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+750.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 74958 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+760.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 75958 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+770.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 76958 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+780.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16483 0 0 0 77958 49 0 0 25 0 1 0 409477504 69742592 16405 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17027 16405 603 41 0 16986 0 vsize: 68108 [startup+790.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 16822 0 0 0 78957 50 0 0 25 0 1 0 409477504 71077888 16744 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17353 16744 603 41 0 17312 0 vsize: 69412 [startup+800.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 17207 0 0 0 79957 51 0 0 25 0 1 0 409477504 72679424 17129 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17744 17129 603 41 0 17703 0 vsize: 70976 [startup+810.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 17591 0 0 0 80956 52 0 0 25 0 1 0 409477504 74272768 17513 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18133 17513 603 41 0 18092 0 vsize: 72532 [startup+820.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 17984 0 0 0 81955 53 0 0 25 0 1 0 409477504 75874304 17906 4294967295 134512640 134672761 3221224544 3221223728 134559385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18524 17906 603 41 0 18483 0 vsize: 74096 [startup+830.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 18397 0 0 0 82954 55 0 0 25 0 1 0 409477504 77479936 18319 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18916 18319 603 41 0 18875 0 vsize: 75664 [startup+840.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 18788 0 0 0 83953 56 0 0 25 0 1 0 409477504 79077376 18710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19306 18710 603 41 0 19265 0 vsize: 77224 [startup+850.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 19170 0 0 0 84952 57 0 0 25 0 1 0 409477504 80666624 19092 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19694 19092 603 41 0 19653 0 vsize: 78776 [startup+860.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 19563 0 0 0 85951 58 0 0 25 0 1 0 409477504 82292736 19485 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20091 19485 603 41 0 20050 0 vsize: 80364 [startup+870.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 19959 0 0 0 86950 59 0 0 25 0 1 0 409477504 83890176 19881 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20481 19881 603 41 0 20440 0 vsize: 81924 [startup+880.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 20347 0 0 0 87950 60 0 0 25 0 1 0 409477504 85495808 20269 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20873 20269 603 41 0 20832 0 vsize: 83492 [startup+890.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 20726 0 0 0 88949 61 0 0 25 0 1 0 409477504 87113728 20648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21268 20648 603 41 0 21227 0 vsize: 85072 [startup+900.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 21119 0 0 0 89947 63 0 0 25 0 1 0 409477504 88711168 21041 4294967295 134512640 134672761 3221224544 3221223648 134559905 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21658 21041 603 41 0 21617 0 vsize: 86632 [startup+910.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 21472 0 0 0 90946 64 0 0 25 0 1 0 409477504 90198016 21394 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22021 21394 603 41 0 21980 0 vsize: 88084 [startup+920.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 21833 0 0 0 91946 65 0 0 25 0 1 0 409477504 91656192 21755 4294967295 134512640 134672761 3221224544 3221223712 134559063 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22377 21755 603 41 0 22336 0 vsize: 89508 [startup+930.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22208 0 0 0 92945 65 0 0 25 0 1 0 409477504 93130752 22130 4294967295 134512640 134672761 3221224544 3221223680 134560714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22737 22130 603 41 0 22696 0 vsize: 90948 [startup+940.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 93945 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+950.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 94946 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+960.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 95946 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+970.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 96946 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+980.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 97946 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+990.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 98946 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 99947 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 100947 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 101947 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22342 0 0 0 102947 66 0 0 25 0 1 0 409477504 93667328 22264 4294967295 134512640 134672761 3221224544 3221223648 134560424 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22264 603 41 0 22827 0 vsize: 91472 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22343 0 0 0 103947 66 0 0 25 0 1 0 409477504 93667328 22265 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22265 603 41 0 22827 0 vsize: 91472 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 104948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 105948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 106948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1080.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 107948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223648 134560390 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 108948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1100.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 109948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1110.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 110948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1120.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 111948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1130.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 112948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1140.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 113948 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1150.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 114949 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1160.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 115949 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 116949 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 117949 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1190.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 118949 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 357 Raw data (stat): 357 (minisat+) R 356 26667 26666 0 -1 0 22345 0 0 0 119949 66 0 0 25 0 1 0 409477504 93667328 22267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22868 22267 603 41 0 22827 0 vsize: 91472 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 357 Raw data (stat): 357 (minisat+) Z 356 26667 26666 0 -1 12 22348 0 0 0 119950 70 0 0 25 0 1 0 409477504 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.08 CPU time (s): 1200.21 CPU user time (s): 1199.5 CPU system time (s): 0.704892 CPU usage (%): 100.01 Max. virtual memory (Kb): 91472 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####