Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-markshare2.opb |
MD5SUM | b54bb080800e2327586cd478559c04ff |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 10368 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 140 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 7340025 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 7340025 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.09 |
Number of variables | 200 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 7 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc8 THE 2005-04-21 13:35:38 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18525 boxname=wulflinc8 idbench=1425 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b54bb080800e2327586cd478559c04ff /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-markshare2.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-markshare2.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-markshare2.opb IDLAUNCH: 18525 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 675328 kB Buffers: 31400 kB Cached: 305744 kB SwapCached: 0 kB Active: 80452 kB Inactive: 259556 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 675076 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 40 kB Writeback: 0 kB Mapped: 6952 kB Slab: 13512 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 13:55:40 (client local time) WITH STATUS 10 IN 1200.2 SECONDS stats: 18525 7 1200.2 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 14 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 12]---> Adder-cost: 354 maxlim: 431615 bits: 20/19 c ---[ 10]---> Adder-cost: 380 maxlim: 461183 bits: 20/19 c ---[ 8]---> Adder-cost: 350 maxlim: 445183 bits: 20/19 c ---[ 6]---> Adder-cost: 340 maxlim: 477951 bits: 20/19 c ---[ 4]---> Adder-cost: 390 maxlim: 451839 bits: 20/19 c ---[ 2]---> Adder-cost: 358 maxlim: 468735 bits: 20/19 c ---[ 0]---> Adder-cost: 374 maxlim: 444543 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 17222 61228 | 5740 0 0 nan | 0.000 % | c | 100 | 17222 61228 | 6314 100 436 4.4 | 9.969 % | c | 251 | 17222 61228 | 6945 251 1589 6.3 | 9.969 % | c | 476 | 17222 61228 | 7639 476 4122 8.7 | 9.969 % | c ============================================================================== c [1mFound solution: 651648[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1069 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 699 | 20136 68102 | 6712 699 10913 15.6 | 9.969 % | c | 799 | 20128 68076 | 7383 798 21519 27.0 | 7.575 % | c | 949 | 20128 68076 | 8121 948 30181 31.8 | 7.575 % | c ============================================================================== c [1mFound solution: 612096[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1058 | 20209 68289 | 6736 1057 40766 38.6 | 7.575 % | c | 1158 | 20209 68289 | 7409 1157 46287 40.0 | 7.570 % | c | 1309 | 20209 68289 | 8150 1308 52924 40.5 | 7.570 % | c | 1534 | 20209 68289 | 8965 1533 81998 53.5 | 7.570 % | c | 1871 | 20209 68289 | 9862 1870 121887 65.2 | 7.570 % | c | 2378 | 20185 68211 | 10848 2374 162760 68.6 | 7.648 % | c ============================================================================== c [1mFound solution: 574080[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2793 | 20200 68242 | 6733 2788 210465 75.5 | 7.648 % | c ============================================================================== c [1mFound solution: 239872[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2845 | 20232 68318 | 6744 2840 211547 74.5 | 7.648 % | c | 2946 | 20224 68292 | 7418 2940 214114 72.8 | 7.716 % | c | 3097 | 20224 68292 | 8160 3091 215459 69.7 | 7.716 % | c | 3322 | 20224 68292 | 8976 3316 226783 68.4 | 7.716 % | c | 3659 | 20200 68214 | 9873 3650 253941 69.6 | 7.794 % | c | 4166 | 20200 68214 | 10861 4157 276163 66.4 | 7.794 % | c | 4925 | 20184 68162 | 11947 4914 293765 59.8 | 7.846 % | c | 6066 | 20184 68162 | 13142 6055 389521 64.3 | 7.846 % | c | 7774 | 20184 68162 | 14456 7763 530254 68.3 | 7.846 % | c ============================================================================== c [1mFound solution: 233472[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8457 | 20206 68216 | 6735 8446 554750 65.7 | 7.846 % | c | 8557 | 20206 68216 | 7408 4323 242172 56.0 | 7.858 % | c | 8707 | 20206 68216 | 8149 4473 243252 54.4 | 7.858 % | c | 8932 | 20206 68216 | 8964 4698 245846 52.3 | 7.858 % | c | 9270 | 20206 68216 | 9860 5036 254179 50.5 | 7.858 % | c | 9779 | 20200 68198 | 10846 5544 268398 48.4 | 7.884 % | c | 10539 | 20200 68198 | 11931 6304 294399 46.7 | 7.884 % | c | 11680 | 20200 68198 | 13124 7445 351264 47.2 | 7.884 % | c | 13388 | 20200 68198 | 14437 9153 446317 48.8 | 7.884 % | c | 15950 | 20200 68198 | 15880 11715 577221 49.3 | 7.884 % | c | 19794 | 20183 68145 | 17468 15557 857831 55.1 | 7.962 % | c | 25561 | 20049 67812 | 19215 12157 724474 59.6 | 8.895 % | c | 34210 | 20017 67733 | 21137 10751 499120 46.4 | 9.077 % | c | 47184 | 20003 67697 | 23251 12920 530179 41.0 | 9.155 % | c | 66646 | 20003 67697 | 25576 20218 949013 46.9 | 9.155 % | c | 95838 | 19995 67671 | 28133 22421 1069802 47.7 | 9.181 % | c | 139628 | 19995 67671 | 30947 21035 1279848 60.8 | 9.181 % | c | 205312 | 19934 67518 | 34041 15912 771109 48.5 | 9.621 % | c | 303841 | 19934 67518 | 37446 33182 1877834 56.6 | 9.621 % | c | 451632 | 19924 67495 | 41190 22072 1191172 54.0 | 9.673 % | c ============================================================================== c [1mFound solution: 131456[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 500118 | 19908 67463 | 6636 15146 633146 41.8 | 9.673 % | c | 500219 | 19908 67463 | 7299 3888 123690 31.8 | 9.876 % | c | 500369 | 19908 67463 | 8029 4038 126129 31.2 | 9.876 % | c | 500594 | 19908 67463 | 8832 4263 130256 30.6 | 9.876 % | c | 500931 | 19908 67463 | 9715 4600 136695 29.7 | 9.876 % | c | 501437 | 19908 67463 | 10687 5106 149285 29.2 | 9.876 % | c | 502197 | 19908 67463 | 11756 5866 170398 29.0 | 9.876 % | c | 503336 | 19908 67463 | 12931 7005 219323 31.3 | 9.876 % | c | 505044 | 19908 67463 | 14224 8713 304374 34.9 | 9.876 % | c | 507606 | 19908 67463 | 15647 11275 412063 36.5 | 9.876 % | c | 511451 | 19908 67463 | 17212 15120 602595 39.9 | 9.876 % | c | 517218 | 19908 67463 | 18933 11593 389204 33.6 | 9.876 % | c | 525867 | 19908 67463 | 20826 10250 426781 41.6 | 9.876 % | c | 538842 | 19895 67433 | 22909 12420 530893 42.7 | 9.979 % | c | 558303 | 19895 67433 | 25200 19850 991637 50.0 | 9.979 % | c | 587498 | 19895 67433 | 27720 22344 834383 37.3 | 9.979 % | c ============================================================================== c [1mFound solution: 119552[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 595514 | 19843 67252 | 6614 12662 510577 40.3 | 9.979 % | c | 595614 | 19843 67252 | 7275 6431 251107 39.0 | 10.375 % | c | 595765 | 19843 67252 | 8002 6582 254009 38.6 | 10.375 % | c | 595990 | 19843 67252 | 8803 6807 259710 38.2 | 10.375 % | c | 596328 | 19843 67252 | 9683 7145 268031 37.5 | 10.375 % | c | 596835 | 19843 67252 | 10651 7652 288100 37.7 | 10.375 % | c | 597594 | 19843 67252 | 11717 8411 306034 36.4 | 10.375 % | c | 598736 | 19843 67252 | 12888 9553 344822 36.1 | 10.375 % | c | 600446 | 19682 66882 | 14177 11248 423649 37.7 | 11.617 % | c | 603008 | 19682 66882 | 15595 13810 528082 38.2 | 11.617 % | c | 606852 | 19682 66882 | 17155 9379 323702 34.5 | 11.617 % | c | 612618 | 19682 66882 | 18870 15145 566404 37.4 | 11.617 % | c | 621269 | 19672 66859 | 20757 13664 620799 45.4 | 11.669 % | c | 634243 | 19609 66707 | 22833 15806 725391 45.9 | 12.290 % | c | 653705 | 19609 66707 | 25116 23281 1040677 44.7 | 12.290 % | c | 682897 | 19609 66707 | 27628 26068 1393797 53.5 | 12.290 % | c | 726686 | 19609 66707 | 30391 23711 1513201 63.8 | 12.290 % | #### 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.53 0.83 0.86 2/54 31714 Raw data (stat): 31714 (runsolver) R 31713 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 473697999 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0007 s] Raw data (loadavg): 0.60 0.83 0.86 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 1338 0 0 0 996 3 0 0 25 0 1 0 473697999 7069696 1316 4294967295 134512640 134672761 3221224544 3221223712 134560788 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1726 1316 603 41 0 1685 0 vsize: 6904 [startup+20.0009 s] Raw data (loadavg): 0.66 0.84 0.86 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 1605 0 0 0 1994 4 0 0 25 0 1 0 473697999 8192000 1583 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2000 1583 603 41 0 1959 0 vsize: 8000 [startup+30.0023 s] Raw data (loadavg): 0.71 0.84 0.86 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2007 0 0 0 2993 5 0 0 25 0 1 0 473697999 9854976 1985 4294967295 134512640 134672761 3221224544 3221223700 134565028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2406 1985 603 41 0 2365 0 vsize: 9624 [startup+40.0031 s] Raw data (loadavg): 0.76 0.85 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2012 0 0 0 3993 6 0 0 25 0 1 0 473697999 9854976 1990 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2406 1990 603 41 0 2365 0 vsize: 9624 [startup+50.0034 s] Raw data (loadavg): 0.79 0.85 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2195 0 0 0 4992 6 0 0 25 0 1 0 473697999 10649600 2173 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2600 2173 603 41 0 2559 0 vsize: 10400 [startup+60.0036 s] Raw data (loadavg): 0.82 0.85 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2196 0 0 0 5992 6 0 0 25 0 1 0 473697999 10649600 2174 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2600 2174 603 41 0 2559 0 vsize: 10400 [startup+70.0041 s] Raw data (loadavg): 0.85 0.86 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2196 0 0 0 6992 7 0 0 25 0 1 0 473697999 10649600 2174 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2600 2174 603 41 0 2559 0 vsize: 10400 [startup+80.0045 s] Raw data (loadavg): 0.87 0.86 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2337 0 0 0 7992 7 0 0 25 0 1 0 473697999 11190272 2315 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2732 2315 603 41 0 2691 0 vsize: 10928 [startup+90.0046 s] Raw data (loadavg): 0.89 0.87 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2444 0 0 0 8992 7 0 0 25 0 1 0 473697999 11595776 2422 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2831 2422 603 41 0 2790 0 vsize: 11324 [startup+100.004 s] Raw data (loadavg): 0.91 0.87 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2444 0 0 0 9992 8 0 0 25 0 1 0 473697999 11595776 2422 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2831 2422 603 41 0 2790 0 vsize: 11324 [startup+110.005 s] Raw data (loadavg): 0.92 0.87 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2444 0 0 0 10992 8 0 0 25 0 1 0 473697999 11595776 2422 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2831 2422 603 41 0 2790 0 vsize: 11324 [startup+120.005 s] Raw data (loadavg): 0.93 0.88 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2519 0 0 0 11992 8 0 0 25 0 1 0 473697999 11866112 2497 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2897 2497 603 41 0 2856 0 vsize: 11588 [startup+130.006 s] Raw data (loadavg): 0.94 0.88 0.87 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2801 0 0 0 12991 9 0 0 25 0 1 0 473697999 13070336 2779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3191 2779 603 41 0 3150 0 vsize: 12764 [startup+140.005 s] Raw data (loadavg): 0.95 0.89 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2803 0 0 0 13991 9 0 0 25 0 1 0 473697999 13070336 2781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3191 2781 603 41 0 3150 0 vsize: 12764 [startup+150.005 s] Raw data (loadavg): 0.96 0.89 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2891 0 0 0 14991 9 0 0 25 0 1 0 473697999 13471744 2869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3289 2869 603 41 0 3248 0 vsize: 13156 [startup+160.006 s] Raw data (loadavg): 0.96 0.89 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3091 0 0 0 15991 10 0 0 25 0 1 0 473697999 14266368 3069 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3483 3069 603 41 0 3442 0 vsize: 13932 [startup+170.006 s] Raw data (loadavg): 0.97 0.89 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3108 0 0 0 16991 10 0 0 25 0 1 0 473697999 14417920 3086 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3520 3086 603 41 0 3479 0 vsize: 14080 [startup+180.007 s] Raw data (loadavg): 0.97 0.90 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3115 0 0 0 17991 10 0 0 25 0 1 0 473697999 14417920 3093 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3520 3093 603 41 0 3479 0 vsize: 14080 [startup+190.008 s] Raw data (loadavg): 0.98 0.90 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3370 0 0 0 18990 11 0 0 25 0 1 0 473697999 15519744 3348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3789 3348 603 41 0 3748 0 vsize: 15156 [startup+200.007 s] Raw data (loadavg): 0.98 0.90 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3371 0 0 0 19991 11 0 0 25 0 1 0 473697999 15519744 3349 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3789 3349 603 41 0 3748 0 vsize: 15156 [startup+210.007 s] Raw data (loadavg): 0.98 0.91 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3379 0 0 0 20990 11 0 0 25 0 1 0 473697999 15519744 3357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3789 3357 603 41 0 3748 0 vsize: 15156 [startup+220.008 s] Raw data (loadavg): 0.98 0.91 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3382 0 0 0 21990 11 0 0 25 0 1 0 473697999 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3789 3360 603 41 0 3748 0 vsize: 15156 [startup+230.008 s] Raw data (loadavg): 0.99 0.91 0.88 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3382 0 0 0 22991 11 0 0 25 0 1 0 473697999 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3789 3360 603 41 0 3748 0 vsize: 15156 [startup+240.008 s] Raw data (loadavg): 0.99 0.91 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3382 0 0 0 23991 11 0 0 25 0 1 0 473697999 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3789 3360 603 41 0 3748 0 vsize: 15156 [startup+250.008 s] Raw data (loadavg): 0.99 0.92 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3382 0 0 0 24991 11 0 0 25 0 1 0 473697999 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3789 3360 603 41 0 3748 0 vsize: 15156 [startup+260.009 s] Raw data (loadavg): 0.99 0.92 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3388 0 0 0 25991 11 0 0 25 0 1 0 473697999 15519744 3366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3789 3366 603 41 0 3748 0 vsize: 15156 [startup+270.009 s] Raw data (loadavg): 0.99 0.92 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3396 0 0 0 26991 11 0 0 25 0 1 0 473697999 15519744 3374 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3789 3374 603 41 0 3748 0 vsize: 15156 [startup+280.01 s] Raw data (loadavg): 0.99 0.92 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3406 0 0 0 27991 11 0 0 25 0 1 0 473697999 15663104 3384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3824 3384 603 41 0 3783 0 vsize: 15296 [startup+290.01 s] Raw data (loadavg): 0.99 0.92 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3406 0 0 0 28992 11 0 0 25 0 1 0 473697999 15663104 3384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3824 3384 603 41 0 3783 0 vsize: 15296 [startup+300.01 s] Raw data (loadavg): 0.99 0.93 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3413 0 0 0 29992 11 0 0 25 0 1 0 473697999 15663104 3391 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3824 3391 603 41 0 3783 0 vsize: 15296 [startup+310.011 s] Raw data (loadavg): 0.99 0.93 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3413 0 0 0 30992 11 0 0 25 0 1 0 473697999 15663104 3391 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3824 3391 603 41 0 3783 0 vsize: 15296 [startup+320.011 s] Raw data (loadavg): 0.99 0.93 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3413 0 0 0 31992 11 0 0 25 0 1 0 473697999 15663104 3391 4294967295 134512640 134672761 3221224544 3221223728 134559166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3824 3391 603 41 0 3783 0 vsize: 15296 [startup+330.012 s] Raw data (loadavg): 0.99 0.93 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3413 0 0 0 32993 11 0 0 25 0 1 0 473697999 15663104 3391 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3824 3391 603 41 0 3783 0 vsize: 15296 [startup+340.012 s] Raw data (loadavg): 0.99 0.93 0.89 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3638 0 0 0 33992 11 0 0 25 0 1 0 473697999 16728064 3616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4084 3616 603 41 0 4043 0 vsize: 16336 [startup+350.012 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3651 0 0 0 34992 12 0 0 25 0 1 0 473697999 16728064 3629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4084 3629 603 41 0 4043 0 vsize: 16336 [startup+360.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3666 0 0 0 35992 12 0 0 25 0 1 0 473697999 16875520 3644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4120 3644 603 41 0 4079 0 vsize: 16480 [startup+370.012 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3667 0 0 0 36992 12 0 0 25 0 1 0 473697999 16875520 3645 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4120 3645 603 41 0 4079 0 vsize: 16480 [startup+380.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3800 0 0 0 37993 12 0 0 25 0 1 0 473697999 17408000 3778 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4250 3778 603 41 0 4209 0 vsize: 17000 [startup+390.014 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 38993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4250 3787 603 41 0 4209 0 vsize: 17000 [startup+400.014 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 39993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4250 3787 603 41 0 4209 0 vsize: 17000 [startup+410.015 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 40993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4250 3787 603 41 0 4209 0 vsize: 17000 [startup+420.014 s] Raw data (loadavg): 0.99 0.95 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 41993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4250 3787 603 41 0 4209 0 vsize: 17000 [startup+430.015 s] Raw data (loadavg): 0.99 0.95 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 42993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4250 3787 603 41 0 4209 0 vsize: 17000 [startup+440.015 s] Raw data (loadavg): 0.99 0.95 0.90 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 43994 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4250 3787 603 41 0 4209 0 vsize: 17000 [startup+450.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3810 0 0 0 44994 12 0 0 25 0 1 0 473697999 17408000 3788 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4250 3788 603 41 0 4209 0 vsize: 17000 [startup+460.016 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3861 0 0 0 45994 12 0 0 25 0 1 0 473697999 17682432 3839 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4317 3839 603 41 0 4276 0 vsize: 17268 [startup+470.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3869 0 0 0 46994 12 0 0 25 0 1 0 473697999 17682432 3847 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4317 3847 603 41 0 4276 0 vsize: 17268 [startup+480.016 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3877 0 0 0 47994 12 0 0 25 0 1 0 473697999 17682432 3855 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4317 3855 603 41 0 4276 0 vsize: 17268 [startup+490.016 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3893 0 0 0 48994 12 0 0 25 0 1 0 473697999 17817600 3871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4350 3871 603 41 0 4309 0 vsize: 17400 [startup+500.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4049 0 0 0 49993 13 0 0 25 0 1 0 473697999 18497536 4027 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4516 4027 603 41 0 4475 0 vsize: 18064 [startup+510.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 50993 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4064 603 41 0 4508 0 vsize: 18196 [startup+520.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 51993 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4064 603 41 0 4508 0 vsize: 18196 [startup+530.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 52993 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4064 603 41 0 4508 0 vsize: 18196 [startup+540.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 53994 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223668 134566128 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4064 603 41 0 4508 0 vsize: 18196 [startup+550.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 54994 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4064 603 41 0 4508 0 vsize: 18196 [startup+560.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 55994 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4064 603 41 0 4508 0 vsize: 18196 [startup+570.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4087 0 0 0 56994 13 0 0 25 0 1 0 473697999 18632704 4065 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4065 603 41 0 4508 0 vsize: 18196 [startup+580.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4092 0 0 0 57994 13 0 0 25 0 1 0 473697999 18632704 4070 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4070 603 41 0 4508 0 vsize: 18196 [startup+590.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4092 0 0 0 58995 13 0 0 25 0 1 0 473697999 18632704 4070 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4070 603 41 0 4508 0 vsize: 18196 [startup+600.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4092 0 0 0 59995 13 0 0 25 0 1 0 473697999 18632704 4070 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4070 603 41 0 4508 0 vsize: 18196 [startup+610.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4095 0 0 0 60995 13 0 0 25 0 1 0 473697999 18632704 4073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4073 603 41 0 4508 0 vsize: 18196 [startup+620.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4098 0 0 0 61995 13 0 0 25 0 1 0 473697999 18632704 4076 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4549 4076 603 41 0 4508 0 vsize: 18196 [startup+630.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4136 0 0 0 62995 13 0 0 25 0 1 0 473697999 18767872 4114 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4582 4114 603 41 0 4541 0 vsize: 18328 [startup+640.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4162 0 0 0 63995 13 0 0 25 0 1 0 473697999 18903040 4140 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4615 4140 603 41 0 4574 0 vsize: 18460 [startup+650.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4178 0 0 0 64995 13 0 0 25 0 1 0 473697999 19054592 4156 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4652 4156 603 41 0 4611 0 vsize: 18608 [startup+660.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4179 0 0 0 65996 13 0 0 25 0 1 0 473697999 19054592 4157 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4652 4157 603 41 0 4611 0 vsize: 18608 [startup+670.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4180 0 0 0 66996 13 0 0 25 0 1 0 473697999 19054592 4158 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4652 4158 603 41 0 4611 0 vsize: 18608 [startup+680.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4272 0 0 0 67996 14 0 0 25 0 1 0 473697999 19451904 4250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4749 4250 603 41 0 4708 0 vsize: 18996 [startup+690.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4327 0 0 0 68996 14 0 0 25 0 1 0 473697999 19587072 4305 4294967295 134512640 134672761 3221224544 3221223728 134558645 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4782 4305 603 41 0 4741 0 vsize: 19128 [startup+700.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4330 0 0 0 69996 14 0 0 25 0 1 0 473697999 19587072 4308 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4782 4308 603 41 0 4741 0 vsize: 19128 [startup+710.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4335 0 0 0 70996 14 0 0 25 0 1 0 473697999 19722240 4313 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4815 4313 603 41 0 4774 0 vsize: 19260 [startup+720.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4345 0 0 0 71996 14 0 0 25 0 1 0 473697999 19722240 4323 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4815 4323 603 41 0 4774 0 vsize: 19260 [startup+730.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 72997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4815 4330 603 41 0 4774 0 vsize: 19260 [startup+740.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 73997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4815 4330 603 41 0 4774 0 vsize: 19260 [startup+750.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 74997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4815 4330 603 41 0 4774 0 vsize: 19260 [startup+760.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 75997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223600 134565096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4815 4330 603 41 0 4774 0 vsize: 19260 [startup+770.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 76997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4815 4330 603 41 0 4774 0 vsize: 19260 [startup+780.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 77997 14 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4881 4393 603 41 0 4840 0 vsize: 19524 [startup+790.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 78998 14 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4881 4393 603 41 0 4840 0 vsize: 19524 [startup+800.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 79997 15 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4881 4393 603 41 0 4840 0 vsize: 19524 [startup+810.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 80997 15 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4881 4393 603 41 0 4840 0 vsize: 19524 [startup+820.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 81997 15 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4881 4393 603 41 0 4840 0 vsize: 19524 [startup+830.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 82997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+840.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 83996 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+850.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 84997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+860.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 85997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+870.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 86997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223680 134565119 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+880.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 87997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+890.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 88997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+900.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 89998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+910.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 90998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+920.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 91998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+930.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 92998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+940.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 93998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+950.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 94999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+960.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 95999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+970.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 96999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+980.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 97999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+990.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 98999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 99999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 101000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 102000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 103000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 104000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 105000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 106001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 107001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 108001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 109001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 110001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 111002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 112002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 113002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1140.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 114002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1150.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 115002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223728 134558875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1160.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 116002 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 117002 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 118002 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1190.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 119003 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31714 Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 120003 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5011 4519 603 41 0 4970 0 vsize: 20044 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 31714 Raw data (stat): 31714 (minisat+) Z 31713 26667 26666 0 -1 12 4544 0 0 0 120003 17 0 0 25 0 1 0 473697999 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.05 CPU time (s): 1200.2 CPU user time (s): 1200.03 CPU system time (s): 0.170974 CPU usage (%): 100.013 Max. virtual memory (Kb): 20044 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####