Name | normalized-opb/submitted/manquinho/logic-synthesis/normalized-f51m.b.opb |
MD5SUM | 4fc22abde8250807abd95442a25fac44 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 18 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 407 |
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 | 407 |
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 | 407 |
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.02684 |
Number of variables | 406 |
Total number of constraints | 538 |
Number of constraints which are clauses | 520 |
Number of constraints which are cardinality constraints (but not clauses) | 18 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 123 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc13 THE 2005-04-13 20:29:55 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=617 boxname=wulflinc13 idbench=69 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 4fc22abde8250807abd95442a25fac44 /oldhome/oroussel/tmp/wulflinc13/normalized-f51m.b.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-f51m.b.opb IDLAUNCH: 617 /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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 924376 kB Buffers: 34008 kB Cached: 56720 kB SwapCached: 392 kB Active: 49616 kB Inactive: 44396 kB HighTotal: 131008 kB HighFree: 70364 kB LowTotal: 903652 kB LowFree: 854012 kB SwapTotal: 2097136 kB SwapFree: 2096744 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6928 kB Slab: 10808 kB Committed_AS: 63480 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 20:49:57 (client local time) WITH STATUS 10 IN 1200.13 SECONDS stats: 617 7 1200.13 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 498 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 | 498 13351 | 166 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 26[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:14920 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1 | 16604 50904 | 5534 1 18 18.0 | 0.000 % | c | 101 | 16604 50904 | 6087 101 2898 28.7 | 0.055 % | c ============================================================================== c [1mFound solution: 21[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 | 208 | 16615 50935 | 5538 187 12825 68.6 | 0.055 % | c | 309 | 16615 50935 | 6091 288 21975 76.3 | 0.192 % | c | 459 | 16615 50935 | 6700 438 33909 77.4 | 0.192 % | c | 686 | 16615 50935 | 7371 665 58415 87.8 | 0.192 % | c | 1029 | 16615 50935 | 8108 1008 95310 94.6 | 0.192 % | c | 1536 | 16615 50935 | 8919 1515 138105 91.2 | 0.192 % | c ============================================================================== c [1mFound solution: 19[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 | 1913 | 16410 50460 | 5470 1862 174770 93.9 | 0.192 % | c | 2013 | 16410 50460 | 6017 1962 183811 93.7 | 1.618 % | c | 2163 | 16402 50444 | 6618 2111 189584 89.8 | 1.655 % | c | 2388 | 16402 50444 | 7280 2336 201318 86.2 | 1.655 % | c | 2726 | 16402 50444 | 8008 2674 217793 81.4 | 1.655 % | c | 3232 | 16402 50444 | 8809 3180 247166 77.7 | 1.655 % | c | 3992 | 16402 50444 | 9690 3940 279064 70.8 | 1.655 % | c | 5131 | 16402 50444 | 10659 5079 327949 64.6 | 1.655 % | c | 6839 | 16402 50444 | 11725 6787 409251 60.3 | 1.655 % | c | 9401 | 16402 50444 | 12897 9349 513437 54.9 | 1.655 % | c | 13245 | 16402 50444 | 14187 13193 698978 53.0 | 1.655 % | c | 19011 | 16402 50444 | 15606 11519 497107 43.2 | 1.655 % | c | 27660 | 16402 50444 | 17167 12053 609989 50.6 | 1.655 % | c ============================================================================== c [1mFound solution: 18[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 | 33376 | 16414 50475 | 5471 17769 928999 52.3 | 1.655 % | c | 33478 | 16414 50475 | 6018 4545 221744 48.8 | 1.663 % | c | 33628 | 16414 50475 | 6619 4695 229759 48.9 | 1.663 % | c | 33855 | 16414 50475 | 7281 4922 240660 48.9 | 1.663 % | c | 34192 | 16414 50475 | 8010 5259 254469 48.4 | 1.663 % | c | 34700 | 16414 50475 | 8811 5767 274708 47.6 | 1.663 % | c | 35461 | 16414 50475 | 9692 6528 308203 47.2 | 1.663 % | c | 36601 | 16414 50475 | 10661 7668 361716 47.2 | 1.663 % | c | 38309 | 16414 50475 | 11727 9376 425326 45.4 | 1.663 % | c | 40871 | 16414 50475 | 12900 11938 539786 45.2 | 1.663 % | c | 44717 | 16414 50475 | 14190 9168 330073 36.0 | 1.663 % | c | 50487 | 16414 50475 | 15609 7682 245410 31.9 | 1.663 % | c | 59136 | 16414 50475 | 17170 8283 287557 34.7 | 1.663 % | c | 72111 | 16414 50475 | 18887 12406 433973 35.0 | 1.663 % | c | 91574 | 16414 50475 | 20776 12488 450296 36.1 | 1.663 % | c | 120768 | 16414 50475 | 22853 20303 750005 36.9 | 1.663 % | c | 164558 | 16414 50475 | 25139 17290 577512 33.4 | 1.663 % | c | 230246 | 16414 50475 | 27653 18531 543896 29.4 | 1.663 % | c | 328772 | 16414 50475 | 30418 14118 592755 42.0 | 1.663 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.95 0.90 2/54 964 Raw data (stat): 964 (runsolver) R 963 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420623233 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.001 s] Raw data (loadavg): 0.93 0.95 0.90 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 1602 0 0 0 995 3 0 0 25 0 1 0 420623233 8617984 1576 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2104 1576 603 41 0 2063 0 vsize: 8416 [startup+20.002 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 1874 0 0 0 1993 4 0 0 25 0 1 0 420623233 9711616 1848 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2371 1848 603 41 0 2330 0 vsize: 9484 [startup+30.0033 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2130 0 0 0 2991 6 0 0 25 0 1 0 420623233 10792960 2104 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2635 2104 603 41 0 2594 0 vsize: 10540 [startup+40.0027 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2139 0 0 0 3990 6 0 0 25 0 1 0 420623233 10792960 2113 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2635 2113 603 41 0 2594 0 vsize: 10540 [startup+50.0029 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2158 0 0 0 4990 6 0 0 25 0 1 0 420623233 10928128 2132 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2668 2132 603 41 0 2627 0 vsize: 10672 [startup+60.0029 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2191 0 0 0 5990 6 0 0 25 0 1 0 420623233 11063296 2165 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2701 2165 603 41 0 2660 0 vsize: 10804 [startup+70.0026 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2322 0 0 0 6990 7 0 0 25 0 1 0 420623233 11603968 2296 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2833 2296 603 41 0 2792 0 vsize: 11332 [startup+80.0029 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2438 0 0 0 7989 7 0 0 25 0 1 0 420623233 12120064 2412 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2959 2412 603 41 0 2918 0 vsize: 11836 [startup+90.0029 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2438 0 0 0 8990 7 0 0 25 0 1 0 420623233 12120064 2412 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2959 2412 603 41 0 2918 0 vsize: 11836 [startup+100.003 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2438 0 0 0 9990 7 0 0 25 0 1 0 420623233 12120064 2412 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2959 2412 603 41 0 2918 0 vsize: 11836 [startup+110.003 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2438 0 0 0 10990 7 0 0 25 0 1 0 420623233 12120064 2412 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2959 2412 603 41 0 2918 0 vsize: 11836 [startup+120.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2448 0 0 0 11989 8 0 0 25 0 1 0 420623233 12259328 2422 4294967295 134512640 134672761 3221224640 3221223828 1075347063 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2993 2422 603 41 0 2952 0 vsize: 11972 [startup+130.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2452 0 0 0 12989 8 0 0 25 0 1 0 420623233 12259328 2426 4294967295 134512640 134672761 3221224640 3221223808 134560842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2993 2426 603 41 0 2952 0 vsize: 11972 [startup+140.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2459 0 0 0 13988 9 0 0 25 0 1 0 420623233 12259328 2433 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2993 2433 603 41 0 2952 0 vsize: 11972 [startup+150.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2459 0 0 0 14988 9 0 0 25 0 1 0 420623233 12259328 2433 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2993 2433 603 41 0 2952 0 vsize: 11972 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2489 0 0 0 15988 9 0 0 25 0 1 0 420623233 12406784 2463 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3029 2463 603 41 0 2988 0 vsize: 12116 [startup+170.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2491 0 0 0 16988 9 0 0 25 0 1 0 420623233 12406784 2465 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3029 2465 603 41 0 2988 0 vsize: 12116 [startup+180.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2495 0 0 0 17987 10 0 0 25 0 1 0 420623233 12554240 2469 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3065 2469 603 41 0 3024 0 vsize: 12260 [startup+190.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2500 0 0 0 18987 10 0 0 25 0 1 0 420623233 12554240 2474 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3065 2474 603 41 0 3024 0 vsize: 12260 [startup+200.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2507 0 0 0 19986 10 0 0 25 0 1 0 420623233 12554240 2481 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3065 2481 603 41 0 3024 0 vsize: 12260 [startup+210.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2548 0 0 0 20986 11 0 0 25 0 1 0 420623233 12689408 2522 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3098 2522 603 41 0 3057 0 vsize: 12392 [startup+220.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2586 0 0 0 21985 12 0 0 25 0 1 0 420623233 12820480 2560 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3130 2560 603 41 0 3089 0 vsize: 12520 [startup+230.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2598 0 0 0 22985 12 0 0 25 0 1 0 420623233 12963840 2572 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3165 2572 603 41 0 3124 0 vsize: 12660 [startup+240.005 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2605 0 0 0 23985 12 0 0 25 0 1 0 420623233 12963840 2579 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3165 2579 603 41 0 3124 0 vsize: 12660 [startup+250.006 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2621 0 0 0 24985 12 0 0 25 0 1 0 420623233 13107200 2595 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3200 2595 603 41 0 3159 0 vsize: 12800 [startup+260.006 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2621 0 0 0 25984 12 0 0 25 0 1 0 420623233 13107200 2595 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3200 2595 603 41 0 3159 0 vsize: 12800 [startup+270.006 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2629 0 0 0 26984 13 0 0 25 0 1 0 420623233 13107200 2603 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3200 2603 603 41 0 3159 0 vsize: 12800 [startup+280.006 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2629 0 0 0 27984 13 0 0 25 0 1 0 420623233 13107200 2603 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3200 2603 603 41 0 3159 0 vsize: 12800 [startup+290.007 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2629 0 0 0 28984 13 0 0 25 0 1 0 420623233 13107200 2603 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3200 2603 603 41 0 3159 0 vsize: 12800 [startup+300.008 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2655 0 0 0 29984 13 0 0 25 0 1 0 420623233 13238272 2629 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3232 2629 603 41 0 3191 0 vsize: 12928 [startup+310.009 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2716 0 0 0 30983 13 0 0 25 0 1 0 420623233 13373440 2690 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3265 2690 603 41 0 3224 0 vsize: 13060 [startup+320.008 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2735 0 0 0 31983 13 0 0 25 0 1 0 420623233 13516800 2709 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3300 2709 603 41 0 3259 0 vsize: 13200 [startup+330.009 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2746 0 0 0 32983 14 0 0 25 0 1 0 420623233 13516800 2720 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3300 2720 603 41 0 3259 0 vsize: 13200 [startup+340.008 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2757 0 0 0 33983 14 0 0 25 0 1 0 420623233 13680640 2731 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2731 603 41 0 3299 0 vsize: 13360 [startup+350.008 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2758 0 0 0 34983 14 0 0 25 0 1 0 420623233 13680640 2732 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2732 603 41 0 3299 0 vsize: 13360 [startup+360.008 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2763 0 0 0 35983 14 0 0 25 0 1 0 420623233 13680640 2737 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2737 603 41 0 3299 0 vsize: 13360 [startup+370.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2763 0 0 0 36983 14 0 0 25 0 1 0 420623233 13680640 2737 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2737 603 41 0 3299 0 vsize: 13360 [startup+380.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2763 0 0 0 37983 14 0 0 25 0 1 0 420623233 13680640 2737 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3340 2737 603 41 0 3299 0 vsize: 13360 [startup+390.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2784 0 0 0 38983 14 0 0 25 0 1 0 420623233 13873152 2758 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3387 2758 603 41 0 3346 0 vsize: 13548 [startup+400.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2792 0 0 0 39984 14 0 0 25 0 1 0 420623233 13873152 2766 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3387 2766 603 41 0 3346 0 vsize: 13548 [startup+410.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2802 0 0 0 40984 14 0 0 25 0 1 0 420623233 13873152 2776 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3387 2776 603 41 0 3346 0 vsize: 13548 [startup+420.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2804 0 0 0 41984 14 0 0 25 0 1 0 420623233 13873152 2778 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3387 2778 603 41 0 3346 0 vsize: 13548 [startup+430.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2839 0 0 0 42984 14 0 0 25 0 1 0 420623233 14020608 2813 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3423 2813 603 41 0 3382 0 vsize: 13692 [startup+440.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2841 0 0 0 43984 14 0 0 25 0 1 0 420623233 14020608 2815 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3423 2815 603 41 0 3382 0 vsize: 13692 [startup+450.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2853 0 0 0 44984 14 0 0 25 0 1 0 420623233 14168064 2827 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3459 2827 603 41 0 3418 0 vsize: 13836 [startup+460.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2853 0 0 0 45984 14 0 0 25 0 1 0 420623233 14168064 2827 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3459 2827 603 41 0 3418 0 vsize: 13836 [startup+470.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2892 0 0 0 46984 14 0 0 25 0 1 0 420623233 14303232 2866 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3492 2866 603 41 0 3451 0 vsize: 13968 [startup+480.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2892 0 0 0 47985 14 0 0 25 0 1 0 420623233 14303232 2866 4294967295 134512640 134672761 3221224640 3221223776 134560560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3492 2866 603 41 0 3451 0 vsize: 13968 [startup+490.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2898 0 0 0 48985 14 0 0 25 0 1 0 420623233 14303232 2872 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3492 2872 603 41 0 3451 0 vsize: 13968 [startup+500.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2904 0 0 0 49985 14 0 0 25 0 1 0 420623233 14303232 2878 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3492 2878 603 41 0 3451 0 vsize: 13968 [startup+510.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2904 0 0 0 50985 14 0 0 25 0 1 0 420623233 14303232 2878 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3492 2878 603 41 0 3451 0 vsize: 13968 [startup+520.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2909 0 0 0 51985 14 0 0 25 0 1 0 420623233 14467072 2883 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3532 2883 603 41 0 3491 0 vsize: 14128 [startup+530.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2918 0 0 0 52985 14 0 0 25 0 1 0 420623233 14467072 2892 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3532 2892 603 41 0 3491 0 vsize: 14128 [startup+540.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2922 0 0 0 53985 14 0 0 25 0 1 0 420623233 14467072 2896 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3532 2896 603 41 0 3491 0 vsize: 14128 [startup+550.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2927 0 0 0 54986 14 0 0 25 0 1 0 420623233 14467072 2901 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3532 2901 603 41 0 3491 0 vsize: 14128 [startup+560.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2933 0 0 0 55986 14 0 0 25 0 1 0 420623233 14467072 2907 4294967295 134512640 134672761 3221224640 3221223744 134560364 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3532 2907 603 41 0 3491 0 vsize: 14128 [startup+570.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2934 0 0 0 56986 14 0 0 25 0 1 0 420623233 14467072 2908 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3532 2908 603 41 0 3491 0 vsize: 14128 [startup+580.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2948 0 0 0 57986 14 0 0 25 0 1 0 420623233 14610432 2922 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3567 2922 603 41 0 3526 0 vsize: 14268 [startup+590.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2949 0 0 0 58986 14 0 0 25 0 1 0 420623233 14610432 2923 4294967295 134512640 134672761 3221224640 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3567 2923 603 41 0 3526 0 vsize: 14268 [startup+600.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2959 0 0 0 59986 14 0 0 25 0 1 0 420623233 14610432 2933 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3567 2933 603 41 0 3526 0 vsize: 14268 [startup+610.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2971 0 0 0 60986 15 0 0 25 0 1 0 420623233 14610432 2945 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3567 2945 603 41 0 3526 0 vsize: 14268 [startup+620.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2992 0 0 0 61986 15 0 0 25 0 1 0 420623233 14774272 2966 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3607 2966 603 41 0 3566 0 vsize: 14428 [startup+630.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 2995 0 0 0 62986 15 0 0 25 0 1 0 420623233 14774272 2969 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3607 2969 603 41 0 3566 0 vsize: 14428 [startup+640.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3008 0 0 0 63986 15 0 0 25 0 1 0 420623233 14938112 2982 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2982 603 41 0 3606 0 vsize: 14588 [startup+650.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3008 0 0 0 64986 15 0 0 25 0 1 0 420623233 14938112 2982 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2982 603 41 0 3606 0 vsize: 14588 [startup+660.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3008 0 0 0 65987 15 0 0 25 0 1 0 420623233 14938112 2982 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2982 603 41 0 3606 0 vsize: 14588 [startup+670.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3020 0 0 0 66987 15 0 0 25 0 1 0 420623233 14938112 2994 4294967295 134512640 134672761 3221224640 3221223808 134561256 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2994 603 41 0 3606 0 vsize: 14588 [startup+680.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3021 0 0 0 67987 15 0 0 25 0 1 0 420623233 14938112 2995 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2995 603 41 0 3606 0 vsize: 14588 [startup+690.005 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3023 0 0 0 68987 15 0 0 25 0 1 0 420623233 14938112 2997 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2997 603 41 0 3606 0 vsize: 14588 [startup+700.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3024 0 0 0 69987 15 0 0 25 0 1 0 420623233 14938112 2998 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2998 603 41 0 3606 0 vsize: 14588 [startup+710.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3024 0 0 0 70987 15 0 0 25 0 1 0 420623233 14938112 2998 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2998 603 41 0 3606 0 vsize: 14588 [startup+720.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 71988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2999 603 41 0 3606 0 vsize: 14588 [startup+730.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 72988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2999 603 41 0 3606 0 vsize: 14588 [startup+740.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 73988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223824 134558651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2999 603 41 0 3606 0 vsize: 14588 [startup+750.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 74988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2999 603 41 0 3606 0 vsize: 14588 [startup+760.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 75988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2999 603 41 0 3606 0 vsize: 14588 [startup+770.006 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 76988 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2999 603 41 0 3606 0 vsize: 14588 [startup+780.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3025 0 0 0 77989 15 0 0 25 0 1 0 420623233 14938112 2999 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3647 2999 603 41 0 3606 0 vsize: 14588 [startup+790.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3085 0 0 0 78988 16 0 0 25 0 1 0 420623233 15200256 3059 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3711 3059 603 41 0 3670 0 vsize: 14844 [startup+800.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3141 0 0 0 79989 16 0 0 25 0 1 0 420623233 15495168 3115 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3783 3115 603 41 0 3742 0 vsize: 15132 [startup+810.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3143 0 0 0 80989 16 0 0 25 0 1 0 420623233 15495168 3117 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3783 3117 603 41 0 3742 0 vsize: 15132 [startup+820.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3144 0 0 0 81989 16 0 0 25 0 1 0 420623233 15495168 3118 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3783 3118 603 41 0 3742 0 vsize: 15132 [startup+830.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3207 0 0 0 82988 16 0 0 25 0 1 0 420623233 15761408 3181 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3848 3181 603 41 0 3807 0 vsize: 15392 [startup+840.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3207 0 0 0 83989 16 0 0 25 0 1 0 420623233 15761408 3181 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3848 3181 603 41 0 3807 0 vsize: 15392 [startup+850.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3216 0 0 0 84989 16 0 0 25 0 1 0 420623233 15761408 3190 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3848 3190 603 41 0 3807 0 vsize: 15392 [startup+860.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3317 0 0 0 85989 16 0 0 25 0 1 0 420623233 16162816 3291 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3946 3291 603 41 0 3905 0 vsize: 15784 [startup+870.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3452 0 0 0 86988 17 0 0 25 0 1 0 420623233 16695296 3426 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4076 3426 603 41 0 4035 0 vsize: 16304 [startup+880.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3514 0 0 0 87988 17 0 0 25 0 1 0 420623233 16965632 3488 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4142 3488 603 41 0 4101 0 vsize: 16568 [startup+890.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3527 0 0 0 88988 17 0 0 25 0 1 0 420623233 17100800 3501 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3501 603 41 0 4134 0 vsize: 16700 [startup+900.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3529 0 0 0 89989 17 0 0 25 0 1 0 420623233 17100800 3503 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3503 603 41 0 4134 0 vsize: 16700 [startup+910.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3543 0 0 0 90989 17 0 0 25 0 1 0 420623233 17100800 3517 4294967295 134512640 134672761 3221224640 3221223744 134560207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3517 603 41 0 4134 0 vsize: 16700 [startup+920.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3547 0 0 0 91989 18 0 0 25 0 1 0 420623233 17100800 3521 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3521 603 41 0 4134 0 vsize: 16700 [startup+930.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3547 0 0 0 92989 18 0 0 25 0 1 0 420623233 17100800 3521 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3521 603 41 0 4134 0 vsize: 16700 [startup+940.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3551 0 0 0 93989 18 0 0 25 0 1 0 420623233 17100800 3525 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3525 603 41 0 4134 0 vsize: 16700 [startup+950.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3553 0 0 0 94989 18 0 0 25 0 1 0 420623233 17100800 3527 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3527 603 41 0 4134 0 vsize: 16700 [startup+960.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3563 0 0 0 95989 18 0 0 25 0 1 0 420623233 17100800 3537 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3537 603 41 0 4134 0 vsize: 16700 [startup+970.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3563 0 0 0 96990 18 0 0 25 0 1 0 420623233 17100800 3537 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3537 603 41 0 4134 0 vsize: 16700 [startup+980.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3563 0 0 0 97989 18 0 0 25 0 1 0 420623233 17100800 3537 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3537 603 41 0 4134 0 vsize: 16700 [startup+990.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3563 0 0 0 98990 18 0 0 25 0 1 0 420623233 17100800 3537 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4175 3537 603 41 0 4134 0 vsize: 16700 [startup+1000.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3576 0 0 0 99990 18 0 0 25 0 1 0 420623233 17264640 3550 4294967295 134512640 134672761 3221224640 3221223744 134554687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4215 3550 603 41 0 4174 0 vsize: 16860 [startup+1010.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3585 0 0 0 100990 18 0 0 25 0 1 0 420623233 17264640 3559 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4215 3559 603 41 0 4174 0 vsize: 16860 [startup+1020.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3591 0 0 0 101990 18 0 0 25 0 1 0 420623233 17264640 3565 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4215 3565 603 41 0 4174 0 vsize: 16860 [startup+1030.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3592 0 0 0 102990 18 0 0 25 0 1 0 420623233 17264640 3566 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4215 3566 603 41 0 4174 0 vsize: 16860 [startup+1040.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3594 0 0 0 103990 18 0 0 25 0 1 0 420623233 17264640 3568 4294967295 134512640 134672761 3221224640 3221223776 134560654 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4215 3568 603 41 0 4174 0 vsize: 16860 [startup+1050.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3594 0 0 0 104991 18 0 0 25 0 1 0 420623233 17264640 3568 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4215 3568 603 41 0 4174 0 vsize: 16860 [startup+1060.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3594 0 0 0 105991 18 0 0 25 0 1 0 420623233 17264640 3568 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4215 3568 603 41 0 4174 0 vsize: 16860 [startup+1070.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3619 0 0 0 106991 18 0 0 25 0 1 0 420623233 17461248 3593 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4263 3593 603 41 0 4222 0 vsize: 17052 [startup+1080.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3635 0 0 0 107991 18 0 0 25 0 1 0 420623233 17461248 3609 4294967295 134512640 134672761 3221224640 3221223808 134561261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4263 3609 603 41 0 4222 0 vsize: 17052 [startup+1090.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3635 0 0 0 108991 18 0 0 25 0 1 0 420623233 17461248 3609 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4263 3609 603 41 0 4222 0 vsize: 17052 [startup+1100.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3635 0 0 0 109991 18 0 0 25 0 1 0 420623233 17461248 3609 4294967295 134512640 134672761 3221224640 3221223824 134559385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4263 3609 603 41 0 4222 0 vsize: 17052 [startup+1110.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3635 0 0 0 110991 18 0 0 25 0 1 0 420623233 17461248 3609 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4263 3609 603 41 0 4222 0 vsize: 17052 [startup+1120.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3641 0 0 0 111991 18 0 0 25 0 1 0 420623233 17461248 3615 4294967295 134512640 134672761 3221224640 3221223744 134554677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4263 3615 603 41 0 4222 0 vsize: 17052 [startup+1130.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3650 0 0 0 112992 18 0 0 25 0 1 0 420623233 17625088 3624 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4303 3624 603 41 0 4262 0 vsize: 17212 [startup+1140.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3652 0 0 0 113992 18 0 0 25 0 1 0 420623233 17625088 3626 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4303 3626 603 41 0 4262 0 vsize: 17212 [startup+1150.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3652 0 0 0 114992 18 0 0 25 0 1 0 420623233 17625088 3626 4294967295 134512640 134672761 3221224640 3221223808 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4303 3626 603 41 0 4262 0 vsize: 17212 [startup+1160.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3665 0 0 0 115992 18 0 0 25 0 1 0 420623233 17625088 3639 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4303 3639 603 41 0 4262 0 vsize: 17212 [startup+1170.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3666 0 0 0 116992 18 0 0 25 0 1 0 420623233 17625088 3640 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4303 3640 603 41 0 4262 0 vsize: 17212 [startup+1180.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3667 0 0 0 117992 18 0 0 25 0 1 0 420623233 17625088 3641 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4303 3641 603 41 0 4262 0 vsize: 17212 [startup+1190.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3667 0 0 0 118993 18 0 0 25 0 1 0 420623233 17625088 3641 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4303 3641 603 41 0 4262 0 vsize: 17212 [startup+1200.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 964 Raw data (stat): 964 (minisat+) R 963 30701 30700 0 -1 0 3667 0 0 0 119993 18 0 0 25 0 1 0 420623233 17625088 3641 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4303 3641 603 41 0 4262 0 vsize: 17212 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.02 s] Raw data (loadavg): 1.00 0.99 0.91 1/54 964 Raw data (stat): 964 (minisat+) Z 963 30701 30700 0 -1 12 3670 0 0 0 119993 19 0 0 25 0 1 0 420623233 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.02 CPU time (s): 1200.13 CPU user time (s): 1199.93 CPU system time (s): 0.19697 CPU usage (%): 100.009 Max. virtual memory (Kb): 17212 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####