Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran10x10b.opb |
MD5SUM | 76a1809de3568e1012eb6c6785191a40 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 7588573 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 3100 |
Biggest coefficient in the objective function | 4831838208 |
Number of bits for the biggest coefficient in the objective function | 33 |
Sum of the numbers in the objective function | 511129031204 |
Number of bits of the sum of numbers in the objective function | 39 |
Biggest number in a constraint | 4831838208 |
Number of bits of the biggest number in a constraint | 33 |
Biggest sum of numbers in a constraint | 511129031204 |
Number of bits of the biggest sum of numbers | 39 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1217.92 |
Number of variables | 3100 |
Total number of constraints | 120 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 120 |
Minimum length of a constraint | 31 |
Maximum length of a constraint | 300 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc3 THE 2005-05-25 20:26:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22278 boxname=wulflinc3 idbench=1094 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 76a1809de3568e1012eb6c6785191a40 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-ran10x10b.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-ran10x10b.opb IDLAUNCH: 22278 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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: 906332 kB Buffers: 8856 kB Cached: 100468 kB SwapCached: 20 kB Active: 39668 kB Inactive: 72332 kB HighTotal: 131008 kB HighFree: 27300 kB LowTotal: 903652 kB LowFree: 879032 kB SwapTotal: 2097136 kB SwapFree: 2096784 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6576 kB Slab: 10824 kB Committed_AS: 71784 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 20:47:06 (client local time) WITH STATUS 152 IN 1229.88 SECONDS stats: 22278 7 1229.88 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 140 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #################### c -- Clauses(.)/Splits(s): (none) c ---[ 138]---> Sorter-cost: 2650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 136]---> Sorter-cost: 2492 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 134]---> Sorter-cost: 2492 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 132]---> Sorter-cost: 2650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 130]---> Sorter-cost: 2492 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 128]---> Sorter-cost: 2633 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> Sorter-cost: 2633 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 124]---> Adder-cost: 216 maxlim: 35830 bits: 16/16 c ---[ 122]---> Sorter-cost: 2492 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> Sorter-cost: 2650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 118]---> Sorter-cost: 2306 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 116]---> Sorter-cost: 2650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 114]---> Adder-cost: 234 maxlim: 71670 bits: 17/17 c ---[ 112]---> Sorter-cost: 2731 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 110]---> Sorter-cost: 2731 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 108]---> Sorter-cost: 2306 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 2731 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 104]---> Sorter-cost: 2650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 102]---> Sorter-cost: 2090 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 100]---> Sorter-cost: 2650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> BDD-cost: 14 c ---[ 98]---> BDD-cost: 18 c ---[ 97]---> BDD-cost: 14 c ---[ 96]---> BDD-cost: 16 c ---[ 95]---> BDD-cost: 15 c ---[ 94]---> BDD-cost: 16 c ---[ 93]---> BDD-cost: 16 c ---[ 92]---> BDD-cost: 14 c ---[ 91]---> BDD-cost: 16 c ---[ 90]---> BDD-cost: 16 c ---[ 89]---> BDD-cost: 12 c ---[ 88]---> BDD-cost: 16 c ---[ 87]---> BDD-cost: 15 c ---[ 86]---> BDD-cost: 14 c ---[ 85]---> BDD-cost: 14 c ---[ 84]---> BDD-cost: 14 c ---[ 83]---> BDD-cost: 14 c ---[ 82]---> BDD-cost: 14 c ---[ 81]---> BDD-cost: 14 c ---[ 80]---> BDD-cost: 14 c ---[ 79]---> BDD-cost: 14 c ---[ 78]---> BDD-cost: 12 c ---[ 77]---> BDD-cost: 14 c ---[ 76]---> BDD-cost: 16 c ---[ 75]---> BDD-cost: 14 c ---[ 74]---> BDD-cost: 18 c ---[ 73]---> BDD-cost: 15 c ---[ 72]---> BDD-cost: 20 c ---[ 71]---> BDD-cost: 20 c ---[ 70]---> BDD-cost: 14 c ---[ 69]---> BDD-cost: 20 c ---[ 68]---> BDD-cost: 18 c ---[ 67]---> BDD-cost: 12 c ---[ 66]---> BDD-cost: 18 c ---[ 65]---> BDD-cost: 16 c ---[ 64]---> BDD-cost: 14 c ---[ 63]---> BDD-cost: 16 c ---[ 62]---> BDD-cost: 16 c ---[ 61]---> BDD-cost: 16 c ---[ 60]---> BDD-cost: 16 c ---[ 59]---> BDD-cost: 14 c ---[ 58]---> BDD-cost: 16 c ---[ 57]---> BDD-cost: 16 c ---[ 56]---> BDD-cost: 12 c ---[ 55]---> BDD-cost: 16 c ---[ 54]---> BDD-cost: 14 c ---[ 53]---> BDD-cost: 14 c ---[ 52]---> BDD-cost: 16 c ---[ 51]---> BDD-cost: 15 c ---[ 50]---> BDD-cost: 16 c ---[ 49]---> BDD-cost: 16 c ---[ 48]---> BDD-cost: 14 c ---[ 47]---> BDD-cost: 16 c ---[ 46]---> BDD-cost: 18 c ---[ 45]---> BDD-cost: 12 c ---[ 44]---> BDD-cost: 18 c ---[ 43]---> BDD-cost: 16 c ---[ 42]---> BDD-cost: 14 c ---[ 41]---> BDD-cost: 18 c ---[ 40]---> BDD-cost: 15 c ---[ 39]---> BDD-cost: 18 c ---[ 38]---> BDD-cost: 18 c ---[ 37]---> BDD-cost: 14 c ---[ 36]---> BDD-cost: 18 c ---[ 35]---> BDD-cost: 18 c ---[ 34]---> BDD-cost: 12 c ---[ 33]---> BDD-cost: 18 c ---[ 32]---> BDD-cost: 18 c ---[ 31]---> BDD-cost: 14 c ---[ 30]---> BDD-cost: 14 c ---[ 29]---> BDD-cost: 14 c ---[ 28]---> BDD-cost: 14 c ---[ 27]---> BDD-cost: 14 c ---[ 26]---> BDD-cost: 14 c ---[ 25]---> BDD-cost: 14 c ---[ 24]---> BDD-cost: 14 c ---[ 23]---> BDD-cost: 12 c ---[ 22]---> BDD-cost: 14 c ---[ 21]---> BDD-cost: 12 c ---[ 20]---> BDD-cost: 14 c ---[ 19]---> BDD-cost: 14 c ---[ 18]---> BDD-cost: 14 c ---[ 17]---> BDD-cost: 14 c ---[ 16]---> BDD-cost: 14 c ---[ 15]---> BDD-cost: 14 c ---[ 14]---> BDD-cost: 14 c ---[ 13]---> BDD-cost: 14 c ---[ 12]---> BDD-cost: 12 c ---[ 11]---> BDD-cost: 14 c ---[ 10]---> BDD-cost: 18 c ---[ 9]---> BDD-cost: 14 c ---[ 8]---> BDD-cost: 18 c ---[ 7]---> BDD-cost: 15 c ---[ 6]---> BDD-cost: 19 c ---[ 5]---> BDD-cost: 20 c ---[ 4]---> BDD-cost: 14 c ---[ 3]---> BDD-cost: 20 c ---[ 2]---> BDD-cost: 18 c ---[ 1]---> BDD-cost: 12 c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 124542 297125 | 41514 0 0 nan | 0.000 % | c | 100 | 124542 297125 | 45665 100 426 4.3 | 7.068 % | c | 250 | 124542 297125 | 50231 250 1125 4.5 | 7.068 % | c | 476 | 124542 297125 | 55255 476 2274 4.8 | 7.068 % | c | 813 | 124542 297125 | 60780 813 3951 4.9 | 7.068 % | c | 1321 | 124542 297125 | 66858 1321 6491 4.9 | 7.068 % | c | 2080 | 124542 297125 | 73544 2080 10617 5.1 | 7.068 % | c | 3219 | 124518 297072 | 80899 3218 17426 5.4 | 7.084 % | c | 4927 | 124494 297019 | 88988 4924 27795 5.6 | 7.099 % | c | 7489 | 124332 296637 | 97887 7476 43689 5.8 | 7.198 % | c | 11333 | 123998 295811 | 107676 11295 69975 6.2 | 7.401 % | c ============================================================================== c [1mFound solution: 28111120[0m c ---[ 0]---> Adder-cost: 4880 maxlim: 4765972 bits: 24/23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15524 | 157854 416987 | 52618 15481 98297 6.3 | 7.401 % | c | 15624 | 157804 416873 | 57879 15576 98764 6.3 | 6.822 % | c | 15774 | 157685 416603 | 63667 15718 99598 6.3 | 6.889 % | c | 15999 | 157685 416603 | 70034 15943 100812 6.3 | 6.889 % | c | 16336 | 157650 416524 | 77038 16278 102874 6.3 | 6.907 % | c | 16842 | 157585 416378 | 84741 16781 105881 6.3 | 6.947 % | c | 17601 | 157576 416349 | 93215 17538 111082 6.3 | 6.951 % | c | 18741 | 157534 416255 | 102537 18675 118295 6.3 | 6.976 % | c | 20449 | 157405 415959 | 112791 20379 131439 6.4 | 7.049 % | c ============================================================================== c [1mFound solution: 27693382[0m c ---[ 0]---> Adder-cost: 0 maxlim: 5183710 bits: 24/23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21557 | 157435 416224 | 52478 21487 139947 6.5 | 7.049 % | c | 21657 | 157340 416007 | 57725 21579 140459 6.5 | 7.124 % | c | 21807 | 157340 416007 | 63498 21729 141273 6.5 | 7.124 % | c | 22032 | 157340 416007 | 69848 21954 142763 6.5 | 7.124 % | c | 22369 | 157340 416007 | 76833 22291 144704 6.5 | 7.124 % | c | 22877 | 157333 415991 | 84516 22798 148014 6.5 | 7.130 % | c | 23638 | 157333 415991 | 92967 23559 153253 6.5 | 7.130 % | c | 24777 | 157333 415991 | 102264 24698 160889 6.5 | 7.130 % | c | 26487 | 157195 415676 | 112491 26398 174909 6.6 | 7.211 % | c ============================================================================== c [1mFound solution: 27315187[0m c ---[ 0]---> Adder-cost: 0 maxlim: 5561905 bits: 24/23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27289 | 157120 415587 | 52373 27193 180346 6.6 | 7.211 % | c | 27389 | 157120 415587 | 57610 27293 180799 6.6 | 7.276 % | c | 27539 | 157120 415587 | 63371 27443 181736 6.6 | 7.276 % | c | 27764 | 157120 415587 | 69708 27668 183289 6.6 | 7.276 % | c | 28101 | 157120 415587 | 76679 28005 185398 6.6 | 7.276 % | c ============================================================================== c [1mFound solution: 25935176[0m c ---[ 0]---> Adder-cost: 0 maxlim: 6941916 bits: 24/23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28412 | 157116 415762 | 52372 28314 194022 6.9 | 7.276 % | c | 28513 | 157116 415762 | 57609 28415 194642 6.8 | 7.318 % | c | 28664 | 157116 415762 | 63370 28566 195589 6.8 | 7.318 % | c | 28889 | 157116 415762 | 69707 28791 197508 6.9 | 7.318 % | c | 29226 | 157116 415762 | 76677 29128 201465 6.9 | 7.318 % | c | 29732 | 157116 415762 | 84345 29634 205909 6.9 | 7.318 % | c ============================================================================== c [1mFound solution: 25822821[0m c ---[ 0]---> Adder-cost: 0 maxlim: 7054271 bits: 24/23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30195 | 157125 415873 | 52375 30097 210428 7.0 | 7.318 % | c | 30295 | 157125 415873 | 57612 30197 210996 7.0 | 7.332 % | c | 30445 | 157125 415873 | 63373 30347 212079 7.0 | 7.332 % | c | 30670 | 157125 415873 | 69711 30572 213397 7.0 | 7.332 % | c | 31007 | 157125 415873 | 76682 30909 215350 7.0 | 7.332 % | c | 31514 | 157125 415873 | 84350 31416 219927 7.0 | 7.332 % | c | 32276 | 157097 415811 | 92785 32173 224518 7.0 | 7.349 % | c | 33417 | 157097 415811 | 102064 33314 273487 8.2 | 7.349 % | c | 35126 | 157093 415802 | 112270 35022 364603 10.4 | 7.351 % | c ============================================================================== c [1mFound solution: 25638121[0m c ---[ 0]---> Adder-cost: 0 maxlim: 7238971 bits: 24/23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36486 | 157034 415806 | 52344 36380 389724 10.7 | 7.351 % | c | 36586 | 157034 415806 | 57578 36480 390283 10.7 | 7.423 % | c | 36736 | 157034 415806 | 63336 36630 391374 10.7 | 7.423 % | c | 36961 | 157034 415806 | 69669 36855 393462 10.7 | 7.423 % | c | 37298 | 157034 415806 | 76636 37192 395916 10.6 | 7.423 % | c | 37804 | 157024 415784 | 84300 37697 404714 10.7 | 7.429 % | c | 38563 | 156993 415715 | 92730 38449 423824 11.0 | 7.450 % | c ============================================================================== c [1mFound solution: 25246558[0m c ---[ 0]---> Adder-cost: 0 maxlim: 7630534 bits: 24/23 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39122 | 156861 415568 | 52287 39006 431162 11.1 | 7.450 % | c | 39222 | 156861 415568 | 57515 39106 431718 11.0 | 7.572 % | c | 39372 | 156861 415568 | 63267 39256 433253 11.0 | 7.572 % | c | 39597 | 156861 415568 | 69593 39481 434854 11.0 | 7.572 % | c | 39935 | 156861 415568 | 76553 39819 437389 11.0 | 7.572 % | c | 40441 | 156861 415568 | 84208 40325 442109 11.0 | 7.572 % | c | 41201 | 156861 415568 | 92629 41085 519020 12.6 | 7.572 % | c | 42342 | 156861 415568 | 101892 42226 611883 14.5 | 7.572 % | c | 44050 | 156754 415321 | 112081 43930 706973 16.1 | 7.645 % | c | 46612 | 156615 415002 | 123290 46486 769439 16.6 | 7.734 % | c ============================================================================== c [1mFound solution: 19406826[0m c ---[ 0]---> Adder-cost: 2 maxlim: 13470266 bits: 25/24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 48672 | 156654 415270 | 52218 48546 850884 17.5 | 7.734 % | c | 48772 | 156654 415270 | 57439 48646 851490 17.5 | 7.757 % | c | 48922 | 156654 415270 | 63183 48796 853652 17.5 | 7.757 % | c | 49147 | 156654 415270 | 69502 49021 862061 17.6 | 7.757 % | c | 49484 | 156654 415270 | 76452 49358 869542 17.6 | 7.757 % | c | 49990 | 156654 415270 | 84097 49864 884758 17.7 | 7.757 % | c | 50749 | 156654 415270 | 92507 50623 937500 18.5 | 7.757 % | c | 51888 | 156654 415270 | 101758 51762 1025023 19.8 | 7.757 % | c | 53597 | 156651 415264 | 111933 53470 1102804 20.6 | 7.759 % | c | 56160 | 156641 415241 | 123127 56031 1308236 23.3 | 7.765 % | c ============================================================================== c [1mFound solution: 18503008[0m c ---[ 0]---> Adder-cost: 0 maxlim: 14374084 bits: 25/24 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 59312 | 156563 415185 | 52187 59180 1552825 26.2 | 7.765 % | c | 59412 | 156563 415185 | 57405 24604 789571 32.1 | 7.844 % | c | 59563 | 156563 415185 | 63146 24755 791901 32.0 | 7.844 % | c | 59788 | 156544 415142 | 69460 24978 793455 31.8 | 7.854 % | c | 60125 | 156544 415142 | 76406 25315 796932 31.5 | 7.854 % | c | 60631 | 156544 415142 | 84047 25821 801519 31.0 | 7.854 % | c | 61391 | 156544 415142 | 92452 26581 810323 30.5 | 7.854 % | c | 62530 | 156544 415142 | 101697 27720 840942 30.3 | 7.854 % | c | 64239 | 156527 415103 | 111867 29427 903763 30.7 | 7.867 % | c | 66801 | 156527 415103 | 123054 31989 994527 31.1 | 7.867 % | c | 70647 | 156511 415057 | 135359 35831 1214024 33.9 | 7.873 % | c | 76414 | 156316 414608 | 148895 41585 1568654 37.7 | 7.984 % | c | 85065 | 156300 414556 | 163785 50232 2099767 41.8 | 7.990 % | c | 98040 | 156225 414387 | 180163 63201 3325519 52.6 | 8.036 % | c ============================================================================== c [1mFound solution: 10701810[0m c ---[ 0]---> Adder-cost: 0 maxlim: 22175282 bits: 25/25 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 106481 | 156222 414259 | 52074 68698 4407637 64.2 | 8.036 % | c | 106581 | 156222 414259 | 57281 22674 1774267 78.3 | 8.059 % | c | 106732 | 156222 414259 | 63009 22825 1775085 77.8 | 8.059 % | c | 106957 | 156222 414259 | 69310 23050 1776404 77.1 | 8.059 % | c | 107295 | 156222 414259 | 76241 23388 1779290 76.1 | 8.059 % | c | 107801 | 156222 414259 | 83865 23894 1782625 74.6 | 8.059 % | c | 108560 | 156222 414259 | 92252 24653 1787244 72.5 | 8.059 % | c | 109700 | 156222 414259 | 101477 25793 1793825 69.5 | 8.059 % | c | 111409 | 156164 414128 | 111625 27498 1830254 66.6 | 8.093 % | c | 113971 | 156164 414128 | 122787 30060 1920536 63.9 | 8.093 % | c | 117817 | 156164 414128 | 135066 33906 2051559 60.5 | 8.093 % | c | 123585 | 156164 414128 | 148573 39674 2734088 68.9 | 8.093 % | c | 132236 | 156096 413967 | 163430 48317 3739236 77.4 | 8.134 % | c | 145210 | 156076 413923 | 179773 61289 4399587 71.8 | 8.146 % | c | 164671 | 155438 412456 | 197750 80694 5761099 71.4 | 8.524 % | c | 193863 | 155289 412098 | 217526 109860 7768737 70.7 | 8.611 % | c | 237652 | 155040 411521 | 239278 153625 11725125 76.3 | 8.758 % | c | 303336 | 154916 411236 | 263206 219305 17536993 80.0 | 8.829 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 4220 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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.92 2/54 4216 Raw data (stat): 4216 (runsolver) R 4215 20224 20223 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783521059 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0001 s] Raw data (loadavg): 0.93 0.95 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0002 s] Raw data (loadavg): 0.94 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0011 s] Raw data (loadavg): 0.95 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0006 s] Raw data (loadavg): 0.95 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0017 s] Raw data (loadavg): 0.96 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0019 s] Raw data (loadavg): 0.97 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0021 s] Raw data (loadavg): 0.97 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0035 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0041 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.005 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.006 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.027 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.029 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.029 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.034 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.043 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.043 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.058 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.075 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.076 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.077 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.077 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.078 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.077 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.079 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.079 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.079 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.079 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.079 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.08 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.081 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.08 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.081 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.081 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.08 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.202 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.203 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.203 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.203 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.203 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.203 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.204 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.206 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.206 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.21 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.21 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.21 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.21 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.21 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.21 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.21 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.22 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.76 s] Raw data (loadavg): 0.99 0.97 0.92 1/53 4220 Raw data (stat): 4216 (minisat+_script) S 4215 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783521059 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.76 CPU time (s): 1229.88 CPU user time (s): 1228.92 CPU system time (s): 0.958854 CPU usage (%): 100.01 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####