Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-lseu.opb |
MD5SUM | 5fcfa2f72175b9723ffb2781fb76fcdc |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1120 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 85 |
Biggest coefficient in the objective function | 517 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 15494 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 1656 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 15494 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02184 |
Number of variables | 89 |
Total number of constraints | 117 |
Number of constraints which are clauses | 2 |
Number of constraints which are cardinality constraints (but not clauses) | 104 |
Number of constraints which are nor clauses,nor cardinality constraints | 11 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 47 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc7 THE 2005-04-22 02:25:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=11926 boxname=wulflinc7 idbench=918 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 5fcfa2f72175b9723ffb2781fb76fcdc /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-lseu.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-lseu.opb IDLAUNCH: 11926 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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.050 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: 296100 kB Buffers: 24488 kB Cached: 692040 kB SwapCached: 328 kB Active: 63768 kB Inactive: 655356 kB HighTotal: 131008 kB HighFree: 24024 kB LowTotal: 903652 kB LowFree: 272076 kB SwapTotal: 2097136 kB SwapFree: 2096520 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6460 kB Slab: 13812 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-22 02:36:06 (client local time) WITH STATUS 30 IN 662.695 SECONDS stats: 11926 0 662.695 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 28 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: # c -- Clauses(.)/Splits(s): ...s.. c ---[ 28]---> BDD-cost: 3 c ---[ 27]---> BDD-cost: 7 c ---[ 26]---> BDD-cost: 5 c ---[ 24]---> BDD-cost: 3 c ---[ 23]---> BDD-cost: 5 c ---[ 22]---> BDD-cost: 11 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 7 c ---[ 19]---> BDD-cost: 3 c ---[ 18]---> BDD-cost: 7 c ---[ 17]---> BDD-cost: 5 c ---[ 16]---> BDD-cost: 7 c ---[ 15]---> BDD-cost: 5 c ---[ 14]---> BDD-cost: 3 c ---[ 12]---> BDD-cost: 7 c ---[ 9]---> Sorter-cost: 3170 Base: 5 2 2 3 c ---[ 8]---> BDD-cost: 28 c ---[ 7]---> BDD-cost: 202 c ---[ 6]---> Sorter-cost: 1878 Base: 5 2 2 3 c ---[ 4]---> Sorter-cost: 1741 Base: 5 2 2 2 c ---[ 2]---> BDD-cost: 16 c ---[ 0]---> BDD-cost: 32 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 16046 38074 | 5348 0 0 nan | 0.000 % | c | 101 | 15986 37942 | 5882 99 1341 13.5 | 0.826 % | c ============================================================================== c [1mFound solution: 3697[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:12454 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 202 | 44688 105076 | 14896 173 2195 12.7 | 0.826 % | c ============================================================================== c [1mFound solution: 3371[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 256 | 44990 105888 | 14996 226 2982 13.2 | 0.826 % | c | 356 | 43633 102789 | 16495 292 3359 11.5 | 3.986 % | c | 507 | 43603 102719 | 18145 441 4465 10.1 | 4.039 % | c | 733 | 42927 101162 | 19959 655 8311 12.7 | 5.281 % | c | 1070 | 42674 100581 | 21955 987 12553 12.7 | 5.716 % | c | 1581 | 41908 98827 | 24151 1477 21494 14.6 | 7.053 % | c ============================================================================== c [1mFound solution: 3322[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1681 | 41980 99026 | 13993 1559 22101 14.2 | 7.053 % | c ============================================================================== c [1mFound solution: 3266[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1699 | 42327 99876 | 14109 1577 22632 14.4 | 7.053 % | c | 1799 | 42177 99527 | 15519 1666 25015 15.0 | 7.434 % | c ============================================================================== c [1mFound solution: 3256[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1848 | 42261 99747 | 14087 1715 26486 15.4 | 7.434 % | c | 1948 | 42261 99747 | 15495 1815 27050 14.9 | 7.424 % | c | 2099 | 42224 99662 | 17045 1963 29077 14.8 | 7.494 % | c ============================================================================== c [1mFound solution: 2378[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2173 | 42342 99948 | 14114 2037 30298 14.9 | 7.494 % | c | 2273 | 40889 96607 | 15525 2082 31508 15.1 | 10.064 % | c | 2423 | 40747 96295 | 17077 2230 38797 17.4 | 10.314 % | c ============================================================================== c [1mFound solution: 2053[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2639 | 40757 96342 | 13585 2445 47397 19.4 | 10.314 % | c | 2740 | 40697 96205 | 14943 2543 49595 19.5 | 10.462 % | c | 2891 | 40697 96205 | 16437 2694 52472 19.5 | 10.462 % | c | 3119 | 40389 95500 | 18081 2918 57025 19.5 | 11.032 % | c | 3458 | 40186 95030 | 19889 3252 68502 21.1 | 11.363 % | c ============================================================================== c [1mFound solution: 2037[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3836 | 40320 95376 | 13440 3628 85309 23.5 | 11.363 % | c | 3936 | 40286 95298 | 14784 3716 86903 23.4 | 11.496 % | c ============================================================================== c [1mFound solution: 1955[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3980 | 40237 95215 | 13412 3759 88809 23.6 | 11.496 % | c | 4080 | 40237 95215 | 14753 3859 89989 23.3 | 11.595 % | c | 4230 | 40237 95215 | 16228 4009 94858 23.7 | 11.595 % | c | 4455 | 40237 95215 | 17851 4234 106663 25.2 | 11.595 % | c | 4792 | 40237 95215 | 19636 4571 129714 28.4 | 11.595 % | c | 5299 | 40168 95064 | 21600 5070 155326 30.6 | 11.728 % | c | 6058 | 40067 94833 | 23760 5826 206079 35.4 | 11.936 % | c | 7198 | 40035 94764 | 26136 6963 270614 38.9 | 12.011 % | c | 8909 | 37164 88133 | 28749 8599 344207 40.0 | 17.102 % | c ============================================================================== c [1mFound solution: 1950[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10282 | 36034 85530 | 12011 9929 416384 41.9 | 17.102 % | c | 10387 | 36034 85530 | 13212 10034 417773 41.6 | 19.346 % | c | 10537 | 36034 85530 | 14533 10184 421049 41.3 | 19.346 % | c | 10765 | 36034 85530 | 15986 10412 430808 41.4 | 19.346 % | c | 11102 | 36034 85530 | 17585 10749 448087 41.7 | 19.346 % | c | 11608 | 36034 85530 | 19343 11255 462432 41.1 | 19.346 % | c ============================================================================== c [1mFound solution: 1850[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11882 | 36052 85587 | 12017 11529 471731 40.9 | 19.346 % | c | 11982 | 36052 85587 | 13218 11629 474845 40.8 | 19.338 % | c ============================================================================== c [1mFound solution: 1841[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12017 | 36059 85619 | 12019 11664 476260 40.8 | 19.338 % | c | 12117 | 36059 85619 | 13220 11764 482121 41.0 | 19.338 % | c | 12267 | 36059 85619 | 14542 11914 488323 41.0 | 19.338 % | c | 12493 | 36004 85490 | 15997 12135 500186 41.2 | 19.453 % | c | 12831 | 36004 85490 | 17597 12473 513216 41.1 | 19.453 % | c | 13339 | 35900 85252 | 19356 12973 535678 41.3 | 19.631 % | c | 14098 | 35900 85252 | 21292 13732 565749 41.2 | 19.631 % | c | 15238 | 35900 85252 | 23421 14872 632272 42.5 | 19.631 % | c | 16946 | 35900 85252 | 25763 16580 718187 43.3 | 19.631 % | c | 19508 | 35861 85162 | 28340 19141 820839 42.9 | 19.706 % | c ============================================================================== c [1mFound solution: 1831[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20797 | 35868 85178 | 11956 20430 868635 42.5 | 19.706 % | c ============================================================================== c [1mFound solution: 1800[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20822 | 35875 85194 | 11958 10240 370925 36.2 | 19.706 % | c | 20922 | 35875 85194 | 13153 10340 376338 36.4 | 19.709 % | c | 21073 | 35820 85065 | 14469 10484 379199 36.2 | 19.812 % | c | 21298 | 35820 85065 | 15916 10709 384451 35.9 | 19.812 % | c | 21635 | 35820 85065 | 17507 11046 403641 36.5 | 19.812 % | c | 22141 | 35797 85013 | 19258 11551 425009 36.8 | 19.852 % | c ============================================================================== c [1mFound solution: 1729[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22401 | 35807 85052 | 11935 11811 435927 36.9 | 19.852 % | c | 22503 | 35807 85052 | 13128 11913 437731 36.7 | 19.850 % | c | 22654 | 35807 85052 | 14441 12064 440540 36.5 | 19.850 % | c | 22882 | 35807 85052 | 15885 12292 449714 36.6 | 19.850 % | c | 23220 | 35605 84581 | 17474 12628 457488 36.2 | 20.188 % | c ============================================================================== c [1mFound solution: 1727[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23653 | 35611 84596 | 11870 13061 479394 36.7 | 20.188 % | c ============================================================================== c [1mFound solution: 1683[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23732 | 35616 84608 | 11872 13140 483575 36.8 | 20.188 % | c | 23832 | 35616 84608 | 13059 13240 487557 36.8 | 20.192 % | c | 23983 | 35616 84608 | 14365 13391 493894 36.9 | 20.192 % | c ============================================================================== c [1mFound solution: 1675[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24036 | 35621 84619 | 11873 13444 495347 36.8 | 20.192 % | c | 24136 | 35621 84619 | 13060 13544 503809 37.2 | 20.194 % | c | 24286 | 35621 84619 | 14366 13694 506670 37.0 | 20.194 % | c | 24512 | 35621 84619 | 15802 13920 519039 37.3 | 20.194 % | c | 24849 | 35621 84619 | 17383 14257 537179 37.7 | 20.194 % | c | 25355 | 35621 84619 | 19121 14763 550379 37.3 | 20.194 % | c | 26114 | 35023 83235 | 21033 15466 571637 37.0 | 21.324 % | c | 27253 | 35023 83235 | 23137 16605 619296 37.3 | 21.324 % | c | 28963 | 35023 83235 | 25450 18315 687059 37.5 | 21.324 % | c ============================================================================== c [1mFound solution: 1614[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29392 | 35028 83246 | 11676 18744 708385 37.8 | 21.324 % | c | 29492 | 35028 83246 | 12843 9472 290847 30.7 | 21.327 % | c | 29642 | 34964 83098 | 14127 9621 294252 30.6 | 21.447 % | c | 29869 | 34964 83098 | 15540 9848 299169 30.4 | 21.447 % | c | 30208 | 34964 83098 | 17094 10187 308569 30.3 | 21.447 % | c | 30714 | 34964 83098 | 18804 10693 320449 30.0 | 21.447 % | c ============================================================================== c [1mFound solution: 1587[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31206 | 34978 83134 | 11659 11185 339724 30.4 | 21.447 % | c | 31306 | 34978 83134 | 12824 11285 341955 30.3 | 21.442 % | c | 31457 | 34978 83134 | 14107 11436 349352 30.5 | 21.442 % | c ============================================================================== c [1mFound solution: 1570[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31521 | 34985 83154 | 11661 11500 352534 30.7 | 21.442 % | c | 31623 | 34985 83154 | 12827 11602 354369 30.5 | 21.442 % | c | 31774 | 34985 83154 | 14109 11753 356599 30.3 | 21.442 % | c | 32001 | 34985 83154 | 15520 11980 363253 30.3 | 21.442 % | c | 32340 | 34985 83154 | 17072 12319 378819 30.8 | 21.442 % | c | 32847 | 34985 83154 | 18780 12826 388215 30.3 | 21.442 % | c | 33608 | 34985 83154 | 20658 13587 426121 31.4 | 21.442 % | c | 34748 | 34985 83154 | 22723 14727 487779 33.1 | 21.442 % | c | 36457 | 34985 83154 | 24996 16436 583123 35.5 | 21.442 % | c | 39020 | 34801 82731 | 27496 18992 681940 35.9 | 21.745 % | c ============================================================================== c [1mFound solution: 1517[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 41774 | 34808 82747 | 11602 21746 853274 39.2 | 21.745 % | c | 41875 | 34808 82747 | 12762 10974 412117 37.6 | 21.746 % | c | 42025 | 34808 82747 | 14038 11124 417783 37.6 | 21.746 % | c | 42251 | 34808 82747 | 15442 11350 422061 37.2 | 21.746 % | c | 42591 | 34808 82747 | 16986 11690 428663 36.7 | 21.746 % | c | 43099 | 34808 82747 | 18685 12198 438542 36.0 | 21.746 % | c | 43858 | 34808 82747 | 20553 12957 454152 35.1 | 21.746 % | c | 44997 | 34808 82747 | 22609 14096 515846 36.6 | 21.746 % | c ============================================================================== c [1mFound solution: 1516[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45960 | 34815 82763 | 11605 15059 573361 38.1 | 21.746 % | c | 46063 | 34815 82763 | 12765 15162 578306 38.1 | 21.747 % | c | 46214 | 34815 82763 | 14042 15313 582046 38.0 | 21.747 % | c | 46439 | 34815 82763 | 15446 15538 589238 37.9 | 21.747 % | c ============================================================================== c [1mFound solution: 1503[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 46460 | 34820 82775 | 11606 15559 589681 37.9 | 21.747 % | c | 46561 | 34820 82775 | 12766 7881 213609 27.1 | 21.749 % | c | 46712 | 34820 82775 | 14043 8032 219155 27.3 | 21.749 % | c | 46941 | 34820 82775 | 15447 8261 225582 27.3 | 21.749 % | c | 47278 | 34820 82775 | 16992 8598 236302 27.5 | 21.749 % | c | 47785 | 34820 82775 | 18691 9105 253128 27.8 | 21.749 % | c | 48545 | 34652 82385 | 20560 9857 279243 28.3 | 22.070 % | c ============================================================================== c [1mFound solution: 1455[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 48864 | 34640 82360 | 11546 10174 303361 29.8 | 22.070 % | c | 48966 | 34640 82360 | 12700 10276 305980 29.8 | 22.094 % | c | 49117 | 34640 82360 | 13970 10427 313871 30.1 | 22.094 % | c | 49342 | 34640 82360 | 15367 10652 325753 30.6 | 22.094 % | c | 49679 | 34640 82360 | 16904 10989 339980 30.9 | 22.094 % | c | 50187 | 34640 82360 | 18594 11497 359131 31.2 | 22.094 % | c | 50948 | 34640 82360 | 20454 12258 394268 32.2 | 22.094 % | c ============================================================================== c [1mFound solution: 1417[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51133 | 34643 82367 | 11547 12443 404938 32.5 | 22.094 % | c | 51233 | 34643 82367 | 12701 12543 406841 32.4 | 22.098 % | c | 51383 | 34643 82367 | 13971 12693 415156 32.7 | 22.098 % | c | 51608 | 34602 82270 | 15369 12916 422055 32.7 | 22.178 % | c | 51947 | 34602 82270 | 16905 13255 442806 33.4 | 22.178 % | c | 52453 | 34602 82270 | 18596 13761 461213 33.5 | 22.178 % | c ============================================================================== c [1mFound solution: 1404[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 52597 | 34606 82280 | 11535 13905 467095 33.6 | 22.178 % | c | 52697 | 34606 82280 | 12688 14005 470183 33.6 | 22.180 % | c | 52848 | 34606 82280 | 13957 14156 476842 33.7 | 22.180 % | c | 53074 | 34606 82280 | 15353 14382 483083 33.6 | 22.180 % | c | 53411 | 34606 82280 | 16888 14719 490781 33.3 | 22.180 % | c | 53918 | 34606 82280 | 18577 15226 502335 33.0 | 22.180 % | c | 54677 | 34292 81543 | 20434 15982 546741 34.2 | 22.723 % | c | 55816 | 34292 81543 | 22478 17121 612088 35.8 | 22.723 % | c ============================================================================== c [1mFound solution: 1375[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 56923 | 34297 81555 | 11432 18228 678540 37.2 | 22.723 % | c | 57023 | 34297 81555 | 12575 9214 293213 31.8 | 22.725 % | c ============================================================================== c [1mFound solution: 1356[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 57139 | 34304 81571 | 11434 9330 295845 31.7 | 22.725 % | c | 57241 | 34304 81571 | 12577 9432 297556 31.5 | 22.726 % | c | 57391 | 34304 81571 | 13835 9582 300893 31.4 | 22.726 % | c | 57616 | 34304 81571 | 15218 9807 310558 31.7 | 22.726 % | c ============================================================================== c [1mFound solution: 1337[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 57898 | 34309 81583 | 11436 10089 322077 31.9 | 22.726 % | c | 57998 | 34309 81583 | 12579 10189 323845 31.8 | 22.728 % | c | 58149 | 34259 81469 | 13837 10339 326150 31.5 | 22.819 % | c | 58374 | 34241 81428 | 15221 10562 336472 31.9 | 22.853 % | c | 58711 | 34241 81428 | 16743 10899 361196 33.1 | 22.853 % | c | 59217 | 34241 81428 | 18417 11405 371956 32.6 | 22.853 % | c | 59976 | 34168 81259 | 20259 12161 416868 34.3 | 22.991 % | c | 61115 | 34082 81059 | 22285 13297 472342 35.5 | 23.151 % | c ============================================================================== c [1mFound solution: 1312[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 61210 | 34089 81075 | 11363 13392 476347 35.6 | 23.151 % | c | 61311 | 34089 81075 | 12499 13493 483194 35.8 | 23.151 % | c | 61461 | 34089 81075 | 13749 13643 489705 35.9 | 23.151 % | c | 61686 | 34089 81075 | 15124 13868 501226 36.1 | 23.151 % | c ============================================================================== c [1mFound solution: 1311[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 61812 | 34094 81087 | 11364 13994 506283 36.2 | 23.151 % | c ============================================================================== c [1mFound solution: 1308[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 61823 | 34101 81103 | 11367 14005 506542 36.2 | 23.151 % | c | 61923 | 34101 81103 | 12503 14105 513908 36.4 | 23.154 % | c | 62075 | 34101 81103 | 13754 14257 521363 36.6 | 23.153 % | c | 62300 | 34101 81103 | 15129 14482 535416 37.0 | 23.153 % | c | 62639 | 34043 80967 | 16642 14820 543359 36.7 | 23.262 % | c | 63145 | 33977 80813 | 18306 15325 570800 37.2 | 23.394 % | c ============================================================================== c [1mFound solution: 1276[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 63370 | 33993 80853 | 11331 15550 584365 37.6 | 23.394 % | c | 63474 | 33993 80853 | 12464 7879 229194 29.1 | 23.386 % | c | 63624 | 33993 80853 | 13710 8029 235781 29.4 | 23.386 % | c | 63852 | 33993 80853 | 15081 8257 241118 29.2 | 23.386 % | c | 64190 | 33993 80853 | 16589 8595 255628 29.7 | 23.386 % | c | 64696 | 33993 80853 | 18248 9101 265330 29.2 | 23.386 % | c | 65457 | 33993 80853 | 20073 9862 281658 28.6 | 23.386 % | c | 66597 | 33993 80853 | 22080 11002 307035 27.9 | 23.386 % | c | 68305 | 33993 80853 | 24289 12710 368240 29.0 | 23.386 % | c ============================================================================== c [1mFound solution: 1261[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 68916 | 33997 80865 | 11332 13321 404243 30.3 | 23.386 % | c | 69017 | 33997 80865 | 12465 13422 410227 30.6 | 23.388 % | c | 69167 | 33997 80865 | 13711 13572 415038 30.6 | 23.388 % | c | 69392 | 33997 80865 | 15082 13797 425319 30.8 | 23.388 % | c | 69730 | 33997 80865 | 16591 14135 433786 30.7 | 23.388 % | c | 70236 | 33997 80865 | 18250 14641 444412 30.4 | 23.388 % | c | 70995 | 33997 80865 | 20075 15400 501489 32.6 | 23.388 % | c ============================================================================== c [1mFound solution: 1249[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 71760 | 34004 80893 | 11334 16165 543216 33.6 | 23.388 % | c | 71861 | 34004 80893 | 12467 8184 240743 29.4 | 23.387 % | c | 72011 | 34004 80893 | 13714 8334 248316 29.8 | 23.387 % | c | 72237 | 34000 80884 | 15085 8559 258603 30.2 | 23.392 % | c | 72578 | 34000 80884 | 16594 8900 269183 30.2 | 23.392 % | c | 73084 | 34000 80884 | 18253 9406 290102 30.8 | 23.392 % | c ============================================================================== c [1mFound solution: 1233[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 73571 | 34004 80894 | 11334 9893 312372 31.6 | 23.392 % | c | 73671 | 34004 80894 | 12467 9993 316963 31.7 | 23.394 % | c | 73821 | 34004 80894 | 13714 10143 323069 31.9 | 23.394 % | c | 74047 | 34004 80894 | 15085 10369 327866 31.6 | 23.394 % | c | 74385 | 34004 80894 | 16594 10707 342711 32.0 | 23.394 % | c | 74894 | 34004 80894 | 18253 11216 372879 33.2 | 23.394 % | c ============================================================================== c [1mFound solution: 1219[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 75485 | 34009 80905 | 11336 11807 403318 34.2 | 23.394 % | c | 75585 | 34009 80905 | 12469 11907 407498 34.2 | 23.396 % | c | 75735 | 34009 80905 | 13716 12057 413667 34.3 | 23.396 % | c | 75961 | 34009 80905 | 15088 12283 419498 34.2 | 23.396 % | c | 76300 | 34009 80905 | 16597 12622 434871 34.5 | 23.396 % | c | 76810 | 34009 80905 | 18256 13132 456938 34.8 | 23.396 % | c | 77569 | 34009 80905 | 20082 13891 495418 35.7 | 23.396 % | c ============================================================================== c [1mFound solution: 1215[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 78703 | 34014 80916 | 11338 15025 556512 37.0 | 23.396 % | c | 78803 | 34014 80916 | 12471 15125 560304 37.0 | 23.398 % | c | 78955 | 34014 80916 | 13718 15277 567187 37.1 | 23.397 % | c | 79180 | 34014 80916 | 15090 15502 570412 36.8 | 23.397 % | c | 79517 | 34014 80916 | 16599 15839 574576 36.3 | 23.397 % | c | 80024 | 34014 80916 | 18259 16346 584008 35.7 | 23.397 % | c | 80783 | 33957 80784 | 20085 17103 609563 35.6 | 23.506 % | c | 81922 | 33957 80784 | 22094 18242 652586 35.8 | 23.506 % | c | 83631 | 33957 80784 | 24304 19951 738171 37.0 | 23.506 % | c | 86193 | 33957 80784 | 26734 22513 862647 38.3 | 23.506 % | c ============================================================================== c [1mFound solution: 1194[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86651 | 33964 80800 | 11321 22971 879386 38.3 | 23.506 % | c ============================================================================== c [1mFound solution: 1149[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86700 | 33968 80809 | 11322 11535 366925 31.8 | 23.506 % | c ============================================================================== c [1mFound solution: 1145[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86718 | 33973 80820 | 11324 11553 367741 31.8 | 23.506 % | c | 86822 | 33973 80820 | 12456 11657 372147 31.9 | 23.512 % | c | 86973 | 33973 80820 | 13702 11808 379427 32.1 | 23.512 % | c | 87198 | 33973 80820 | 15072 12033 388418 32.3 | 23.512 % | c ============================================================================== c [1mFound solution: 1136[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 87295 | 33982 80843 | 11327 12130 392054 32.3 | 23.512 % | c | 87395 | 33982 80843 | 12459 12230 397615 32.5 | 23.510 % | c | 87546 | 33982 80843 | 13705 12381 401852 32.5 | 23.510 % | c | 87771 | 33982 80843 | 15076 12606 408267 32.4 | 23.510 % | c | 88111 | 33982 80843 | 16583 12946 416712 32.2 | 23.510 % | c | 88617 | 33982 80843 | 18242 13452 438552 32.6 | 23.510 % | c | 89376 | 33982 80843 | 20066 14211 467515 32.9 | 23.510 % | c | 90515 | 33982 80843 | 22073 15350 505978 33.0 | 23.510 % | c | 92223 | 33982 80843 | 24280 17058 574942 33.7 | 23.510 % | c | 94785 | 33946 80759 | 26708 19618 651326 33.2 | 23.573 % | c ============================================================================== c [1mFound solution: 1128[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 98336 | 33952 80774 | 11317 23169 802322 34.6 | 23.573 % | c | 98438 | 33952 80774 | 12448 11687 310808 26.6 | 23.573 % | c | 98588 | 33952 80774 | 13693 11837 317230 26.8 | 23.573 % | c | 98817 | 33952 80774 | 15062 12066 326295 27.0 | 23.573 % | c | 99155 | 33952 80774 | 16569 12404 336095 27.1 | 23.573 % | c | 99661 | 33952 80774 | 18226 12910 359193 27.8 | 23.573 % | c | 100420 | 33952 80774 | 20048 13669 396157 29.0 | 23.573 % | c | 101560 | 33952 80774 | 22053 14809 437250 29.5 | 23.573 % | c | 103268 | 33952 80774 | 24258 16517 516374 31.3 | 23.573 % | c | 105830 | 33952 80774 | 26684 19079 624783 32.7 | 23.573 % | c | 109676 | 33952 80774 | 29353 22925 762667 33.3 | 23.573 % | c | 115442 | 33952 80774 | 32288 28691 989080 34.5 | 23.573 % | c | 124092 | 33952 80774 | 35517 37341 1393060 37.3 | 23.573 % | c ============================================================================== c [1mFound solution: 1120[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 3 13 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 136193 | 33955 80781 | 11318 26816 1021714 38.1 | 23.573 % | c | 136293 | 33955 80781 | 12449 13508 480514 35.6 | 23.576 % | c | 136444 | 33939 80744 | 13694 13658 485170 35.5 | 23.605 % | c | 136669 | 33939 80744 | 15064 13883 491212 35.4 | 23.605 % | c | 137006 | 33939 80744 | 16570 14220 500993 35.2 | 23.605 % | c | 137516 | 33939 80744 | 18227 14730 521903 35.4 | 23.605 % | c | 138276 | 33939 80744 | 20050 15490 536341 34.6 | 23.605 % | c | 139416 | 33939 80744 | 22055 16630 592086 35.6 | 23.605 % | c | 141124 | 33939 80744 | 24261 18338 662753 36.1 | 23.605 % | c | 143686 | 33939 80744 | 26687 20900 767136 36.7 | 23.605 % | c | 147530 | 33939 80744 | 29355 24744 895353 36.2 | 23.605 % | c | 153296 | 33793 80407 | 32291 30507 1148443 37.6 | 23.901 % | c ============================================================================== c [1mOptimal solution: 1120[0m s OPTIMUM FOUND v C101_bit0 C102_bit0 -C103_bit0 -C104_bit0 -C105_bit0 -C108_bit0 -C111_bit0 -C112_bit0 -C113_bit0 C114_bit0 -C115_bit0 -C116_bit0 -C117_bit0 -C118_bit0 -C119_bit0 -C120_bit0 -C121_bit0 -C122_bit0 -C123_bit0 -C124_bit0 -C125_bit0 -C126_bit0 C127_bit0 -C128_bit0 -C129_bit0 -C130_bit0 -C131_bit0 -C132_bit0 -C133_bit0 -C134_bit0 C135_bit0 -C136_bit0 -C137_bit0 -C138_bit0 C139_bit0 -C140_bit0 -C141_bit0 -C142_bit0 C143_bit0 -C144_bit0 -C145_bit0 -C146_bit0 -C147_bit0 -C148_bit0 -C149_bit0 -C150_bit0 C151_bit0 -C152_bit0 C153_bit0 -C154_bit0 -C155_bit0 -C156_bit0 -C157_bit0 -C158_bit0 -C159_bit0 -C160_bit0 -C161_bit0 -C162_bit0 -C163_bit0 C164_bit0 -C165_bit0 C166_bit0 -C167_bit0 -C168_bit0 -C169_bit0 -C170_bit0 -C171_bit0 -C172_bit0 -C173_bit0 -C174_bit0 -C175_bit0 -C176_bit0 -C177_bit0 -C178_bit0 -C179_bit0 -C180_bit0 -C181_bit0 -C182_bit0 -C183_bit0 -C184_bit0 -C185_bit0 C186_bit0 -C187_bit0 -C188_bit0 -C189_bit0 -C106_bit0 C107_bit0 -C109_bit0 -C110_bit0 c _______________________________________________________________________________ c c restarts : 247 c conflicts : 155748 (235 /sec) c decisions : 277901 (419 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 662.518 s c _______________________________________________________________________________ #### 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.64 0.89 0.93 2/54 25175 Raw data (stat): 25175 (runsolver) R 25174 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491885068 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0004 s] Raw data (loadavg): 0.70 0.90 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 1827 0 0 0 994 4 0 0 25 0 1 0 491885068 10072064 1794 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2459 1794 603 41 0 2418 0 vsize: 9836 [startup+20.001 s] Raw data (loadavg): 0.75 0.90 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2021 0 0 0 1993 5 0 0 25 0 1 0 491885068 10964992 1988 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2677 1988 603 41 0 2636 0 vsize: 10708 [startup+30.0011 s] Raw data (loadavg): 0.78 0.90 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2178 0 0 0 2992 6 0 0 25 0 1 0 491885068 11632640 2145 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2840 2145 603 41 0 2799 0 vsize: 11360 [startup+40.0016 s] Raw data (loadavg): 0.82 0.90 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2323 0 0 0 3992 7 0 0 25 0 1 0 491885068 12115968 2290 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2958 2290 603 41 0 2917 0 vsize: 11832 [startup+50.0029 s] Raw data (loadavg): 0.84 0.91 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2504 0 0 0 4991 8 0 0 25 0 1 0 491885068 12914688 2471 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3153 2471 603 41 0 3112 0 vsize: 12612 [startup+60.0031 s] Raw data (loadavg): 0.87 0.91 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2635 0 0 0 5991 8 0 0 25 0 1 0 491885068 13414400 2602 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3275 2602 603 41 0 3234 0 vsize: 13100 [startup+70.0032 s] Raw data (loadavg): 0.89 0.91 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2761 0 0 0 6990 9 0 0 25 0 1 0 491885068 13946880 2728 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3405 2728 603 41 0 3364 0 vsize: 13620 [startup+80.0038 s] Raw data (loadavg): 0.90 0.91 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2783 0 0 0 7990 9 0 0 25 0 1 0 491885068 14077952 2750 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3437 2750 603 41 0 3396 0 vsize: 13748 [startup+90.004 s] Raw data (loadavg): 0.92 0.92 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2785 0 0 0 8990 9 0 0 25 0 1 0 491885068 14077952 2752 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3437 2752 603 41 0 3396 0 vsize: 13748 [startup+100.005 s] Raw data (loadavg): 0.93 0.92 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2785 0 0 0 9990 9 0 0 25 0 1 0 491885068 14077952 2752 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3437 2752 603 41 0 3396 0 vsize: 13748 [startup+110.006 s] Raw data (loadavg): 0.94 0.92 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2786 0 0 0 10990 10 0 0 25 0 1 0 491885068 14077952 2753 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3437 2753 603 41 0 3396 0 vsize: 13748 [startup+120.006 s] Raw data (loadavg): 0.95 0.92 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2786 0 0 0 11990 10 0 0 25 0 1 0 491885068 14077952 2753 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3437 2753 603 41 0 3396 0 vsize: 13748 [startup+130.007 s] Raw data (loadavg): 0.96 0.92 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2786 0 0 0 12990 10 0 0 25 0 1 0 491885068 14077952 2753 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3437 2753 603 41 0 3396 0 vsize: 13748 [startup+140.008 s] Raw data (loadavg): 0.96 0.93 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2786 0 0 0 13990 10 0 0 25 0 1 0 491885068 14077952 2753 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3437 2753 603 41 0 3396 0 vsize: 13748 [startup+150.009 s] Raw data (loadavg): 0.97 0.93 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2827 0 0 0 14990 10 0 0 25 0 1 0 491885068 14213120 2794 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3470 2794 603 41 0 3429 0 vsize: 13880 [startup+160.009 s] Raw data (loadavg): 0.97 0.93 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2861 0 0 0 15989 10 0 0 25 0 1 0 491885068 14344192 2828 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2828 603 41 0 3461 0 vsize: 14008 [startup+170.008 s] Raw data (loadavg): 0.98 0.93 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2861 0 0 0 16990 10 0 0 25 0 1 0 491885068 14344192 2828 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2828 603 41 0 3461 0 vsize: 14008 [startup+180.008 s] Raw data (loadavg): 0.98 0.93 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2861 0 0 0 17990 10 0 0 25 0 1 0 491885068 14344192 2828 4294967295 134512640 134672761 3221224624 3221223728 134560361 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2828 603 41 0 3461 0 vsize: 14008 [startup+190.008 s] Raw data (loadavg): 0.98 0.94 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2861 0 0 0 18990 10 0 0 25 0 1 0 491885068 14344192 2828 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2828 603 41 0 3461 0 vsize: 14008 [startup+200.009 s] Raw data (loadavg): 0.98 0.94 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2861 0 0 0 19990 11 0 0 25 0 1 0 491885068 14344192 2828 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2828 603 41 0 3461 0 vsize: 14008 [startup+210.008 s] Raw data (loadavg): 0.99 0.94 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2862 0 0 0 20990 11 0 0 25 0 1 0 491885068 14344192 2829 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2829 603 41 0 3461 0 vsize: 14008 [startup+220.009 s] Raw data (loadavg): 0.99 0.94 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2862 0 0 0 21990 11 0 0 25 0 1 0 491885068 14344192 2829 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2829 603 41 0 3461 0 vsize: 14008 [startup+230.009 s] Raw data (loadavg): 0.99 0.94 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2862 0 0 0 22990 11 0 0 25 0 1 0 491885068 14344192 2829 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2829 603 41 0 3461 0 vsize: 14008 [startup+240.008 s] Raw data (loadavg): 0.99 0.94 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2862 0 0 0 23990 11 0 0 25 0 1 0 491885068 14344192 2829 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2829 603 41 0 3461 0 vsize: 14008 [startup+250.009 s] Raw data (loadavg): 0.99 0.94 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2862 0 0 0 24991 11 0 0 25 0 1 0 491885068 14344192 2829 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2829 603 41 0 3461 0 vsize: 14008 [startup+260.01 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2862 0 0 0 25991 11 0 0 25 0 1 0 491885068 14344192 2829 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2829 603 41 0 3461 0 vsize: 14008 [startup+270.009 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2870 0 0 0 26991 11 0 0 25 0 1 0 491885068 14344192 2837 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2837 603 41 0 3461 0 vsize: 14008 [startup+280.009 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2870 0 0 0 27991 11 0 0 25 0 1 0 491885068 14344192 2837 4294967295 134512640 134672761 3221224624 3221223808 134558667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2837 603 41 0 3461 0 vsize: 14008 [startup+290.01 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2870 0 0 0 28991 11 0 0 25 0 1 0 491885068 14344192 2837 4294967295 134512640 134672761 3221224624 3221223792 134561264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3502 2837 603 41 0 3461 0 vsize: 14008 [startup+300.01 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2874 0 0 0 29991 11 0 0 25 0 1 0 491885068 14462976 2841 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3531 2841 603 41 0 3490 0 vsize: 14124 [startup+310.01 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2874 0 0 0 30991 11 0 0 25 0 1 0 491885068 14462976 2841 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3531 2841 603 41 0 3490 0 vsize: 14124 [startup+320.01 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2874 0 0 0 31992 11 0 0 25 0 1 0 491885068 14462976 2841 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3531 2841 603 41 0 3490 0 vsize: 14124 [startup+330.01 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2993 0 0 0 32992 11 0 0 25 0 1 0 491885068 14856192 2960 4294967295 134512640 134672761 3221224624 3221223728 134554671 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3627 2960 603 41 0 3586 0 vsize: 14508 [startup+340.01 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2993 0 0 0 33992 11 0 0 25 0 1 0 491885068 14856192 2960 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3627 2960 603 41 0 3586 0 vsize: 14508 [startup+350.011 s] Raw data (loadavg): 0.99 0.95 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 2993 0 0 0 34992 11 0 0 25 0 1 0 491885068 14856192 2960 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3627 2960 603 41 0 3586 0 vsize: 14508 [startup+360.011 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3000 0 0 0 35992 11 0 0 25 0 1 0 491885068 14999552 2967 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3662 2967 603 41 0 3621 0 vsize: 14648 [startup+370.011 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3000 0 0 0 36992 11 0 0 25 0 1 0 491885068 14999552 2967 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3662 2967 603 41 0 3621 0 vsize: 14648 [startup+380.011 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3008 0 0 0 37993 11 0 0 25 0 1 0 491885068 14999552 2975 4294967295 134512640 134672761 3221224624 3221223808 134558338 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3662 2975 603 41 0 3621 0 vsize: 14648 [startup+390.011 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3018 0 0 0 38993 11 0 0 25 0 1 0 491885068 14999552 2985 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3662 2985 603 41 0 3621 0 vsize: 14648 [startup+400.012 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3018 0 0 0 39993 11 0 0 25 0 1 0 491885068 14999552 2985 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3662 2985 603 41 0 3621 0 vsize: 14648 [startup+410.012 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3018 0 0 0 40993 11 0 0 25 0 1 0 491885068 14999552 2985 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3662 2985 603 41 0 3621 0 vsize: 14648 [startup+420.012 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3026 0 0 0 41993 12 0 0 25 0 1 0 491885068 14999552 2993 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3662 2993 603 41 0 3621 0 vsize: 14648 [startup+430.013 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3026 0 0 0 42993 12 0 0 25 0 1 0 491885068 14999552 2993 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3662 2993 603 41 0 3621 0 vsize: 14648 [startup+440.012 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3027 0 0 0 43993 12 0 0 25 0 1 0 491885068 14999552 2994 4294967295 134512640 134672761 3221224624 3221223728 134559910 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3662 2994 603 41 0 3621 0 vsize: 14648 [startup+450.013 s] Raw data (loadavg): 0.99 0.96 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3081 0 0 0 44993 12 0 0 25 0 1 0 491885068 15261696 3048 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3726 3048 603 41 0 3685 0 vsize: 14904 [startup+460.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3192 0 0 0 45993 12 0 0 25 0 1 0 491885068 15798272 3159 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3857 3159 603 41 0 3816 0 vsize: 15428 [startup+470.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3306 0 0 0 46993 13 0 0 25 0 1 0 491885068 16191488 3273 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3953 3273 603 41 0 3912 0 vsize: 15812 [startup+480.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3411 0 0 0 47992 14 0 0 25 0 1 0 491885068 16588800 3378 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4050 3378 603 41 0 4009 0 vsize: 16200 [startup+490.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3513 0 0 0 48992 14 0 0 25 0 1 0 491885068 17244160 3480 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4210 3480 603 41 0 4169 0 vsize: 16840 [startup+500.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3622 0 0 0 49992 14 0 0 25 0 1 0 491885068 17645568 3589 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4308 3589 603 41 0 4267 0 vsize: 17232 [startup+510.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3721 0 0 0 50992 15 0 0 25 0 1 0 491885068 18055168 3688 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4408 3688 603 41 0 4367 0 vsize: 17632 [startup+520.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3809 0 0 0 51991 15 0 0 25 0 1 0 491885068 18456576 3776 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4506 3776 603 41 0 4465 0 vsize: 18024 [startup+530.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3903 0 0 0 52991 16 0 0 25 0 1 0 491885068 18853888 3870 4294967295 134512640 134672761 3221224624 3221223616 134565768 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3870 603 41 0 4562 0 vsize: 18412 [startup+540.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3903 0 0 0 53991 16 0 0 25 0 1 0 491885068 18853888 3870 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3870 603 41 0 4562 0 vsize: 18412 [startup+550.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3905 0 0 0 54992 16 0 0 25 0 1 0 491885068 18853888 3872 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3872 603 41 0 4562 0 vsize: 18412 [startup+560.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3908 0 0 0 55992 16 0 0 25 0 1 0 491885068 18853888 3875 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3875 603 41 0 4562 0 vsize: 18412 [startup+570.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3916 0 0 0 56992 16 0 0 25 0 1 0 491885068 18853888 3883 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3883 603 41 0 4562 0 vsize: 18412 [startup+580.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3917 0 0 0 57992 16 0 0 25 0 1 0 491885068 18853888 3884 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3884 603 41 0 4562 0 vsize: 18412 [startup+590.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3917 0 0 0 58993 16 0 0 25 0 1 0 491885068 18853888 3884 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3884 603 41 0 4562 0 vsize: 18412 [startup+600.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3918 0 0 0 59993 16 0 0 25 0 1 0 491885068 18853888 3885 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3885 603 41 0 4562 0 vsize: 18412 [startup+610.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3920 0 0 0 60993 16 0 0 25 0 1 0 491885068 18853888 3887 4294967295 134512640 134672761 3221224624 3221223760 134560579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3887 603 41 0 4562 0 vsize: 18412 [startup+620.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3921 0 0 0 61993 16 0 0 25 0 1 0 491885068 18853888 3888 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3888 603 41 0 4562 0 vsize: 18412 [startup+630.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3921 0 0 0 62993 16 0 0 25 0 1 0 491885068 18853888 3888 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3888 603 41 0 4562 0 vsize: 18412 [startup+640.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3933 0 0 0 63993 16 0 0 25 0 1 0 491885068 18853888 3900 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3900 603 41 0 4562 0 vsize: 18412 [startup+650.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3933 0 0 0 64994 16 0 0 25 0 1 0 491885068 18853888 3900 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4603 3900 603 41 0 4562 0 vsize: 18412 [startup+660.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3949 0 0 0 65994 16 0 0 25 0 1 0 491885068 19017728 3916 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4643 3916 603 41 0 4602 0 vsize: 18572 [startup+662.609 s] Raw data (loadavg): 0.99 0.97 0.93 1/53 25175 Raw data (stat): 25175 (minisat+) R 25174 22932 22931 0 -1 0 3949 0 0 0 65994 16 0 0 25 0 1 0 491885068 19017728 3916 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4643 3916 603 41 0 4602 0 vsize: 0 Child status: 30 Real time (s): 662.609 CPU time (s): 662.695 CPU user time (s): 662.523 CPU system time (s): 0.171973 CPU usage (%): 100.013 Max. virtual memory (Kb): 18572 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1120 #### END VERIFIER DATA ####