Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-mod008.opb |
MD5SUM | 581d778a36086562107993896110e0a2 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 307 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 319 |
Biggest coefficient in the objective function | 87 |
Number of bits for the biggest coefficient in the objective function | 7 |
Sum of the numbers in the objective function | 23554 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 22000 |
Number of bits of the biggest number in a constraint | 15 |
Biggest sum of numbers in a constraint | 1027256 |
Number of bits of the biggest sum of numbers | 20 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.01784 |
Number of variables | 319 |
Total number of constraints | 325 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 319 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 231 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc19 THE 2005-04-21 23:09:21 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13634 boxname=wulflinc19 idbench=1049 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 581d778a36086562107993896110e0a2 /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-mod008.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-mod008.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-mod008.opb IDLAUNCH: 13634 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 3 cpu MHz : 451.037 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: 617856 kB Buffers: 29844 kB Cached: 363316 kB SwapCached: 560 kB Active: 135456 kB Inactive: 259780 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 617604 kB SwapTotal: 2097892 kB SwapFree: 2096388 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5168 kB Slab: 15900 kB Committed_AS: 63816 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 23:29:23 (client local time) WITH STATUS 10 IN 1200.07 SECONDS stats: 13634 7 1200.07 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 6 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): sss c ---[ 8]---> Adder-cost: 2481 maxlim: 21999 bits: 16/15 c ---[ 5]---> Adder-cost: 2052 maxlim: 4999 bits: 14/13 c ---[ 4]---> Adder-cost: 2306 maxlim: 11999 bits: 15/14 c ---[ 2]---> Adder-cost: 1315 maxlim: 1199 bits: 12/11 c ---[ 1]---> Adder-cost: 1522 maxlim: 2099 bits: 13/12 c ---[ 0]---> Adder-cost: 1797 maxlim: 3999 bits: 13/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 76857 275259 | 25619 0 0 nan | 0.000 % | c | 100 | 76857 275259 | 28180 100 349 3.5 | 0.295 % | c | 250 | 76857 275259 | 30998 250 989 4.0 | 0.295 % | c | 475 | 76857 275259 | 34098 475 2362 5.0 | 0.295 % | c | 812 | 76857 275259 | 37508 812 5564 6.9 | 0.295 % | c | 1318 | 76857 275259 | 41259 1318 9284 7.0 | 0.295 % | c | 2078 | 76857 275259 | 45385 2078 19038 9.2 | 0.295 % | c ============================================================================== c [1mFound solution: 1931[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 1828 maxlim: 21623 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2678 | 89543 320552 | 29847 2678 24935 9.3 | 0.295 % | c | 2778 | 89543 320552 | 32831 2778 26152 9.4 | 0.337 % | c | 2929 | 89543 320552 | 36114 2929 27633 9.4 | 0.337 % | c | 3154 | 89543 320552 | 39726 3154 29393 9.3 | 0.337 % | c | 3491 | 89543 320552 | 43698 3491 32994 9.5 | 0.337 % | c | 3997 | 89543 320552 | 48068 3997 37843 9.5 | 0.337 % | c | 4756 | 89543 320552 | 52875 4756 49159 10.3 | 0.337 % | c | 5897 | 89543 320552 | 58163 5897 168561 28.6 | 0.337 % | c | 7605 | 89510 320441 | 63979 7600 178160 23.4 | 0.382 % | c | 10168 | 89510 320441 | 70377 10163 226253 22.3 | 0.382 % | c | 14012 | 89510 320441 | 77415 14007 371624 26.5 | 0.382 % | c | 19778 | 89510 320441 | 85156 19773 607932 30.7 | 0.382 % | c | 28428 | 89510 320441 | 93672 28423 1292382 45.5 | 0.382 % | c | 41403 | 89510 320441 | 103039 41398 2357260 56.9 | 0.382 % | c ============================================================================== c [1mFound solution: 1848[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 21706 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54059 | 89531 320545 | 29843 54054 3961992 73.3 | 0.382 % | c | 54162 | 89531 320545 | 32827 15292 1592576 104.1 | 0.420 % | c | 54312 | 89531 320545 | 36110 15442 1593483 103.2 | 0.420 % | c | 54537 | 89531 320545 | 39721 15667 1596982 101.9 | 0.420 % | c | 54875 | 89531 320545 | 43693 16005 1602668 100.1 | 0.420 % | c | 55381 | 89531 320545 | 48062 16511 1613704 97.7 | 0.420 % | c | 56143 | 89531 320545 | 52868 17273 1650155 95.5 | 0.420 % | c | 57282 | 89531 320545 | 58155 18412 1696606 92.1 | 0.420 % | c | 58991 | 89531 320545 | 63971 20121 1829381 90.9 | 0.420 % | c | 61553 | 89531 320545 | 70368 22683 1980310 87.3 | 0.420 % | c | 65398 | 89531 320545 | 77405 26528 2168363 81.7 | 0.420 % | c ============================================================================== c [1mFound solution: 1769[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 21785 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 70558 | 89538 320589 | 29846 31688 2707051 85.4 | 0.420 % | c | 70660 | 89538 320589 | 32830 15536 898016 57.8 | 0.449 % | c | 70810 | 89538 320589 | 36113 15686 900279 57.4 | 0.449 % | c | 71035 | 89529 320558 | 39725 15901 904385 56.9 | 0.457 % | c | 71372 | 89529 320558 | 43697 16238 915276 56.4 | 0.457 % | c | 71880 | 89529 320558 | 48067 16746 927203 55.4 | 0.457 % | c | 72639 | 89529 320558 | 52874 17505 959636 54.8 | 0.457 % | c | 73779 | 89529 320558 | 58161 18645 1023755 54.9 | 0.457 % | c | 75487 | 89529 320558 | 63977 20353 1113996 54.7 | 0.457 % | c | 78049 | 89529 320558 | 70375 22915 1190720 52.0 | 0.457 % | c | 81894 | 89529 320558 | 77412 26760 1574240 58.8 | 0.457 % | c | 87661 | 89529 320558 | 85154 32527 1806448 55.5 | 0.457 % | c | 96312 | 89529 320558 | 93669 41178 2513161 61.0 | 0.457 % | c | 109286 | 89529 320558 | 103036 54152 3635289 67.1 | 0.457 % | c | 128747 | 89529 320558 | 113340 73613 5739322 78.0 | 0.457 % | c ============================================================================== c [1mFound solution: 1739[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 21815 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 133466 | 89533 320587 | 29844 78332 6147778 78.5 | 0.457 % | c | 133567 | 89533 320587 | 32828 18672 1409334 75.5 | 0.479 % | c | 133717 | 89533 320587 | 36111 18822 1410854 75.0 | 0.479 % | c | 133942 | 89524 320556 | 39722 19041 1414922 74.3 | 0.487 % | c | 134279 | 89524 320556 | 43694 19378 1422933 73.4 | 0.487 % | c | 134788 | 89498 320466 | 48064 19875 1449674 72.9 | 0.517 % | c | 135547 | 89498 320466 | 52870 20634 1490582 72.2 | 0.517 % | c | 136686 | 89498 320466 | 58157 21773 1505141 69.1 | 0.517 % | c | 138396 | 89498 320466 | 63973 23483 1570444 66.9 | 0.517 % | c | 140960 | 89498 320466 | 70370 26047 1682244 64.6 | 0.517 % | c | 144804 | 89498 320466 | 77407 29891 1991777 66.6 | 0.517 % | c | 150570 | 89498 320466 | 85148 35657 2263637 63.5 | 0.517 % | c | 159219 | 89498 320466 | 93663 44306 2944918 66.5 | 0.517 % | c | 172196 | 89498 320466 | 103029 57283 4042943 70.6 | 0.517 % | c | 191659 | 89498 320466 | 113332 76746 5737800 74.8 | 0.517 % | c ============================================================================== c [1mFound solution: 946[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22608 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 196345 | 89445 320200 | 29815 63587 4160391 65.4 | 0.517 % | c | 196445 | 89445 320200 | 32796 14131 678279 48.0 | 0.621 % | c | 196596 | 89445 320200 | 36076 14282 680874 47.7 | 0.621 % | c | 196821 | 89445 320200 | 39683 14507 688020 47.4 | 0.621 % | c | 197158 | 89445 320200 | 43652 14844 710964 47.9 | 0.621 % | c | 197664 | 89445 320200 | 48017 15350 728038 47.4 | 0.621 % | c | 198423 | 89445 320200 | 52819 16109 791575 49.1 | 0.621 % | c | 199563 | 89445 320200 | 58101 17249 880814 51.1 | 0.621 % | c | 201271 | 89445 320200 | 63911 18957 1016739 53.6 | 0.621 % | c | 203833 | 89445 320200 | 70302 21519 1242229 57.7 | 0.621 % | c | 207677 | 89445 320200 | 77332 25363 1594865 62.9 | 0.621 % | c | 213445 | 89445 320200 | 85065 31131 2149941 69.1 | 0.621 % | c | 222096 | 89445 320200 | 93572 39782 3063330 77.0 | 0.621 % | c | 235070 | 89445 320200 | 102929 52756 4470065 84.7 | 0.621 % | c ============================================================================== c [1mFound solution: 911[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22643 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 251560 | 89450 320229 | 29816 69246 6339367 91.5 | 0.621 % | c | 251660 | 89450 320229 | 32797 18390 1432400 77.9 | 0.643 % | c | 251810 | 89450 320229 | 36077 18540 1436537 77.5 | 0.644 % | c | 252040 | 89450 320229 | 39685 18770 1451042 77.3 | 0.643 % | c | 252378 | 89450 320229 | 43653 19108 1466905 76.8 | 0.643 % | c | 252885 | 89450 320229 | 48018 19615 1504665 76.7 | 0.643 % | c | 253644 | 89450 320229 | 52820 20374 1560056 76.6 | 0.643 % | c | 254783 | 89450 320229 | 58102 21513 1654788 76.9 | 0.643 % | c | 256493 | 89450 320229 | 63913 23223 1785510 76.9 | 0.643 % | c | 259055 | 89450 320229 | 70304 25785 1958197 75.9 | 0.643 % | c | 262900 | 89450 320229 | 77335 29630 2239296 75.6 | 0.643 % | c | 268666 | 89450 320229 | 85068 35396 2714258 76.7 | 0.643 % | c | 277315 | 89450 320229 | 93575 44045 3376127 76.7 | 0.643 % | c ============================================================================== c [1mFound solution: 770[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22784 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 279769 | 89453 320247 | 29817 46499 3620727 77.9 | 0.643 % | c | 279869 | 89427 320157 | 32798 16830 1006352 59.8 | 0.688 % | c | 280019 | 89427 320157 | 36078 16980 1012513 59.6 | 0.688 % | c | 280248 | 89427 320157 | 39686 17209 1028073 59.7 | 0.688 % | c | 280588 | 89427 320157 | 43655 17549 1053941 60.1 | 0.688 % | c | 281097 | 89341 319859 | 48020 18011 1088494 60.4 | 0.793 % | c | 281856 | 89341 319859 | 52822 18770 1143730 60.9 | 0.793 % | c | 282995 | 89341 319859 | 58104 19909 1244248 62.5 | 0.793 % | c ============================================================================== c [1mFound solution: 749[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22805 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 284349 | 89348 319898 | 29782 21263 1345616 63.3 | 0.793 % | c | 284450 | 89348 319898 | 32760 21364 1352753 63.3 | 0.815 % | c | 284604 | 89348 319898 | 36036 21518 1361183 63.3 | 0.815 % | c | 284829 | 89348 319898 | 39639 21743 1377474 63.4 | 0.815 % | c | 285166 | 89348 319898 | 43603 22080 1390687 63.0 | 0.815 % | c | 285672 | 89348 319898 | 47964 22586 1414527 62.6 | 0.815 % | c ============================================================================== c [1mFound solution: 741[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22813 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 286300 | 89352 319930 | 29784 23214 1454021 62.6 | 0.815 % | c | 286400 | 89352 319930 | 32762 23314 1458066 62.5 | 0.837 % | c | 286551 | 89352 319930 | 36038 23465 1467784 62.6 | 0.837 % | c | 286776 | 89352 319930 | 39642 23690 1481349 62.5 | 0.837 % | c | 287116 | 89352 319930 | 43606 24030 1500314 62.4 | 0.837 % | c | 287622 | 89352 319930 | 47967 24536 1529161 62.3 | 0.837 % | c | 288382 | 89352 319930 | 52764 25296 1584096 62.6 | 0.837 % | c | 289521 | 89352 319930 | 58040 26435 1669747 63.2 | 0.837 % | c | 291229 | 89352 319930 | 63844 28143 1799237 63.9 | 0.837 % | c | 293792 | 89352 319930 | 70229 30706 1972225 64.2 | 0.837 % | c | 297636 | 89352 319930 | 77252 34550 2247972 65.1 | 0.837 % | c | 303402 | 89352 319930 | 84977 40316 2660851 66.0 | 0.837 % | c | 312052 | 89352 319930 | 93474 48966 3274473 66.9 | 0.837 % | c | 325028 | 89352 319930 | 102822 61942 4241149 68.5 | 0.837 % | c ============================================================================== c [1mFound solution: 689[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22865 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 328455 | 89356 319957 | 29785 65369 4571282 69.9 | 0.837 % | c | 328557 | 89356 319957 | 32763 18757 1074267 57.3 | 0.859 % | c | 328708 | 89356 319957 | 36039 18908 1086451 57.5 | 0.859 % | c | 328935 | 89356 319957 | 39643 19135 1100616 57.5 | 0.859 % | c | 329272 | 89356 319957 | 43608 19472 1127436 57.9 | 0.859 % | c | 329782 | 89356 319957 | 47969 19982 1166638 58.4 | 0.859 % | c | 330542 | 89356 319957 | 52765 20742 1214476 58.6 | 0.859 % | c | 331681 | 89356 319957 | 58042 21881 1299360 59.4 | 0.859 % | c | 333390 | 89356 319957 | 63846 23590 1448384 61.4 | 0.859 % | c | 335955 | 89356 319957 | 70231 26155 1643941 62.9 | 0.859 % | c ============================================================================== c [1mFound solution: 681[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22873 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 338761 | 89360 319980 | 29786 28961 1945896 67.2 | 0.859 % | c | 338862 | 89360 319980 | 32764 29062 1947465 67.0 | 0.874 % | c | 339012 | 89360 319980 | 36041 29212 1953623 66.9 | 0.874 % | c | 339237 | 89360 319980 | 39645 29437 1975036 67.1 | 0.874 % | c | 339574 | 89360 319980 | 43609 29774 1988516 66.8 | 0.874 % | c | 340080 | 89360 319980 | 47970 30280 2027818 67.0 | 0.874 % | c | 340839 | 89360 319980 | 52767 31039 2085626 67.2 | 0.874 % | c ============================================================================== c [1mFound solution: 657[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22897 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 341314 | 89366 320012 | 29788 31514 2129230 67.6 | 0.874 % | c | 341414 | 89366 320012 | 32766 15857 930079 58.7 | 0.896 % | c | 341564 | 89366 320012 | 36043 16007 946090 59.1 | 0.896 % | c | 341789 | 89366 320012 | 39647 16232 967115 59.6 | 0.896 % | c | 342127 | 89366 320012 | 43612 16570 997471 60.2 | 0.896 % | c | 342633 | 89366 320012 | 47973 17076 1035864 60.7 | 0.896 % | c | 343394 | 89366 320012 | 52771 17837 1106067 62.0 | 0.896 % | c ============================================================================== c [1mFound solution: 636[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22918 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 343979 | 89371 320052 | 29790 18422 1157747 62.8 | 0.896 % | c | 344081 | 89371 320052 | 32769 18524 1160795 62.7 | 0.926 % | c | 344231 | 89371 320052 | 36045 18674 1169790 62.6 | 0.926 % | c | 344459 | 89371 320052 | 39650 18902 1185454 62.7 | 0.926 % | c | 344797 | 89371 320052 | 43615 19240 1215432 63.2 | 0.926 % | c | 345303 | 89371 320052 | 47977 19746 1248021 63.2 | 0.926 % | c | 346062 | 89371 320052 | 52774 20505 1318239 64.3 | 0.926 % | c ============================================================================== c [1mFound solution: 635[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22919 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 347023 | 89373 320063 | 29791 21466 1395363 65.0 | 0.926 % | c | 347123 | 89373 320063 | 32770 21566 1399600 64.9 | 0.933 % | c | 347275 | 89373 320063 | 36047 21718 1410545 64.9 | 0.933 % | c | 347501 | 89373 320063 | 39651 21944 1431487 65.2 | 0.933 % | c | 347839 | 89373 320063 | 43617 22282 1446347 64.9 | 0.933 % | c | 348347 | 89373 320063 | 47978 22790 1487027 65.2 | 0.933 % | c | 349106 | 89373 320063 | 52776 23549 1551551 65.9 | 0.933 % | c ============================================================================== c [1mFound solution: 563[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 22991 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 349336 | 89376 320079 | 29792 23779 1570821 66.1 | 0.933 % | c | 349436 | 89376 320079 | 32771 23879 1572338 65.8 | 0.948 % | c | 349587 | 89376 320079 | 36048 24030 1584564 65.9 | 0.948 % | c | 349812 | 89376 320079 | 39653 24255 1595306 65.8 | 0.948 % | c ============================================================================== c [1mFound solution: 546[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23008 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 349973 | 89330 319927 | 29776 24379 1607855 66.0 | 0.948 % | c | 350076 | 89330 319927 | 32753 24482 1613253 65.9 | 1.022 % | c | 350227 | 89330 319927 | 36028 24633 1624363 65.9 | 1.022 % | c | 350454 | 89330 319927 | 39631 24860 1638779 65.9 | 1.022 % | c | 350791 | 89330 319927 | 43595 25197 1660811 65.9 | 1.022 % | c | 351297 | 89330 319927 | 47954 25703 1706767 66.4 | 1.022 % | c | 352058 | 89330 319927 | 52750 26464 1768930 66.8 | 1.022 % | c ============================================================================== c [1mFound solution: 520[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23034 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 352787 | 89338 319969 | 29779 27193 1832145 67.4 | 1.022 % | c | 352887 | 89338 319969 | 32756 27293 1835973 67.3 | 1.051 % | c | 353037 | 89338 319969 | 36032 27443 1851592 67.5 | 1.051 % | c | 353263 | 89338 319969 | 39635 27669 1862417 67.3 | 1.051 % | c | 353600 | 89338 319969 | 43599 28006 1873654 66.9 | 1.051 % | c | 354106 | 89338 319969 | 47959 28512 1912744 67.1 | 1.051 % | c | 354865 | 89338 319969 | 52755 29271 1963916 67.1 | 1.051 % | c | 356004 | 89338 319969 | 58030 30410 2080531 68.4 | 1.051 % | c | 357712 | 89338 319969 | 63833 32118 2225201 69.3 | 1.051 % | c | 360276 | 89338 319969 | 70217 34682 2431286 70.1 | 1.051 % | c | 364123 | 89338 319969 | 77239 38529 2599173 67.5 | 1.051 % | c ============================================================================== c [1mFound solution: 480[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23074 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 364642 | 89281 319630 | 29760 33995 2124305 62.5 | 1.051 % | c | 364744 | 89281 319630 | 32736 17100 816807 47.8 | 1.148 % | c ============================================================================== c [1mFound solution: 420[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23134 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 364775 | 89293 319683 | 29764 17131 820083 47.9 | 1.148 % | c | 364875 | 89293 319683 | 32740 17231 823221 47.8 | 1.191 % | c | 365025 | 89293 319683 | 36014 17381 839441 48.3 | 1.191 % | c | 365251 | 89293 319683 | 39615 17607 854651 48.5 | 1.191 % | c | 365588 | 89293 319683 | 43577 17944 879981 49.0 | 1.191 % | c | 366097 | 89293 319683 | 47935 18453 907479 49.2 | 1.191 % | c | 366856 | 89293 319683 | 52728 19212 939227 48.9 | 1.191 % | c | 367995 | 89293 319683 | 58001 20351 990808 48.7 | 1.191 % | c | 369705 | 89293 319683 | 63801 22061 1077728 48.9 | 1.191 % | c ============================================================================== c [1mFound solution: 416[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23138 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 371892 | 89299 319710 | 29766 24248 1354947 55.9 | 1.191 % | c | 371992 | 89299 319710 | 32742 24348 1356814 55.7 | 1.213 % | c | 372146 | 89299 319710 | 36016 24502 1373796 56.1 | 1.213 % | c | 372373 | 89299 319710 | 39618 24729 1377921 55.7 | 1.213 % | c | 372710 | 89299 319710 | 43580 25066 1380528 55.1 | 1.213 % | c | 373221 | 89299 319710 | 47938 25577 1432054 56.0 | 1.213 % | c | 373980 | 89299 319710 | 52732 26336 1501098 57.0 | 1.213 % | c | 375119 | 89299 319710 | 58005 27475 1638401 59.6 | 1.213 % | c ============================================================================== c [1mFound solution: 413[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23141 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 375458 | 89303 319730 | 29767 27814 1668063 60.0 | 1.213 % | c | 375561 | 89303 319730 | 32743 27917 1672575 59.9 | 1.228 % | c | 375713 | 89303 319730 | 36018 28069 1677890 59.8 | 1.228 % | c | 375938 | 89303 319730 | 39619 28294 1700111 60.1 | 1.228 % | c | 376275 | 89303 319730 | 43581 28631 1721049 60.1 | 1.228 % | c | 376783 | 89303 319730 | 47940 29139 1748205 60.0 | 1.228 % | c | 377542 | 89303 319730 | 52734 29898 1852194 62.0 | 1.228 % | c | 378681 | 89303 319730 | 58007 31037 1926161 62.1 | 1.228 % | c ============================================================================== c [1mFound solution: 391[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23163 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 379305 | 89309 319753 | 29769 31661 1997107 63.1 | 1.228 % | c | 379405 | 89309 319753 | 32745 15931 987289 62.0 | 1.249 % | c | 379555 | 89309 319753 | 36020 16081 1004207 62.4 | 1.249 % | c | 379780 | 89309 319753 | 39622 16306 1021903 62.7 | 1.249 % | c | 380118 | 89309 319753 | 43584 16644 1068892 64.2 | 1.249 % | c | 380624 | 89309 319753 | 47943 17150 1124282 65.6 | 1.249 % | c | 381384 | 89309 319753 | 52737 17910 1177065 65.7 | 1.249 % | c | 382527 | 89309 319753 | 58011 19053 1260747 66.2 | 1.249 % | c ============================================================================== c [1mFound solution: 383[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23171 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 382559 | 89312 319765 | 29770 19085 1263820 66.2 | 1.249 % | c | 382660 | 89312 319765 | 32747 19186 1279973 66.7 | 1.264 % | c | 382811 | 89312 319765 | 36021 19337 1281662 66.3 | 1.264 % | c | 383036 | 89312 319765 | 39623 19562 1283347 65.6 | 1.264 % | c | 383373 | 89312 319765 | 43586 19899 1286470 64.6 | 1.264 % | c | 383879 | 89303 319734 | 47944 20374 1292598 63.4 | 1.271 % | c | 384638 | 89303 319734 | 52739 21133 1426918 67.5 | 1.271 % | c | 385777 | 89303 319734 | 58013 22272 1442431 64.8 | 1.271 % | c | 387487 | 89303 319734 | 63814 23982 1652277 68.9 | 1.271 % | c | 390053 | 89303 319734 | 70196 26548 1847144 69.6 | 1.271 % | c | 393901 | 89303 319734 | 77215 30396 2175956 71.6 | 1.271 % | c ============================================================================== c [1mFound solution: 379[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23175 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 396154 | 89305 319742 | 29768 32649 2348259 71.9 | 1.271 % | c | 396255 | 89305 319742 | 32744 16426 957663 58.3 | 1.279 % | c | 396406 | 89305 319742 | 36019 16577 968527 58.4 | 1.279 % | c | 396631 | 89305 319742 | 39621 16802 981575 58.4 | 1.279 % | c | 396968 | 89305 319742 | 43583 17139 1003150 58.5 | 1.279 % | c | 397475 | 89305 319742 | 47941 17646 1038658 58.9 | 1.279 % | c ============================================================================== c [1mFound solution: 377[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23177 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 398085 | 89307 319752 | 29769 18256 1129253 61.9 | 1.279 % | c | 398186 | 89307 319752 | 32745 18357 1130922 61.6 | 1.286 % | c | 398339 | 89307 319752 | 36020 18510 1154631 62.4 | 1.286 % | c | 398566 | 89307 319752 | 39622 18737 1170433 62.5 | 1.286 % | c | 398905 | 89307 319752 | 43584 19076 1225864 64.3 | 1.286 % | c | 399412 | 89307 319752 | 47943 19583 1307495 66.8 | 1.286 % | c | 400171 | 89307 319752 | 52737 20342 1394079 68.5 | 1.286 % | c ============================================================================== c [1mFound solution: 375[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23179 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 400829 | 89308 319760 | 29769 21000 1479193 70.4 | 1.286 % | c | 400929 | 89308 319760 | 32745 21100 1491899 70.7 | 1.293 % | c | 401080 | 89308 319760 | 36020 21251 1511648 71.1 | 1.293 % | c | 401305 | 89308 319760 | 39622 21476 1514293 70.5 | 1.293 % | c | 401643 | 89222 319462 | 43584 21776 1525877 70.1 | 1.397 % | c | 402150 | 89222 319462 | 47943 22283 1553678 69.7 | 1.397 % | c | 402913 | 89222 319462 | 52737 23046 1660939 72.1 | 1.397 % | c | 404052 | 89222 319462 | 58011 24185 1951488 80.7 | 1.397 % | c | 405760 | 89222 319462 | 63812 25893 2007780 77.5 | 1.397 % | c | 408322 | 89222 319462 | 70193 28455 2637423 92.7 | 1.397 % | c | 412166 | 89222 319462 | 77213 32299 2783887 86.2 | 1.397 % | c | 417938 | 89222 319462 | 84934 38071 3926319 103.1 | 1.397 % | c ============================================================================== c [1mFound solution: 371[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 23183 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 426578 | 89224 319470 | 29741 46711 6220556 133.2 | 1.397 % | c | 426678 | 89224 319470 | 32715 16779 3072475 183.1 | 1.404 % | c | 426828 | 89224 319470 | 35986 16929 3075611 181.7 | 1.404 % | c | 427055 | 89224 319470 | 39585 17156 3079240 179.5 | 1.404 % | c | 427392 | 89224 319470 | 43543 17493 3088913 176.6 | 1.404 % | c | 427898 | 89224 319470 | 47898 17999 3093916 171.9 | 1.404 % | c | 428657 | 89224 319470 | 52687 18758 3106406 165.6 | 1.404 % | c | 429797 | 89189 319349 | 57956 19885 3128940 157.4 | 1.442 % | c | 431505 | 89189 319349 | 63752 21593 3412504 158.0 | 1.442 % | c | 434069 | 89175 319301 | 70127 24154 3816541 158.0 | 1.464 % | c | 437914 | 89098 319034 | 77140 27975 4441778 158.8 | 1.561 % | c | 443684 | 89040 318834 | 84854 33726 5149734 152.7 | 1.627 % | c | 452334 | 88999 318693 | 93339 42368 6815244 160.9 | 1.672 % | c c *** TERMINATED *** s SATISFIABLE v C2_0x2e__bit0 -C3_0x2e__bit0 -C4_0x2e__bit0 -C5_0x2e__bit0 -C6_0x2e__bit0 -C7_0x2e__bit0 -C8_0x2e__bit0 -C9_0x2e__bit0 -C10_0x2e__bit0 -C11_0x2e__bit0 -C12_0x2e__bit0 -C13_0x2e__bit0 -C14_0x2e__bit0 -C15_0x2e__bit0 -C16_0x2e__bit0 -C17_0x2e__bit0 -C18_0x2e__bit0 -C19_0x2e__bit0 C20_0x2e__bit0 -C21_0x2e__bit0 -C22_0x2e__bit0 -C23_0x2e__bit0 -C24_0x2e__bit0 -C25_0x2e__bit0 -C26_0x2e__bit0 -C27_0x2e__bit0 -C28_0x2e__bit0 -C29_0x2e__bit0 -C30_0x2e__bit0 -C31_0x2e__bit0 -C32_0x2e__bit0 -C33_0x2e__bit0 -C34_0x2e__bit0 C35_0x2e__bit0 -C36_0x2e__bit0 -C37_0x2e__bit0 -C38_0x2e__bit0 -C39_0x2e__bit0 -C40_0x2e__bit0 -C41_0x2e__bit0 -C42_0x2e__bit0 -C43_0x2e__bit0 -C44_0x2e__bit0 -C45_0x2e__bit0 -C46_0x2e__bit0 -C47_0x2e__bit0 -C48_0x2e__bit0 -C49_0x2e__bit0 -C50_0x2e__bit0 -C51_0x2e__bit0 -C52_0x2e__bit0 -C53_0x2e__bit0 -C54_0x2e__bit0 -C55_0x2e__bit0 -C56_0x2e__bit0 -C57_0x2e__bit0 -C58_0x2e__bit0 -C59_0x2e__bit0 -C60_0x2e__bit0 -C61_0x2e__bit0 -C62_0x2e__bit0 -C63_0x2e__bit0 -C64_0x2e__bit0 -C65_0x2e__bit0 -C66_0x2e__bit0 -C67_0x2e__bit0 -C68_0x2e__bit0 -C69_0x2e__bit0 -C70_0x2e__bit0 -C71_0x2e__bit0 -C72_0x2e__bit0 -C73_0x2e__bit0 -C74_0x2e__bit0 -C75_0x2e__bit0 -C76_0x2e__bit0 -C77_0x2e__bit0 -C78_0x2e__bit0 -C79_0x2e__bit0 -C80_0x2e__bit0 -C81_0x2e__bit0 -C82_0x2e__bit0 C83_0x2e__bit0 -C84_0x2e__bit0 -C85_0x2e__bit0 -C86_0x2e__bit0 -C87_0x2e__bit0 -C88_0x2e__bit0 -C89_0x2e__bit0 -C90_0x2e__bit0 -C91_0x2e__bit0 -C92_0x2e__bit0 -C93_0x2e__bit0 -C94_0x2e__bit0 -C95_0x2e__bit0 -C96_0x2e__bit0 -C97_0x2e__bit0 -C98_0x2e__bit0 -C99_0x2e__bit0 -C100_0x2e__bit0 -C101_0x2e__bit0 -C102_0x2e__bit0 -C103_0x2e__bit0 -C104_0x2e__bit0 -C105_0x2e__bit0 -C106_0x2e__bit0 -C107_0x2e__bit0 -C108_0x2e__bit0 -C109_0x2e__bit0 -C110_0x2e__bit0 -C111_0x2e__bit0 -C112_0x2e__bit0 -C113_0x2e__bit0 -C114_0x2e__bit0 -C115_0x2e__bit0 -C116_0x2e__bit0 -C117_0x2e__bit0 C118_0x2e__bit0 -C119_0x2e__bit0 -C120_0x2e__bit0 -C121_0x2e__bit0 -C122_0x2e__bit0 -C123_0x2e__bit0 C124_0x2e__bit0 -C125_0x2e__bit0 -C126_0x2e__bit0 -C127_0x2e__bit0 -C128_0x2e__bit0 -C129_0x2e__bit0 -C130_0x2e__bit0 -C131_0x2e__bit0 -C132_0x2e__bit0 -C133_0x2e__bit0 -C134_0x2e__bit0 -C135_0x2e__bit0 -C136_0x2e__bit0 -C137_0x2e__bit0 -C138_0x2e__bit0 -C139_0x2e__bit0 -C140_0x2e__bit0 -C141_0x2e__bit0 -C142_0x2e__bit0 -C143_0x2e__bit0 -C144_0x2e__bit0 -C145_0x2e__bit0 -C146_0x2e__bit0 -C147_0x2e__bit0 -C148_0x2e__bit0 -C149_0x2e__bit0 -C150_0x2e__bit0 -C151_0x2e__bit0 -C152_0x2e__bit0 -C153_0x2e__bit0 -C154_0x2e__bit0 -C155_0x2e__bit0 -C156_0x2e__bit0 -C157_0x2e__bit0 -C158_0x2e__bit0 -C159_0x2e__bit0 -C160_0x2e__bit0 -C161_0x2e__bit0 -C162_0x2e__bit0 -C163_0x2e__bit0 -C164_0x2e__bit0 -C165_0x2e__bit0 -C166_0x2e__bit0 -C167_0x2e__bit0 -C168_0x2e__bit0 -C169_0x2e__bit0 -C170_0x2e__bit0 -C171_0x2e__bit0 -C172_0x2e__bit0 -C173_0x2e__bit0 -C174_0x2e__bit0 -C175_0x2e__bit0 -C176_0x2e__bit0 -C177_0x2e__bit0 -C178_0x2e__bit0 -C179_0x2e__bit0 -C180_0x2e__bit0 -C181_0x2e__bit0 -C182_0x2e__bit0 -C183_0x2e__bit0 -C184_0x2e__bit0 -C185_0x2e__bit0 -C186_0x2e__bit0 -C187_0x2e__bit0 -C188_0x2e__bit0 -C189_0x2e__bit0 -C190_0x2e__bit0 -C191_0x2e__bit0 -C192_0x2e__bit0 -C193_0x2e__bit0 -C194_0x2e__bit0 -C195_0x2e__bit0 -C196_0x2e__bit0 -C197_0x2e__bit0 -C198_0x2e__bit0 -C199_0x2e__bit0 -C200_0x2e__bit0 -C201_0x2e__bit0 -C202_0x2e__bit0 -C203_0x2e__bit0 -C204_0x2e__bit0 -C205_0x2e__bit0 -C206_0x2e__bit0 -C207_0x2e__bit0 -C208_0x2e__bit0 -C209_0x2e__bit0 -C210_0x2e__bit0 -C211_0x2e__bit0 -C212_0x2e__bit0 -C213_0x2e__bit0 -C214_0x2e__bit0 -C215_0x2e__bit0 -C216_0x2e__bit0 -C217_0x2e__bit0 -C218_0x2e__bit0 -C219_0x2e__bit0 -C220_0x2e__bit0 -C221_0x2e__bit0 -C222_0x2e__bit0 -C223_0x2e__bit0 -C224_0x2e__bit0 -C225_0x2e__bit0 -C226_0x2e__bit0 -C227_0x2e__bit0 -C228_0x2e__bit0 -C229_0x2e__bit0 -C230_0x2e__bit0 -C231_0x2e__bit0 -C232_0x2e__bit0 -C233_0x2e__bit0 -C234_0x2e__bit0 -C235_0x2e__bit0 -C236_0x2e__bit0 -C237_0x2e__bit0 -C238_0x2e__bit0 -C239_0x2e__bit0 -C240_0x2e__bit0 -C241_0x2e__bit0 -C242_0x2e__bit0 -C243_0x2e__bit0 -C244_0x2e__bit0 -C245_0x2e__bit0 -C246_0x2e__bit0 -C2#### 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.84 0.94 0.90 2/55 10424 Raw data (stat): 10424 (runsolver) R 10423 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548921872 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0013 s] Raw data (loadavg): 0.87 0.94 0.90 2/55 10424 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 2393 0 0 0 993 5 0 0 25 0 1 0 548921872 11661312 2364 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2847 2364 603 41 0 2806 0 vsize: 11388 [startup+20.002 s] Raw data (loadavg): 0.89 0.94 0.90 2/55 10424 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 3172 0 0 0 1991 8 0 0 25 0 1 0 548921872 14888960 3143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3635 3143 603 41 0 3594 0 vsize: 14540 [startup+30.0028 s] Raw data (loadavg): 0.90 0.94 0.90 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 3878 0 0 0 2989 10 0 0 25 0 1 0 548921872 17842176 3849 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4356 3849 603 41 0 4315 0 vsize: 17424 [startup+40.0036 s] Raw data (loadavg): 0.92 0.94 0.90 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 4452 0 0 0 3988 11 0 0 25 0 1 0 548921872 20127744 4423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4914 4423 603 41 0 4873 0 vsize: 19656 [startup+50.0045 s] Raw data (loadavg): 0.93 0.94 0.90 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 5063 0 0 0 4985 14 0 0 25 0 1 0 548921872 22675456 5034 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5536 5034 603 41 0 5495 0 vsize: 22144 [startup+60.0049 s] Raw data (loadavg): 0.94 0.95 0.90 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 5710 0 0 0 5983 16 0 0 25 0 1 0 548921872 25219072 5681 4294967295 134512640 134672761 3221224544 3221223728 134559383 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6157 5681 603 41 0 6116 0 vsize: 24628 [startup+70.0051 s] Raw data (loadavg): 0.95 0.95 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6311 0 0 0 6981 18 0 0 25 0 1 0 548921872 27774976 6282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6781 6282 603 41 0 6740 0 vsize: 27124 [startup+80.0059 s] Raw data (loadavg): 0.96 0.95 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6338 0 0 0 7980 19 0 0 25 0 1 0 548921872 27930624 6309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6819 6309 603 41 0 6778 0 vsize: 27276 [startup+90.0063 s] Raw data (loadavg): 0.96 0.95 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6338 0 0 0 8980 20 0 0 25 0 1 0 548921872 27930624 6309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6819 6309 603 41 0 6778 0 vsize: 27276 [startup+100.007 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 9980 20 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6819 6310 603 41 0 6778 0 vsize: 27276 [startup+110.007 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 10979 20 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6819 6310 603 41 0 6778 0 vsize: 27276 [startup+120.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 11979 21 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223760 134557633 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6819 6310 603 41 0 6778 0 vsize: 27276 [startup+130.009 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 12979 21 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6819 6310 603 41 0 6778 0 vsize: 27276 [startup+140.009 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6339 0 0 0 13979 22 0 0 25 0 1 0 548921872 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6819 6310 603 41 0 6778 0 vsize: 27276 [startup+150.01 s] Raw data (loadavg): 0.98 0.95 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6341 0 0 0 14979 22 0 0 25 0 1 0 548921872 27930624 6312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6819 6312 603 41 0 6778 0 vsize: 27276 [startup+160.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 6757 0 0 0 15977 23 0 0 25 0 1 0 548921872 29528064 6728 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7209 6728 603 41 0 7168 0 vsize: 28836 [startup+170.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 7073 0 0 0 16976 25 0 0 25 0 1 0 548921872 30851072 7044 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7532 7044 603 41 0 7491 0 vsize: 30128 [startup+180.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 7443 0 0 0 17974 27 0 0 25 0 1 0 548921872 32583680 7414 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7955 7414 603 41 0 7914 0 vsize: 31820 [startup+190.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 7846 0 0 0 18973 28 0 0 25 0 1 0 548921872 34185216 7817 4294967295 134512640 134672761 3221224544 3221223792 134562614 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8346 7817 603 41 0 8305 0 vsize: 33384 [startup+200.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8216 0 0 0 19972 29 0 0 25 0 1 0 548921872 35778560 8187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8735 8187 603 41 0 8694 0 vsize: 34940 [startup+210.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8589 0 0 0 20971 30 0 0 25 0 1 0 548921872 37249024 8560 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9094 8560 603 41 0 9053 0 vsize: 36376 [startup+220.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 21970 31 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8902 603 41 0 9381 0 vsize: 37688 [startup+230.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 22970 32 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8902 603 41 0 9381 0 vsize: 37688 [startup+240.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 23969 32 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8902 603 41 0 9381 0 vsize: 37688 [startup+250.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 24969 32 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8902 603 41 0 9381 0 vsize: 37688 [startup+260.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8931 0 0 0 25969 33 0 0 25 0 1 0 548921872 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8902 603 41 0 9381 0 vsize: 37688 [startup+270.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 26969 33 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223728 134559379 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8903 603 41 0 9381 0 vsize: 37688 [startup+280.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 27968 34 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8903 603 41 0 9381 0 vsize: 37688 [startup+290.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 28968 34 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8903 603 41 0 9381 0 vsize: 37688 [startup+300.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 29968 35 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8903 603 41 0 9381 0 vsize: 37688 [startup+310.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 30967 35 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8903 603 41 0 9381 0 vsize: 37688 [startup+320.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10426 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 31967 35 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8903 603 41 0 9381 0 vsize: 37688 [startup+330.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8932 0 0 0 32967 36 0 0 25 0 1 0 548921872 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9422 8903 603 41 0 9381 0 vsize: 37688 [startup+340.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 8986 0 0 0 33966 37 0 0 25 0 1 0 548921872 38862848 8957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9488 8957 603 41 0 9447 0 vsize: 37952 [startup+350.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9257 0 0 0 34965 38 0 0 25 0 1 0 548921872 39936000 9228 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9750 9228 603 41 0 9709 0 vsize: 39000 [startup+360.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 35965 39 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+370.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 36964 39 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223696 134564785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+380.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 37964 40 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+390.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 38964 40 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+400.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 39964 40 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+410.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 40953 41 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+420.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 41952 41 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+430.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 42952 42 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+440.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 43951 43 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+450.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 44951 43 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+460.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 45951 43 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+470.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 46950 44 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+480.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9310 0 0 0 47950 44 0 0 25 0 1 0 548921872 40206336 9281 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9281 603 41 0 9775 0 vsize: 39264 [startup+490.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9481 0 0 0 48949 46 0 0 25 0 1 0 548921872 40878080 9452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9980 9452 603 41 0 9939 0 vsize: 39920 [startup+500.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9587 0 0 0 49948 47 0 0 25 0 1 0 548921872 41283584 9558 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9558 603 41 0 10038 0 vsize: 40316 [startup+510.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9587 0 0 0 50947 48 0 0 25 0 1 0 548921872 41283584 9558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9558 603 41 0 10038 0 vsize: 40316 [startup+520.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 51946 48 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9559 603 41 0 10038 0 vsize: 40316 [startup+530.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 52946 49 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9559 603 41 0 10038 0 vsize: 40316 [startup+540.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 53946 49 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9559 603 41 0 10038 0 vsize: 40316 [startup+550.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 54945 50 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9559 603 41 0 10038 0 vsize: 40316 [startup+560.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9588 0 0 0 55945 50 0 0 25 0 1 0 548921872 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9559 603 41 0 10038 0 vsize: 40316 [startup+570.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 56945 50 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+580.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 57944 51 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+590.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 58944 51 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+600.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 59944 52 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+610.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 60943 52 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+620.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10428 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 61943 53 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+630.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 62943 53 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+640.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 63942 54 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+650.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 64942 54 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+660.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 65942 55 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+670.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 66942 55 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+680.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 67941 55 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+690.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 68941 55 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+700.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 69941 56 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+710.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 70941 56 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+720.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 71940 57 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+730.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 72940 57 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+740.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 73940 58 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+750.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9590 0 0 0 74939 58 0 0 25 0 1 0 548921872 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9561 603 41 0 10038 0 vsize: 40316 [startup+760.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 75939 58 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9562 603 41 0 10038 0 vsize: 40316 [startup+770.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 76939 59 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9562 603 41 0 10038 0 vsize: 40316 [startup+780.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 77938 60 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9562 603 41 0 10038 0 vsize: 40316 [startup+790.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 78938 60 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9562 603 41 0 10038 0 vsize: 40316 [startup+800.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9591 0 0 0 79938 60 0 0 25 0 1 0 548921872 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9562 603 41 0 10038 0 vsize: 40316 [startup+810.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 80938 61 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9563 603 41 0 10038 0 vsize: 40316 [startup+820.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 81938 61 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9563 603 41 0 10038 0 vsize: 40316 [startup+830.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 82937 62 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9563 603 41 0 10038 0 vsize: 40316 [startup+840.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 83937 62 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9563 603 41 0 10038 0 vsize: 40316 [startup+850.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 84937 62 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9563 603 41 0 10038 0 vsize: 40316 [startup+860.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 85936 63 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9563 603 41 0 10038 0 vsize: 40316 [startup+870.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 86936 63 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9563 603 41 0 10038 0 vsize: 40316 [startup+880.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 87936 64 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9563 603 41 0 10038 0 vsize: 40316 [startup+890.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9592 0 0 0 88935 64 0 0 25 0 1 0 548921872 41283584 9563 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9563 603 41 0 10038 0 vsize: 40316 [startup+900.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 89935 65 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+910.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 90935 65 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+920.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10430 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 91934 66 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+930.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 92934 66 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+940.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 93934 67 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+950.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 94933 67 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+960.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 95933 68 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+970.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 96932 68 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+980.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 97932 69 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+990.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9593 0 0 0 98931 70 0 0 25 0 1 0 548921872 41283584 9564 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10079 9564 603 41 0 10038 0 vsize: 40316 [startup+1000.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 99930 70 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1010.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 100930 71 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1020.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 101930 71 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1030.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 102930 72 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1040.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 103929 72 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1050.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 104929 73 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1060.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 105929 73 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1070.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 106929 73 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 107929 73 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 108928 74 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 9886 0 0 0 109928 75 0 0 25 0 1 0 548921872 42471424 9857 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10369 9857 603 41 0 10328 0 vsize: 41476 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 10006 0 0 0 110927 75 0 0 25 0 1 0 548921872 43003904 9977 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10499 9977 603 41 0 10458 0 vsize: 41996 [startup+1120.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 10247 0 0 0 111927 76 0 0 25 0 1 0 548921872 44064768 10218 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10758 10218 603 41 0 10717 0 vsize: 43032 [startup+1130.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 10581 0 0 0 112926 77 0 0 25 0 1 0 548921872 45363200 10552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11075 10552 603 41 0 11034 0 vsize: 44300 [startup+1140.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 10834 0 0 0 113925 78 0 0 25 0 1 0 548921872 46424064 10805 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11334 10805 603 41 0 11293 0 vsize: 45336 [startup+1150.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 11204 0 0 0 114923 80 0 0 25 0 1 0 548921872 47882240 11175 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11690 11175 603 41 0 11649 0 vsize: 46760 [startup+1160.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 11585 0 0 0 115922 81 0 0 25 0 1 0 548921872 49451008 11556 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12073 11556 603 41 0 12032 0 vsize: 48292 [startup+1170.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 11929 0 0 0 116921 83 0 0 25 0 1 0 548921872 50913280 11900 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12430 11900 603 41 0 12389 0 vsize: 49720 [startup+1180.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 12189 0 0 0 117920 84 0 0 25 0 1 0 548921872 51978240 12160 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12690 12160 603 41 0 12649 0 vsize: 50760 [startup+1190.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 12465 0 0 0 118919 85 0 0 25 0 1 0 548921872 53166080 12436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12980 12436 603 41 0 12939 0 vsize: 51920 [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10432 Raw data (stat): 10424 (minisat+) R 10423 22929 22928 0 -1 0 12795 0 0 0 119918 86 0 0 25 0 1 0 548921872 54460416 12766 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13296 12766 603 41 0 13255 0 vsize: 53184 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 1/55 10432 Raw data (stat): 10424 (minisat+) Z 10423 22929 22928 0 -1 12 12798 0 0 0 119918 88 0 0 25 0 1 0 548921872 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.09 CPU time (s): 1200.07 CPU user time (s): 1199.18 CPU system time (s): 0.889864 CPU usage (%): 99.9987 Max. virtual memory (Kb): 53184 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####