Name | normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cmb.opb |
MD5SUM | a8596c98551f801a6658f1ce91b33278 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1053 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 304 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 12887 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 12887 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.97785 |
Number of variables | 304 |
Total number of constraints | 671 |
Number of constraints which are clauses | 671 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 28 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc11 THE 2005-04-13 21:12:40 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2273 boxname=wulflinc11 idbench=253 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: a8596c98551f801a6658f1ce91b33278 /oldhome/oroussel/tmp/wulflinc11/normalized-cmb.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc11/normalized-cmb.opb IDLAUNCH: 2273 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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.028 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: 918352 kB Buffers: 34528 kB Cached: 57712 kB SwapCached: 4932 kB Active: 53532 kB Inactive: 46460 kB HighTotal: 131008 kB HighFree: 69552 kB LowTotal: 903652 kB LowFree: 848800 kB SwapTotal: 2097136 kB SwapFree: 2092204 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6924 kB Slab: 10712 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 21:32:42 (client local time) WITH STATUS 10 IN 1200.12 SECONDS stats: 2273 7 1200.12 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 667 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 | 667 3359 | 222 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 1524[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:43621 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 105121 247278 | 35040 0 0 nan | 0.000 % | c | 103 | 104168 245118 | 38544 97 4313 44.5 | 0.665 % | c | 253 | 103349 243238 | 42398 229 8034 35.1 | 1.287 % | c | 479 | 103349 243238 | 46638 455 17849 39.2 | 1.287 % | c | 816 | 103349 243238 | 51302 792 23717 29.9 | 1.287 % | c | 1322 | 103349 243238 | 56432 1298 40177 31.0 | 1.287 % | c | 2083 | 103122 242717 | 62075 2058 75941 36.9 | 1.487 % | c | 3222 | 102780 241953 | 68283 3169 126886 40.0 | 1.754 % | c | 4932 | 102722 241821 | 75111 4870 197921 40.6 | 1.797 % | c | 7495 | 102722 241821 | 82622 7433 294908 39.7 | 1.797 % | c ============================================================================== c [1mFound solution: 1514[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:36082 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8239 | 189796 445156 | 63265 8177 316528 38.7 | 1.797 % | c | 8339 | 189796 445156 | 69591 8277 322185 38.9 | 1.049 % | c | 8490 | 189796 445156 | 76550 8428 326473 38.7 | 1.049 % | c | 8715 | 189774 445107 | 84205 8650 331229 38.3 | 1.059 % | c | 9052 | 189647 444838 | 92626 8982 333087 37.1 | 1.125 % | c | 9558 | 189568 444660 | 101888 9486 337879 35.6 | 1.152 % | c ============================================================================== c [1mFound solution: 1498[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9601 | 189573 444797 | 63191 9529 339448 35.6 | 1.152 % | c ============================================================================== c [1mFound solution: 1490[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9608 | 189907 445610 | 63302 9536 339814 35.6 | 1.152 % | c ============================================================================== c [1mFound solution: 1450[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9611 | 189928 445664 | 63309 9539 340630 35.7 | 1.152 % | c ============================================================================== c [1mFound solution: 1416[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9623 | 190264 446559 | 63421 9551 341049 35.7 | 1.152 % | c | 9724 | 190264 446559 | 69763 9652 348331 36.1 | 1.152 % | c | 9874 | 190264 446559 | 76739 9802 364696 37.2 | 1.152 % | c | 10099 | 190252 446532 | 84413 10026 380599 38.0 | 1.157 % | c | 10439 | 190252 446532 | 92854 10366 387470 37.4 | 1.157 % | c | 10945 | 190252 446532 | 102140 10872 406819 37.4 | 1.157 % | c ============================================================================== c [1mFound solution: 1326[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11585 | 190286 446619 | 63428 11512 555064 48.2 | 1.157 % | c | 11686 | 190286 446619 | 69770 11613 558245 48.1 | 1.158 % | c | 11839 | 190286 446619 | 76747 11766 566083 48.1 | 1.158 % | c | 12064 | 190286 446619 | 84422 11991 577304 48.1 | 1.158 % | c | 12402 | 190286 446619 | 92864 12329 581418 47.2 | 1.158 % | c | 12908 | 190258 446556 | 102151 12834 604153 47.1 | 1.167 % | c | 13667 | 190204 446436 | 112366 13589 636533 46.8 | 1.190 % | c | 14806 | 190153 446322 | 123603 14720 668941 45.4 | 1.212 % | c | 16514 | 189969 445907 | 135963 16409 754857 46.0 | 1.289 % | c | 19076 | 189969 445907 | 149559 18971 880480 46.4 | 1.289 % | c | 22921 | 189969 445907 | 164515 22816 1083581 47.5 | 1.289 % | c | 28688 | 189969 445907 | 180967 28583 1429962 50.0 | 1.289 % | c | 37340 | 189969 445907 | 199064 37235 2157656 57.9 | 1.289 % | c | 50318 | 189969 445907 | 218970 50213 4133473 82.3 | 1.289 % | c | 69780 | 189969 445907 | 240867 69675 7316398 105.0 | 1.289 % | c | 98972 | 189969 445907 | 264954 98867 9521248 96.3 | 1.289 % | #### 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.92 0.90 2/54 4241 Raw data (stat): 4241 (runsolver) R 4240 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420873984 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.0011 s] Raw data (loadavg): 0.92 0.92 0.90 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 3736 0 0 0 988 10 0 0 25 0 1 0 420873984 17948672 3534 4294967295 134512640 134672761 3221224640 3221223824 134558667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4382 3534 603 41 0 4341 0 vsize: 17528 [startup+20.0029 s] Raw data (loadavg): 0.93 0.93 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 3862 0 0 0 1988 10 0 0 25 0 1 0 420873984 18513920 3660 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4520 3660 603 41 0 4479 0 vsize: 18080 [startup+30.0032 s] Raw data (loadavg): 0.94 0.93 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 4019 0 0 0 2987 11 0 0 25 0 1 0 420873984 19050496 3817 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4651 3817 603 41 0 4610 0 vsize: 18604 [startup+40.0034 s] Raw data (loadavg): 0.95 0.93 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 6510 0 0 0 3980 18 0 0 25 0 1 0 420873984 32186368 6266 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7858 6266 603 41 0 7817 0 vsize: 31432 [startup+50.0042 s] Raw data (loadavg): 0.96 0.93 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 6804 0 0 0 4979 19 0 0 25 0 1 0 420873984 32739328 6434 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7993 6434 603 41 0 7952 0 vsize: 31972 [startup+60.0045 s] Raw data (loadavg): 0.96 0.93 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 6943 0 0 0 5978 19 0 0 25 0 1 0 420873984 33415168 6573 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8158 6573 603 41 0 8117 0 vsize: 32632 [startup+70.0058 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7064 0 0 0 6978 20 0 0 25 0 1 0 420873984 33722368 6665 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8233 6665 603 41 0 8192 0 vsize: 32932 [startup+80.0066 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7134 0 0 0 7977 21 0 0 25 0 1 0 420873984 33992704 6735 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8299 6735 603 41 0 8258 0 vsize: 33196 [startup+90.0059 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7197 0 0 0 8976 21 0 0 25 0 1 0 420873984 34258944 6798 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8364 6798 603 41 0 8323 0 vsize: 33456 [startup+100.006 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7273 0 0 0 9975 22 0 0 25 0 1 0 420873984 34664448 6874 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8463 6874 603 41 0 8422 0 vsize: 33852 [startup+110.007 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7338 0 0 0 10975 23 0 0 25 0 1 0 420873984 34930688 6939 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8528 6939 603 41 0 8487 0 vsize: 34112 [startup+120.008 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7397 0 0 0 11975 23 0 0 25 0 1 0 420873984 35201024 6998 4294967295 134512640 134672761 3221224640 3221223840 134557913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8594 6998 603 41 0 8553 0 vsize: 34376 [startup+130.009 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7451 0 0 0 12974 23 0 0 25 0 1 0 420873984 35332096 7052 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8626 7052 603 41 0 8585 0 vsize: 34504 [startup+140.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7515 0 0 0 13974 23 0 0 25 0 1 0 420873984 35602432 7116 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8692 7116 603 41 0 8651 0 vsize: 34768 [startup+150.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7587 0 0 0 14974 24 0 0 25 0 1 0 420873984 35868672 7188 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8757 7188 603 41 0 8716 0 vsize: 35028 [startup+160.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7665 0 0 0 15973 24 0 0 25 0 1 0 420873984 36265984 7266 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8854 7266 603 41 0 8813 0 vsize: 35416 [startup+170.01 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7753 0 0 0 16972 25 0 0 25 0 1 0 420873984 36536320 7354 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8920 7354 603 41 0 8879 0 vsize: 35680 [startup+180.01 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7832 0 0 0 17971 25 0 0 25 0 1 0 420873984 36941824 7433 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9019 7433 603 41 0 8978 0 vsize: 36076 [startup+190.012 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 7934 0 0 0 18971 26 0 0 25 0 1 0 420873984 37347328 7535 4294967295 134512640 134672761 3221224640 3221223776 134565143 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9118 7535 603 41 0 9077 0 vsize: 36472 [startup+200.012 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8038 0 0 0 19970 27 0 0 25 0 1 0 420873984 37744640 7639 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9215 7639 603 41 0 9174 0 vsize: 36860 [startup+210.012 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8115 0 0 0 20969 27 0 0 25 0 1 0 420873984 38010880 7716 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9280 7716 603 41 0 9239 0 vsize: 37120 [startup+220.014 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8191 0 0 0 21969 28 0 0 25 0 1 0 420873984 38408192 7792 4294967295 134512640 134672761 3221224640 3221223744 134560022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 7792 603 41 0 9336 0 vsize: 37508 [startup+230.014 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8274 0 0 0 22969 28 0 0 25 0 1 0 420873984 38678528 7875 4294967295 134512640 134672761 3221224640 3221223744 134559877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9443 7875 603 41 0 9402 0 vsize: 37772 [startup+240.014 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8352 0 0 0 23968 28 0 0 25 0 1 0 420873984 39075840 7953 4294967295 134512640 134672761 3221224640 3221223840 134557814 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9540 7953 603 41 0 9499 0 vsize: 38160 [startup+250.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8424 0 0 0 24968 29 0 0 25 0 1 0 420873984 39342080 8025 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9605 8025 603 41 0 9564 0 vsize: 38420 [startup+260.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8508 0 0 0 25967 29 0 0 25 0 1 0 420873984 39739392 8109 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9702 8109 603 41 0 9661 0 vsize: 38808 [startup+270.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8561 0 0 0 26966 30 0 0 25 0 1 0 420873984 40009728 8162 4294967295 134512640 134672761 3221224640 3221223824 134558658 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9768 8162 603 41 0 9727 0 vsize: 39072 [startup+280.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8638 0 0 0 27966 30 0 0 25 0 1 0 420873984 40271872 8239 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9832 8239 603 41 0 9791 0 vsize: 39328 [startup+290.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8707 0 0 0 28965 31 0 0 25 0 1 0 420873984 40538112 8308 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9897 8308 603 41 0 9856 0 vsize: 39588 [startup+300.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8766 0 0 0 29964 32 0 0 25 0 1 0 420873984 40808448 8367 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9963 8367 603 41 0 9922 0 vsize: 39852 [startup+310.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8837 0 0 0 30963 32 0 0 25 0 1 0 420873984 41078784 8438 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10029 8438 603 41 0 9988 0 vsize: 40116 [startup+320.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8899 0 0 0 31963 33 0 0 25 0 1 0 420873984 41349120 8500 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10095 8500 603 41 0 10054 0 vsize: 40380 [startup+330.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 8970 0 0 0 32962 34 0 0 25 0 1 0 420873984 41623552 8571 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10162 8571 603 41 0 10121 0 vsize: 40648 [startup+340.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 9037 0 0 0 33961 34 0 0 25 0 1 0 420873984 41897984 8638 4294967295 134512640 134672761 3221224640 3221223776 134560596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10229 8638 603 41 0 10188 0 vsize: 40916 [startup+350.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 9129 0 0 0 34961 35 0 0 25 0 1 0 420873984 42299392 8730 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10327 8730 603 41 0 10286 0 vsize: 41308 [startup+360.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 9233 0 0 0 35962 36 0 0 25 0 1 0 420873984 42700800 8834 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10425 8834 603 41 0 10384 0 vsize: 41700 [startup+370.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 9343 0 0 0 36962 36 0 0 25 0 1 0 420873984 43106304 8944 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10524 8944 603 41 0 10483 0 vsize: 42096 [startup+380.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 9442 0 0 0 37961 37 0 0 25 0 1 0 420873984 43511808 9043 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10623 9043 603 41 0 10582 0 vsize: 42492 [startup+390.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 9582 0 0 0 38960 38 0 0 25 0 1 0 420873984 44183552 9183 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10787 9183 603 41 0 10746 0 vsize: 43148 [startup+400.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 9733 0 0 0 39960 39 0 0 25 0 1 0 420873984 44724224 9334 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10919 9334 603 41 0 10878 0 vsize: 43676 [startup+410.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 9884 0 0 0 40959 40 0 0 25 0 1 0 420873984 45383680 9485 4294967295 134512640 134672761 3221224640 3221223840 134557822 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11080 9485 603 41 0 11039 0 vsize: 44320 [startup+420.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 10009 0 0 0 41958 40 0 0 25 0 1 0 420873984 45916160 9610 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11210 9610 603 41 0 11169 0 vsize: 44840 [startup+430.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 10143 0 0 0 42957 41 0 0 25 0 1 0 420873984 46456832 9744 4294967295 134512640 134672761 3221224640 3221223808 134561161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11342 9744 603 41 0 11301 0 vsize: 45368 [startup+440.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 10278 0 0 0 43956 43 0 0 25 0 1 0 420873984 46989312 9879 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11472 9879 603 41 0 11431 0 vsize: 45888 [startup+450.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 10439 0 0 0 44955 44 0 0 25 0 1 0 420873984 47652864 10040 4294967295 134512640 134672761 3221224640 3221223744 134560316 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11634 10040 603 41 0 11593 0 vsize: 46536 [startup+460.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 10591 0 0 0 45954 45 0 0 25 0 1 0 420873984 48189440 10192 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11765 10192 603 41 0 11724 0 vsize: 47060 [startup+470.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 10769 0 0 0 46952 46 0 0 25 0 1 0 420873984 48984064 10370 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11959 10370 603 41 0 11918 0 vsize: 47836 [startup+480.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 10915 0 0 0 47951 47 0 0 25 0 1 0 420873984 49524736 10516 4294967295 134512640 134672761 3221224640 3221223744 134560514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12091 10516 603 41 0 12050 0 vsize: 48364 [startup+490.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 11046 0 0 0 48951 48 0 0 25 0 1 0 420873984 50069504 10647 4294967295 134512640 134672761 3221224640 3221223724 134565024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12224 10647 603 41 0 12183 0 vsize: 48896 [startup+500.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 11135 0 0 0 49950 48 0 0 25 0 1 0 420873984 50470912 10736 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12322 10736 603 41 0 12281 0 vsize: 49288 [startup+510.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 11226 0 0 0 50950 48 0 0 25 0 1 0 420873984 50868224 10827 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12419 10827 603 41 0 12378 0 vsize: 49676 [startup+520.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 11341 0 0 0 51949 49 0 0 25 0 1 0 420873984 51273728 10942 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12518 10942 603 41 0 12477 0 vsize: 50072 [startup+530.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 11516 0 0 0 52948 50 0 0 25 0 1 0 420873984 52072448 11117 4294967295 134512640 134672761 3221224640 3221223744 134560514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12713 11117 603 41 0 12672 0 vsize: 50852 [startup+540.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 11636 0 0 0 53947 51 0 0 25 0 1 0 420873984 52461568 11237 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12808 11237 603 41 0 12767 0 vsize: 51232 [startup+550.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 11726 0 0 0 54947 51 0 0 25 0 1 0 420873984 52867072 11327 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12907 11327 603 41 0 12866 0 vsize: 51628 [startup+560.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 11824 0 0 0 55945 52 0 0 25 0 1 0 420873984 53272576 11425 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13006 11425 603 41 0 12965 0 vsize: 52024 [startup+570.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 11953 0 0 0 56945 53 0 0 25 0 1 0 420873984 53809152 11554 4294967295 134512640 134672761 3221224640 3221223784 134560630 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13137 11554 603 41 0 13096 0 vsize: 52548 [startup+580.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 12087 0 0 0 57944 54 0 0 25 0 1 0 420873984 54345728 11688 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13268 11688 603 41 0 13227 0 vsize: 53072 [startup+590.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 12221 0 0 0 58943 55 0 0 25 0 1 0 420873984 54874112 11822 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13397 11822 603 41 0 13356 0 vsize: 53588 [startup+600.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 12368 0 0 0 59942 55 0 0 25 0 1 0 420873984 55533568 11969 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13558 11969 603 41 0 13517 0 vsize: 54232 [startup+610.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 12520 0 0 0 60941 56 0 0 25 0 1 0 420873984 56070144 12121 4294967295 134512640 134672761 3221224640 3221223744 134560150 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13689 12121 603 41 0 13648 0 vsize: 54756 [startup+620.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 12655 0 0 0 61941 57 0 0 25 0 1 0 420873984 56610816 12256 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13821 12256 603 41 0 13780 0 vsize: 55284 [startup+630.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 12818 0 0 0 62939 58 0 0 25 0 1 0 420873984 57405440 12419 4294967295 134512640 134672761 3221224640 3221223744 134560194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14015 12419 603 41 0 13974 0 vsize: 56060 [startup+640.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 12959 0 0 0 63938 59 0 0 25 0 1 0 420873984 57942016 12560 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14146 12560 603 41 0 14105 0 vsize: 56584 [startup+650.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 13075 0 0 0 64938 59 0 0 25 0 1 0 420873984 58359808 12676 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14248 12676 603 41 0 14207 0 vsize: 56992 [startup+660.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 13219 0 0 0 65938 59 0 0 25 0 1 0 420873984 59035648 12820 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14413 12820 603 41 0 14372 0 vsize: 57652 [startup+670.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 13407 0 0 0 66938 60 0 0 25 0 1 0 420873984 59834368 13008 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14608 13008 603 41 0 14567 0 vsize: 58432 [startup+680.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 13574 0 0 0 67937 61 0 0 25 0 1 0 420873984 60772352 13175 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14837 13175 603 41 0 14796 0 vsize: 59348 [startup+690.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 13735 0 0 0 68937 61 0 0 25 0 1 0 420873984 61444096 13336 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15001 13336 603 41 0 14960 0 vsize: 60004 [startup+700.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 13893 0 0 0 69936 62 0 0 25 0 1 0 420873984 61984768 13494 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15133 13494 603 41 0 15092 0 vsize: 60532 [startup+710.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14017 0 0 0 70936 63 0 0 25 0 1 0 420873984 62513152 13618 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15262 13618 603 41 0 15221 0 vsize: 61048 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14177 0 0 0 71936 63 0 0 25 0 1 0 420873984 63172608 13778 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15423 13778 603 41 0 15382 0 vsize: 61692 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14310 0 0 0 72936 63 0 0 25 0 1 0 420873984 63705088 13911 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15553 13911 603 41 0 15512 0 vsize: 62212 [startup+740.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14406 0 0 0 73935 64 0 0 25 0 1 0 420873984 64110592 14007 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15652 14007 603 41 0 15611 0 vsize: 62608 [startup+750.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14459 0 0 0 74934 64 0 0 25 0 1 0 420873984 64372736 14060 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15716 14060 603 41 0 15675 0 vsize: 62864 [startup+760.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14510 0 0 0 75934 64 0 0 25 0 1 0 420873984 64503808 14111 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15748 14111 603 41 0 15707 0 vsize: 62992 [startup+770.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14560 0 0 0 76934 65 0 0 25 0 1 0 420873984 64774144 14161 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15814 14161 603 41 0 15773 0 vsize: 63256 [startup+780.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14622 0 0 0 77934 65 0 0 25 0 1 0 420873984 65040384 14223 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15879 14223 603 41 0 15838 0 vsize: 63516 [startup+790.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14686 0 0 0 78934 65 0 0 25 0 1 0 420873984 65298432 14287 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15942 14287 603 41 0 15901 0 vsize: 63768 [startup+800.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14731 0 0 0 79934 65 0 0 25 0 1 0 420873984 65441792 14332 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15977 14332 603 41 0 15936 0 vsize: 63908 [startup+810.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14795 0 0 0 80934 66 0 0 25 0 1 0 420873984 65708032 14396 4294967295 134512640 134672761 3221224640 3221223744 134559953 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16042 14396 603 41 0 16001 0 vsize: 64168 [startup+820.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14847 0 0 0 81934 66 0 0 25 0 1 0 420873984 65970176 14448 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16106 14448 603 41 0 16065 0 vsize: 64424 [startup+830.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14905 0 0 0 82934 66 0 0 25 0 1 0 420873984 66101248 14506 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16138 14506 603 41 0 16097 0 vsize: 64552 [startup+840.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 14956 0 0 0 83934 66 0 0 25 0 1 0 420873984 66367488 14557 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16203 14557 603 41 0 16162 0 vsize: 64812 [startup+850.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15001 0 0 0 84934 66 0 0 25 0 1 0 420873984 66498560 14602 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16235 14602 603 41 0 16194 0 vsize: 64940 [startup+860.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15076 0 0 0 85934 67 0 0 25 0 1 0 420873984 66904064 14677 4294967295 134512640 134672761 3221224640 3221223744 134560248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16334 14677 603 41 0 16293 0 vsize: 65336 [startup+870.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15138 0 0 0 86934 67 0 0 25 0 1 0 420873984 67035136 14739 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16366 14739 603 41 0 16325 0 vsize: 65464 [startup+880.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15187 0 0 0 87934 67 0 0 25 0 1 0 420873984 67301376 14788 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16431 14788 603 41 0 16390 0 vsize: 65724 [startup+890.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15243 0 0 0 88934 67 0 0 25 0 1 0 420873984 67563520 14844 4294967295 134512640 134672761 3221224640 3221223776 134560604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16495 14844 603 41 0 16454 0 vsize: 65980 [startup+900.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15294 0 0 0 89934 68 0 0 25 0 1 0 420873984 67694592 14895 4294967295 134512640 134672761 3221224640 3221223824 134558654 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16527 14895 603 41 0 16486 0 vsize: 66108 [startup+910.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15347 0 0 0 90934 68 0 0 25 0 1 0 420873984 67956736 14948 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16591 14948 603 41 0 16550 0 vsize: 66364 [startup+920.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15391 0 0 0 91934 68 0 0 25 0 1 0 420873984 68087808 14992 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16623 14992 603 41 0 16582 0 vsize: 66492 [startup+930.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15438 0 0 0 92935 68 0 0 25 0 1 0 420873984 68349952 15039 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16687 15039 603 41 0 16646 0 vsize: 66748 [startup+940.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15482 0 0 0 93935 68 0 0 25 0 1 0 420873984 68485120 15083 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16720 15083 603 41 0 16679 0 vsize: 66880 [startup+950.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15524 0 0 0 94935 68 0 0 25 0 1 0 420873984 68616192 15125 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16752 15125 603 41 0 16711 0 vsize: 67008 [startup+960.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15581 0 0 0 95935 68 0 0 25 0 1 0 420873984 68882432 15182 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16817 15182 603 41 0 16776 0 vsize: 67268 [startup+970.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15649 0 0 0 96935 68 0 0 25 0 1 0 420873984 69152768 15250 4294967295 134512640 134672761 3221224640 3221223808 134561264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16883 15250 603 41 0 16842 0 vsize: 67532 [startup+980.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15705 0 0 0 97935 69 0 0 25 0 1 0 420873984 69423104 15306 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16949 15306 603 41 0 16908 0 vsize: 67796 [startup+990.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15757 0 0 0 98935 69 0 0 25 0 1 0 420873984 69558272 15358 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16982 15358 603 41 0 16941 0 vsize: 67928 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15810 0 0 0 99935 69 0 0 25 0 1 0 420873984 69820416 15411 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17046 15411 603 41 0 17005 0 vsize: 68184 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15872 0 0 0 100935 70 0 0 25 0 1 0 420873984 70090752 15473 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17112 15473 603 41 0 17071 0 vsize: 68448 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15935 0 0 0 101934 70 0 0 25 0 1 0 420873984 70356992 15536 4294967295 134512640 134672761 3221224640 3221223796 134561032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17177 15536 603 41 0 17136 0 vsize: 68708 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 15993 0 0 0 102934 70 0 0 25 0 1 0 420873984 70488064 15594 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17209 15594 603 41 0 17168 0 vsize: 68836 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16064 0 0 0 103934 70 0 0 25 0 1 0 420873984 70893568 15665 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17308 15665 603 41 0 17267 0 vsize: 69232 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16140 0 0 0 104934 71 0 0 25 0 1 0 420873984 71155712 15741 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17372 15741 603 41 0 17331 0 vsize: 69488 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16213 0 0 0 105934 71 0 0 25 0 1 0 420873984 71421952 15814 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17437 15814 603 41 0 17396 0 vsize: 69748 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16271 0 0 0 106934 71 0 0 25 0 1 0 420873984 71684096 15872 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17501 15872 603 41 0 17460 0 vsize: 70004 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16332 0 0 0 107934 72 0 0 25 0 1 0 420873984 71950336 15933 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17566 15933 603 41 0 17525 0 vsize: 70264 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16393 0 0 0 108934 72 0 0 25 0 1 0 420873984 72212480 15994 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17630 15994 603 41 0 17589 0 vsize: 70520 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16458 0 0 0 109933 73 0 0 25 0 1 0 420873984 72478720 16059 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17695 16059 603 41 0 17654 0 vsize: 70780 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16517 0 0 0 110933 73 0 0 25 0 1 0 420873984 72749056 16118 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17761 16118 603 41 0 17720 0 vsize: 71044 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16575 0 0 0 111933 73 0 0 25 0 1 0 420873984 72880128 16176 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17793 16176 603 41 0 17752 0 vsize: 71172 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16632 0 0 0 112933 73 0 0 25 0 1 0 420873984 73150464 16233 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17859 16233 603 41 0 17818 0 vsize: 71436 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16690 0 0 0 113934 73 0 0 25 0 1 0 420873984 73416704 16291 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17924 16291 603 41 0 17883 0 vsize: 71696 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16743 0 0 0 114933 74 0 0 25 0 1 0 420873984 73547776 16344 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17956 16344 603 41 0 17915 0 vsize: 71824 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16802 0 0 0 115933 74 0 0 25 0 1 0 420873984 73814016 16403 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18021 16403 603 41 0 17980 0 vsize: 72084 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16863 0 0 0 116933 74 0 0 25 0 1 0 420873984 74084352 16464 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18087 16464 603 41 0 18046 0 vsize: 72348 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16918 0 0 0 117933 74 0 0 25 0 1 0 420873984 74379264 16519 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18159 16519 603 41 0 18118 0 vsize: 72636 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 16964 0 0 0 118933 74 0 0 25 0 1 0 420873984 74510336 16565 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18191 16565 603 41 0 18150 0 vsize: 72764 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4241 Raw data (stat): 4241 (minisat+) R 4240 32461 32460 0 -1 0 17028 0 0 0 119933 75 0 0 25 0 1 0 420873984 74768384 16629 4294967295 134512640 134672761 3221224640 3221223792 134561040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18254 16629 603 41 0 18213 0 vsize: 73016 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.13 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 4241 Raw data (stat): 4241 (minisat+) Z 4240 32461 32460 0 -1 12 17031 0 0 0 119933 78 0 0 25 0 1 0 420873984 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.12 CPU time (s): 1200.12 CPU user time (s): 1199.33 CPU system time (s): 0.78388 CPU usage (%): 99.9994 Max. virtual memory (Kb): 73016 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####