Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0040.opb |
MD5SUM | 1c249519911563f3292efb34f4875b44 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 62027 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 40 |
Biggest coefficient in the objective function | 8161 |
Number of bits for the biggest coefficient in the objective function | 13 |
Sum of the numbers in the objective function | 265332 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 8161 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 265332 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.293954 |
Number of variables | 40 |
Total number of constraints | 63 |
Number of constraints which are clauses | 10 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 3 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 10 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc24 THE 2005-04-21 17:42:29 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17105 boxname=wulflinc24 idbench=1316 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1c249519911563f3292efb34f4875b44 /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-p0040.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-p0040.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-p0040.opb IDLAUNCH: 17105 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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.080 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: 784884 kB Buffers: 29936 kB Cached: 195980 kB SwapCached: 524 kB Active: 82180 kB Inactive: 145676 kB HighTotal: 131008 kB HighFree: 280 kB LowTotal: 903652 kB LowFree: 784604 kB SwapTotal: 2097892 kB SwapFree: 2096476 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5108 kB Slab: 16376 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 18:02:31 (client local time) WITH STATUS 10 IN 1200.16 SECONDS stats: 17105 7 1200.16 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 23 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ########## c -- Clauses(.)/Splits(s): . c ---[ 21]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 19]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 17]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 15]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 13]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 11]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 9]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 7]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 5]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 3]---> Adder-cost: 6 maxlim: 3 bits: 3/2 c ---[ 2]---> Adder-cost: 83 maxlim: 2683 bits: 13/12 c ---[ 1]---> Adder-cost: 83 maxlim: 3214 bits: 13/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1207 4264 | 402 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 67116[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 538 maxlim: 198216 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 89 | 4842 17249 | 1614 86 748 8.7 | 0.000 % | c ============================================================================== c [1mFound solution: 66788[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 198544 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 145 | 4855 17340 | 1618 142 2454 17.3 | 0.000 % | c ============================================================================== c [1mFound solution: 66238[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 199094 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 188 | 4877 17516 | 1625 185 2930 15.8 | 0.000 % | c ============================================================================== c [1mFound solution: 66214[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 199118 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 211 | 4884 17608 | 1628 208 3827 18.4 | 0.000 % | c ============================================================================== c [1mFound solution: 65927[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 199405 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 215 | 4893 17719 | 1631 212 3862 18.2 | 0.000 % | c ============================================================================== c [1mFound solution: 65904[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 199428 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 222 | 4896 17769 | 1632 219 4025 18.4 | 0.000 % | c ============================================================================== c [1mFound solution: 65034[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 200298 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 228 | 4905 17879 | 1635 225 4105 18.2 | 0.000 % | c | 329 | 4905 17879 | 1798 326 8690 26.7 | 12.614 % | c ============================================================================== c [1mFound solution: 65029[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 200303 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 427 | 4898 17873 | 1632 423 11209 26.5 | 12.614 % | c ============================================================================== c [1mFound solution: 65027[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 200305 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 509 | 4891 17870 | 1630 504 14681 29.1 | 12.614 % | c | 609 | 4891 17870 | 1793 604 16280 27.0 | 13.265 % | c | 759 | 4891 17870 | 1972 754 23721 31.5 | 13.265 % | c | 984 | 4883 17848 | 2169 978 31884 32.6 | 13.492 % | c ============================================================================== c [1mFound solution: 64924[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 200408 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1105 | 4891 17933 | 1630 1099 35766 32.5 | 13.492 % | c | 1205 | 4891 17933 | 1793 1199 39475 32.9 | 13.933 % | c | 1357 | 4891 17933 | 1972 1351 44590 33.0 | 13.933 % | c ============================================================================== c [1mFound solution: 64676[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 200656 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1389 | 4901 18017 | 1633 1383 45458 32.9 | 13.933 % | c ============================================================================== c [1mFound solution: 64643[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 200689 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1475 | 4907 18073 | 1635 1469 48572 33.1 | 13.933 % | c | 1575 | 4907 18073 | 1798 1569 51663 32.9 | 14.570 % | c | 1726 | 4907 18073 | 1978 1720 58011 33.7 | 14.570 % | c | 1951 | 4907 18073 | 2176 1945 66146 34.0 | 14.570 % | c | 2290 | 4907 18073 | 2393 2284 77050 33.7 | 14.570 % | c | 2798 | 4907 18073 | 2633 1493 41034 27.5 | 14.570 % | c | 3557 | 4907 18073 | 2896 2252 71450 31.7 | 14.570 % | c | 4697 | 4899 18051 | 3186 1818 51331 28.2 | 14.790 % | c ============================================================================== c [1mFound solution: 64637[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 200695 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4794 | 4900 18068 | 1633 1915 53162 27.8 | 14.790 % | c ============================================================================== c [1mFound solution: 64449[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 200883 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4812 | 4910 18150 | 1636 976 16120 16.5 | 14.790 % | c ============================================================================== c [1mFound solution: 64411[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 200921 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4823 | 4918 18222 | 1639 987 16424 16.6 | 14.790 % | c ============================================================================== c [1mFound solution: 64208[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 201124 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4836 | 4928 18309 | 1642 1000 16806 16.8 | 14.790 % | c | 4936 | 4928 18309 | 1806 1100 21860 19.9 | 15.970 % | c | 5086 | 4928 18309 | 1986 1250 27364 21.9 | 15.970 % | c ============================================================================== c [1mFound solution: 64177[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 201155 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5133 | 4932 18343 | 1644 1297 28945 22.3 | 15.970 % | c | 5235 | 4932 18343 | 1808 1399 33256 23.8 | 16.115 % | c ============================================================================== c [1mFound solution: 64139[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 201193 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5286 | 4938 18396 | 1646 1450 34971 24.1 | 16.115 % | c | 5386 | 4938 18396 | 1810 1550 38563 24.9 | 16.331 % | c | 5536 | 4938 18396 | 1991 1700 42696 25.1 | 16.331 % | c | 5762 | 4938 18396 | 2190 1926 49754 25.8 | 16.331 % | c ============================================================================== c [1mFound solution: 63298[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 202034 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5882 | 4947 18494 | 1649 2046 52303 25.6 | 16.331 % | c | 5982 | 4947 18494 | 1813 1123 17936 16.0 | 16.807 % | c | 6133 | 4947 18494 | 1995 1274 23784 18.7 | 16.807 % | c | 6359 | 4947 18494 | 2194 1500 35233 23.5 | 16.807 % | c | 6699 | 4947 18494 | 2414 1840 48615 26.4 | 16.807 % | c | 7206 | 4947 18494 | 2655 2347 68753 29.3 | 16.807 % | c | 7965 | 4947 18494 | 2921 1655 38010 23.0 | 16.807 % | c | 9106 | 4947 18494 | 3213 2796 78911 28.2 | 16.807 % | c | 10814 | 4947 18494 | 3534 2745 72306 26.3 | 16.807 % | c | 13376 | 4938 18463 | 3888 3407 90662 26.6 | 16.912 % | c ============================================================================== c [1mFound solution: 62134[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 203198 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14568 | 4954 18606 | 1651 2527 62572 24.8 | 16.912 % | c | 14669 | 4954 18606 | 1816 1365 19210 14.1 | 17.562 % | c | 14819 | 4954 18606 | 1997 1515 23473 15.5 | 17.562 % | c | 15046 | 4948 18589 | 2197 1740 27851 16.0 | 17.665 % | c | 15384 | 4948 18589 | 2417 2078 38380 18.5 | 17.665 % | c | 15890 | 4948 18589 | 2658 2584 50822 19.7 | 17.666 % | c | 16649 | 4948 18589 | 2924 1913 30252 15.8 | 17.665 % | c | 17788 | 4948 18589 | 3217 3052 61956 20.3 | 17.665 % | c | 19497 | 4948 18589 | 3539 2997 69927 23.3 | 17.665 % | c | 22061 | 4948 18589 | 3892 3653 79117 21.7 | 17.665 % | c | 25905 | 4948 18589 | 4282 3311 75101 22.7 | 17.665 % | c | 31672 | 4940 18567 | 4710 4526 102609 22.7 | 17.872 % | c | 40321 | 4940 18567 | 5181 3126 78610 25.1 | 17.872 % | c | 53297 | 4940 18567 | 5699 5150 113558 22.1 | 17.872 % | c | 72759 | 4940 18567 | 6269 3555 66878 18.8 | 17.872 % | c | 101952 | 4940 18567 | 6896 3378 59841 17.7 | 17.872 % | c | 145743 | 4940 18567 | 7586 3977 85339 21.5 | 17.872 % | c | 211430 | 4940 18567 | 8344 6647 171582 25.8 | 17.872 % | c ============================================================================== c [1mFound solution: 62027[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 203305 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 285207 | 4948 18636 | 1649 7166 143190 20.0 | 17.872 % | c | 285307 | 4948 18636 | 1813 1892 27203 14.4 | 18.135 % | c | 285459 | 4948 18636 | 1995 2044 33189 16.2 | 18.135 % | c | 285684 | 4948 18636 | 2194 2269 37547 16.5 | 18.135 % | c | 286021 | 4948 18636 | 2414 1375 14176 10.3 | 18.135 % | c | 286528 | 4948 18636 | 2655 1882 27241 14.5 | 18.135 % | c | 287287 | 4948 18636 | 2921 2641 47179 17.9 | 18.135 % | c | 288426 | 4948 18636 | 3213 2194 37225 17.0 | 18.135 % | c | 290135 | 4948 18636 | 3534 2152 34257 15.9 | 18.135 % | c | 292697 | 4948 18636 | 3888 2780 50731 18.2 | 18.135 % | c | 296542 | 4948 18636 | 4277 2439 42495 17.4 | 18.135 % | c | 302309 | 4948 18636 | 4704 3667 73066 19.9 | 18.135 % | c | 310958 | 4948 18636 | 5175 4823 103171 21.4 | 18.135 % | c | 323933 | 4948 18636 | 5692 4072 77038 18.9 | 18.135 % | c | 343396 | 4948 18636 | 6262 5592 113680 20.3 | 18.136 % | c | 372588 | 4948 18636 | 6888 5210 113742 21.8 | 18.135 % | c | 416379 | 4948 18636 | 7577 5838 117842 20.2 | 18.135 % | c | 482063 | 4948 18636 | 8334 4531 78754 17.4 | 18.135 % | c | 580591 | 4948 18636 | 9168 8099 176360 21.8 | 18.135 % | c | 728383 | 4948 18636 | 10085 9034 209434 23.2 | 18.135 % | c | 950066 | 4948 18636 | 11093 7258 148416 20.4 | 18.135 % | c | 1282592 | 4948 18636 | 12203 9111 224890 24.7 | 18.135 % | #### 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/54 13367 Raw data (stat): 13367 (runsolver) R 13366 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546962214 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0001 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 598 0 0 0 996 1 0 0 25 0 1 0 546962214 4022272 576 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 982 576 603 41 0 941 0 vsize: 3928 [startup+20.0012 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 644 0 0 0 1996 2 0 0 25 0 1 0 546962214 4157440 622 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1015 622 603 41 0 974 0 vsize: 4060 [startup+30.0016 s] Raw data (loadavg): 0.90 0.94 0.90 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 701 0 0 0 2995 2 0 0 25 0 1 0 546962214 4423680 679 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1080 679 603 41 0 1039 0 vsize: 4320 [startup+40.002 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 733 0 0 0 3996 2 0 0 25 0 1 0 546962214 4554752 711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1112 711 603 41 0 1071 0 vsize: 4448 [startup+50.002 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 772 0 0 0 4996 2 0 0 25 0 1 0 546962214 4689920 750 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1145 750 603 41 0 1104 0 vsize: 4580 [startup+60.0017 s] Raw data (loadavg): 0.94 0.95 0.90 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 811 0 0 0 5996 2 0 0 25 0 1 0 546962214 4960256 789 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1211 789 603 41 0 1170 0 vsize: 4844 [startup+70.0021 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 831 0 0 0 6996 2 0 0 25 0 1 0 546962214 4960256 809 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1211 809 603 41 0 1170 0 vsize: 4844 [startup+80.0023 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 846 0 0 0 7996 2 0 0 25 0 1 0 546962214 5091328 824 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1243 824 603 41 0 1202 0 vsize: 4972 [startup+90.0029 s] Raw data (loadavg): 1.04 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 876 0 0 0 8996 2 0 0 25 0 1 0 546962214 5226496 854 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1276 854 603 41 0 1235 0 vsize: 5104 [startup+100.002 s] Raw data (loadavg): 1.04 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 899 0 0 0 9996 2 0 0 25 0 1 0 546962214 5226496 877 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1276 877 603 41 0 1235 0 vsize: 5104 [startup+110.002 s] Raw data (loadavg): 1.03 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 900 0 0 0 10996 2 0 0 25 0 1 0 546962214 5226496 878 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1276 878 603 41 0 1235 0 vsize: 5104 [startup+120.003 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 905 0 0 0 11996 2 0 0 25 0 1 0 546962214 5361664 883 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1309 883 603 41 0 1268 0 vsize: 5236 [startup+130.002 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 915 0 0 0 12996 2 0 0 25 0 1 0 546962214 5361664 893 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1309 893 603 41 0 1268 0 vsize: 5236 [startup+140.004 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 939 0 0 0 13996 2 0 0 25 0 1 0 546962214 5492736 917 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1341 917 603 41 0 1300 0 vsize: 5364 [startup+150.004 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 941 0 0 0 14996 3 0 0 25 0 1 0 546962214 5492736 919 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1341 919 603 41 0 1300 0 vsize: 5364 [startup+160.003 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 949 0 0 0 15996 3 0 0 25 0 1 0 546962214 5492736 927 4294967295 134512640 134672761 3221224544 3221223648 134554629 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1341 927 603 41 0 1300 0 vsize: 5364 [startup+170.003 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 955 0 0 0 16997 3 0 0 25 0 1 0 546962214 5492736 933 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1341 933 603 41 0 1300 0 vsize: 5364 [startup+180.003 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 959 0 0 0 17996 3 0 0 25 0 1 0 546962214 5636096 937 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 937 603 41 0 1335 0 vsize: 5504 [startup+190.003 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 959 0 0 0 18996 3 0 0 25 0 1 0 546962214 5636096 937 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 937 603 41 0 1335 0 vsize: 5504 [startup+200.004 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 959 0 0 0 19996 3 0 0 25 0 1 0 546962214 5636096 937 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 937 603 41 0 1335 0 vsize: 5504 [startup+210.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 960 0 0 0 20997 3 0 0 25 0 1 0 546962214 5636096 938 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 938 603 41 0 1335 0 vsize: 5504 [startup+220.004 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 960 0 0 0 21997 3 0 0 25 0 1 0 546962214 5636096 938 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 938 603 41 0 1335 0 vsize: 5504 [startup+230.004 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 960 0 0 0 22997 3 0 0 25 0 1 0 546962214 5636096 938 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 938 603 41 0 1335 0 vsize: 5504 [startup+240.004 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 963 0 0 0 23997 3 0 0 25 0 1 0 546962214 5636096 941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 941 603 41 0 1335 0 vsize: 5504 [startup+250.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 966 0 0 0 24997 3 0 0 25 0 1 0 546962214 5636096 944 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1376 944 603 41 0 1335 0 vsize: 5504 [startup+260.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 966 0 0 0 25997 3 0 0 25 0 1 0 546962214 5636096 944 4294967295 134512640 134672761 3221224544 3221223716 134559669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 944 603 41 0 1335 0 vsize: 5504 [startup+270.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 974 0 0 0 26997 4 0 0 25 0 1 0 546962214 5636096 952 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 952 603 41 0 1335 0 vsize: 5504 [startup+280.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 974 0 0 0 27997 4 0 0 25 0 1 0 546962214 5636096 952 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 952 603 41 0 1335 0 vsize: 5504 [startup+290.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 975 0 0 0 28997 4 0 0 25 0 1 0 546962214 5636096 953 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1376 953 603 41 0 1335 0 vsize: 5504 [startup+300.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1008 0 0 0 29997 4 0 0 25 0 1 0 546962214 5771264 986 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1409 986 603 41 0 1368 0 vsize: 5636 [startup+310.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1011 0 0 0 30997 4 0 0 25 0 1 0 546962214 5771264 989 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1409 989 603 41 0 1368 0 vsize: 5636 [startup+320.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1016 0 0 0 31997 4 0 0 25 0 1 0 546962214 5771264 994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1409 994 603 41 0 1368 0 vsize: 5636 [startup+330.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1026 0 0 0 32997 4 0 0 25 0 1 0 546962214 5914624 1004 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1444 1004 603 41 0 1403 0 vsize: 5776 [startup+340.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1031 0 0 0 33998 4 0 0 25 0 1 0 546962214 5914624 1009 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1444 1009 603 41 0 1403 0 vsize: 5776 [startup+350.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1055 0 0 0 34997 4 0 0 25 0 1 0 546962214 5914624 1033 4294967295 134512640 134672761 3221224544 3221223680 134565058 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1444 1033 603 41 0 1403 0 vsize: 5776 [startup+360.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1057 0 0 0 35998 4 0 0 25 0 1 0 546962214 5914624 1035 4294967295 134512640 134672761 3221224544 3221223680 134560720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1444 1035 603 41 0 1403 0 vsize: 5776 [startup+370.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1062 0 0 0 36997 5 0 0 25 0 1 0 546962214 6049792 1040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1477 1040 603 41 0 1436 0 vsize: 5908 [startup+380.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1063 0 0 0 37998 5 0 0 25 0 1 0 546962214 6049792 1041 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1477 1041 603 41 0 1436 0 vsize: 5908 [startup+390.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1080 0 0 0 38998 5 0 0 25 0 1 0 546962214 6049792 1058 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1477 1058 603 41 0 1436 0 vsize: 5908 [startup+400.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1083 0 0 0 39998 5 0 0 25 0 1 0 546962214 6049792 1061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1477 1061 603 41 0 1436 0 vsize: 5908 [startup+410.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1083 0 0 0 40998 5 0 0 25 0 1 0 546962214 6049792 1061 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1477 1061 603 41 0 1436 0 vsize: 5908 [startup+420.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1107 0 0 0 41998 5 0 0 25 0 1 0 546962214 6184960 1085 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1510 1085 603 41 0 1469 0 vsize: 6040 [startup+430.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1107 0 0 0 42998 5 0 0 25 0 1 0 546962214 6184960 1085 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1510 1085 603 41 0 1469 0 vsize: 6040 [startup+440.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1124 0 0 0 43998 5 0 0 25 0 1 0 546962214 6184960 1102 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1510 1102 603 41 0 1469 0 vsize: 6040 [startup+450.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1161 0 0 0 44998 5 0 0 25 0 1 0 546962214 6332416 1139 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1546 1139 603 41 0 1505 0 vsize: 6184 [startup+460.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1167 0 0 0 45998 6 0 0 25 0 1 0 546962214 6463488 1145 4294967295 134512640 134672761 3221224544 3221223728 134559272 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1145 603 41 0 1537 0 vsize: 6312 [startup+470.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1167 0 0 0 46998 6 0 0 25 0 1 0 546962214 6463488 1145 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1145 603 41 0 1537 0 vsize: 6312 [startup+480.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1170 0 0 0 47998 6 0 0 25 0 1 0 546962214 6463488 1148 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1148 603 41 0 1537 0 vsize: 6312 [startup+490.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1170 0 0 0 48999 6 0 0 25 0 1 0 546962214 6463488 1148 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1148 603 41 0 1537 0 vsize: 6312 [startup+500.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1170 0 0 0 49999 6 0 0 25 0 1 0 546962214 6463488 1148 4294967295 134512640 134672761 3221224544 3221223744 134557796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1148 603 41 0 1537 0 vsize: 6312 [startup+510.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1170 0 0 0 50999 6 0 0 25 0 1 0 546962214 6463488 1148 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1148 603 41 0 1537 0 vsize: 6312 [startup+520.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1171 0 0 0 51999 6 0 0 25 0 1 0 546962214 6463488 1149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1149 603 41 0 1537 0 vsize: 6312 [startup+530.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1171 0 0 0 52999 6 0 0 25 0 1 0 546962214 6463488 1149 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1149 603 41 0 1537 0 vsize: 6312 [startup+540.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1171 0 0 0 54000 6 0 0 25 0 1 0 546962214 6463488 1149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1149 603 41 0 1537 0 vsize: 6312 [startup+550.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1172 0 0 0 55000 6 0 0 25 0 1 0 546962214 6463488 1150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1150 603 41 0 1537 0 vsize: 6312 [startup+560.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1172 0 0 0 56000 6 0 0 25 0 1 0 546962214 6463488 1150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1150 603 41 0 1537 0 vsize: 6312 [startup+570.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1172 0 0 0 57000 6 0 0 25 0 1 0 546962214 6463488 1150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1150 603 41 0 1537 0 vsize: 6312 [startup+580.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1172 0 0 0 58000 6 0 0 25 0 1 0 546962214 6463488 1150 4294967295 134512640 134672761 3221224544 3221223544 1075350833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1578 1150 603 41 0 1537 0 vsize: 6312 [startup+590.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1194 0 0 0 58999 6 0 0 25 0 1 0 546962214 6463488 1172 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1578 1172 603 41 0 1537 0 vsize: 6312 [startup+600.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1202 0 0 0 59999 6 0 0 25 0 1 0 546962214 6602752 1180 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1612 1180 603 41 0 1571 0 vsize: 6448 [startup+610.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1202 0 0 0 60999 6 0 0 25 0 1 0 546962214 6602752 1180 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1612 1180 603 41 0 1571 0 vsize: 6448 [startup+620.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1214 0 0 0 62000 6 0 0 25 0 1 0 546962214 6602752 1192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1612 1192 603 41 0 1571 0 vsize: 6448 [startup+630.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1214 0 0 0 63000 6 0 0 25 0 1 0 546962214 6602752 1192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1612 1192 603 41 0 1571 0 vsize: 6448 [startup+640.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1229 0 0 0 64000 6 0 0 25 0 1 0 546962214 6737920 1207 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1645 1207 603 41 0 1604 0 vsize: 6580 [startup+650.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1248 0 0 0 65000 7 0 0 25 0 1 0 546962214 6737920 1226 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1645 1226 603 41 0 1604 0 vsize: 6580 [startup+660.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1253 0 0 0 66000 7 0 0 25 0 1 0 546962214 6737920 1231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1645 1231 603 41 0 1604 0 vsize: 6580 [startup+670.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1253 0 0 0 67000 7 0 0 25 0 1 0 546962214 6737920 1231 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1645 1231 603 41 0 1604 0 vsize: 6580 [startup+680.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1274 0 0 0 68000 7 0 0 25 0 1 0 546962214 6868992 1252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1252 603 41 0 1636 0 vsize: 6708 [startup+690.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1274 0 0 0 69000 7 0 0 25 0 1 0 546962214 6868992 1252 4294967295 134512640 134672761 3221224544 3221223728 134558641 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1252 603 41 0 1636 0 vsize: 6708 [startup+700.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1278 0 0 0 70001 7 0 0 25 0 1 0 546962214 6868992 1256 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1256 603 41 0 1636 0 vsize: 6708 [startup+710.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1278 0 0 0 71001 7 0 0 25 0 1 0 546962214 6868992 1256 4294967295 134512640 134672761 3221224544 3221223756 134516692 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1256 603 41 0 1636 0 vsize: 6708 [startup+720.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1278 0 0 0 72001 7 0 0 25 0 1 0 546962214 6868992 1256 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1256 603 41 0 1636 0 vsize: 6708 [startup+730.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1283 0 0 0 73001 7 0 0 25 0 1 0 546962214 6868992 1261 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1261 603 41 0 1636 0 vsize: 6708 [startup+740.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1284 0 0 0 74001 7 0 0 25 0 1 0 546962214 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1262 603 41 0 1636 0 vsize: 6708 [startup+750.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1284 0 0 0 75001 7 0 0 25 0 1 0 546962214 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1262 603 41 0 1636 0 vsize: 6708 [startup+760.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1284 0 0 0 76002 7 0 0 25 0 1 0 546962214 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1262 603 41 0 1636 0 vsize: 6708 [startup+770.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1284 0 0 0 77002 7 0 0 25 0 1 0 546962214 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1262 603 41 0 1636 0 vsize: 6708 [startup+780.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1284 0 0 0 78002 7 0 0 25 0 1 0 546962214 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1262 603 41 0 1636 0 vsize: 6708 [startup+790.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1284 0 0 0 79002 7 0 0 25 0 1 0 546962214 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1262 603 41 0 1636 0 vsize: 6708 [startup+800.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1284 0 0 0 80002 7 0 0 25 0 1 0 546962214 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1262 603 41 0 1636 0 vsize: 6708 [startup+810.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1284 0 0 0 81002 7 0 0 25 0 1 0 546962214 6868992 1262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1262 603 41 0 1636 0 vsize: 6708 [startup+820.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1286 0 0 0 82003 7 0 0 25 0 1 0 546962214 6868992 1264 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1677 1264 603 41 0 1636 0 vsize: 6708 [startup+830.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1319 0 0 0 83002 7 0 0 25 0 1 0 546962214 7004160 1297 4294967295 134512640 134672761 3221224544 3221223708 134565156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1710 1297 603 41 0 1669 0 vsize: 6840 [startup+840.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1334 0 0 0 84002 7 0 0 25 0 1 0 546962214 7135232 1312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1312 603 41 0 1701 0 vsize: 6968 [startup+850.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1338 0 0 0 85002 7 0 0 25 0 1 0 546962214 7135232 1316 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1316 603 41 0 1701 0 vsize: 6968 [startup+860.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1339 0 0 0 86002 7 0 0 25 0 1 0 546962214 7135232 1317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1317 603 41 0 1701 0 vsize: 6968 [startup+870.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1339 0 0 0 87002 7 0 0 25 0 1 0 546962214 7135232 1317 4294967295 134512640 134672761 3221224544 3221223680 134565080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1317 603 41 0 1701 0 vsize: 6968 [startup+880.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1343 0 0 0 88002 7 0 0 25 0 1 0 546962214 7135232 1321 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1321 603 41 0 1701 0 vsize: 6968 [startup+890.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1343 0 0 0 89002 7 0 0 25 0 1 0 546962214 7135232 1321 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1321 603 41 0 1701 0 vsize: 6968 [startup+900.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1343 0 0 0 90003 7 0 0 25 0 1 0 546962214 7135232 1321 4294967295 134512640 134672761 3221224544 3221223552 1075350790 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1321 603 41 0 1701 0 vsize: 6968 [startup+910.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1358 0 0 0 91003 7 0 0 25 0 1 0 546962214 7135232 1336 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1336 603 41 0 1701 0 vsize: 6968 [startup+920.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1359 0 0 0 92003 7 0 0 25 0 1 0 546962214 7135232 1337 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1337 603 41 0 1701 0 vsize: 6968 [startup+930.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1360 0 0 0 93003 7 0 0 25 0 1 0 546962214 7135232 1338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1338 603 41 0 1701 0 vsize: 6968 [startup+940.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1360 0 0 0 94003 8 0 0 25 0 1 0 546962214 7135232 1338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1338 603 41 0 1701 0 vsize: 6968 [startup+950.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1360 0 0 0 95003 8 0 0 25 0 1 0 546962214 7135232 1338 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1742 1338 603 41 0 1701 0 vsize: 6968 [startup+960.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1365 0 0 0 96003 8 0 0 25 0 1 0 546962214 7299072 1343 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1782 1343 603 41 0 1741 0 vsize: 7128 [startup+970.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1365 0 0 0 97004 8 0 0 25 0 1 0 546962214 7299072 1343 4294967295 134512640 134672761 3221224544 3221223600 134565066 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1782 1343 603 41 0 1741 0 vsize: 7128 [startup+980.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1427 0 0 0 98004 8 0 0 25 0 1 0 546962214 7434240 1405 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1815 1405 603 41 0 1774 0 vsize: 7260 [startup+990.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1432 0 0 0 99004 8 0 0 25 0 1 0 546962214 7569408 1410 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1410 603 41 0 1807 0 vsize: 7392 [startup+1000.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1435 0 0 0 100004 8 0 0 25 0 1 0 546962214 7569408 1413 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1413 603 41 0 1807 0 vsize: 7392 [startup+1010.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1440 0 0 0 101004 8 0 0 25 0 1 0 546962214 7569408 1418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1418 603 41 0 1807 0 vsize: 7392 [startup+1020.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1440 0 0 0 102004 8 0 0 25 0 1 0 546962214 7569408 1418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1418 603 41 0 1807 0 vsize: 7392 [startup+1030.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1440 0 0 0 103004 8 0 0 25 0 1 0 546962214 7569408 1418 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1418 603 41 0 1807 0 vsize: 7392 [startup+1040.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1445 0 0 0 104004 8 0 0 25 0 1 0 546962214 7569408 1423 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1423 603 41 0 1807 0 vsize: 7392 [startup+1050.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 13367 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1445 0 0 0 105005 8 0 0 25 0 1 0 546962214 7569408 1423 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1423 603 41 0 1807 0 vsize: 7392 [startup+1060.01 s] Raw data (loadavg): 1.08 0.99 0.92 2/54 13420 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1446 0 0 0 105998 14 0 0 25 0 1 0 546962214 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1424 603 41 0 1807 0 vsize: 7392 [startup+1070.01 s] Raw data (loadavg): 1.07 0.99 0.92 2/54 13420 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1446 0 0 0 106998 14 0 0 25 0 1 0 546962214 7569408 1424 4294967295 134512640 134672761 3221224544 3221223728 134559592 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1424 603 41 0 1807 0 vsize: 7392 [startup+1080.01 s] Raw data (loadavg): 1.06 0.99 0.92 2/54 13420 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1446 0 0 0 107998 14 0 0 25 0 1 0 546962214 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1424 603 41 0 1807 0 vsize: 7392 [startup+1090.01 s] Raw data (loadavg): 1.05 0.99 0.92 2/54 13420 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1446 0 0 0 108998 14 0 0 25 0 1 0 546962214 7569408 1424 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1424 603 41 0 1807 0 vsize: 7392 [startup+1100.01 s] Raw data (loadavg): 1.04 0.99 0.92 2/54 13420 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1446 0 0 0 109999 14 0 0 25 0 1 0 546962214 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1424 603 41 0 1807 0 vsize: 7392 [startup+1110.02 s] Raw data (loadavg): 1.03 0.99 0.92 2/54 13420 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1446 0 0 0 110999 14 0 0 25 0 1 0 546962214 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1424 603 41 0 1807 0 vsize: 7392 [startup+1120.02 s] Raw data (loadavg): 1.03 0.99 0.92 2/54 13422 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1446 0 0 0 111999 14 0 0 25 0 1 0 546962214 7569408 1424 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1424 603 41 0 1807 0 vsize: 7392 [startup+1130.02 s] Raw data (loadavg): 1.02 0.99 0.92 2/54 13422 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1451 0 0 0 112999 14 0 0 25 0 1 0 546962214 7569408 1429 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1848 1429 603 41 0 1807 0 vsize: 7392 [startup+1140.02 s] Raw data (loadavg): 1.02 0.99 0.92 2/54 13422 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1457 0 0 0 113999 14 0 0 25 0 1 0 546962214 7733248 1435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1888 1435 603 41 0 1847 0 vsize: 7552 [startup+1150.02 s] Raw data (loadavg): 1.02 0.99 0.92 2/54 13422 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1458 0 0 0 115000 14 0 0 25 0 1 0 546962214 7733248 1436 4294967295 134512640 134672761 3221224544 3221223728 134559663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1888 1436 603 41 0 1847 0 vsize: 7552 [startup+1160.02 s] Raw data (loadavg): 1.01 0.99 0.92 2/54 13422 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1458 0 0 0 116000 14 0 0 25 0 1 0 546962214 7733248 1436 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1888 1436 603 41 0 1847 0 vsize: 7552 [startup+1170.02 s] Raw data (loadavg): 1.01 0.99 0.92 2/54 13422 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1458 0 0 0 117000 14 0 0 25 0 1 0 546962214 7733248 1436 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1888 1436 603 41 0 1847 0 vsize: 7552 [startup+1180.02 s] Raw data (loadavg): 1.01 0.99 0.92 2/54 13422 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1458 0 0 0 118000 14 0 0 25 0 1 0 546962214 7733248 1436 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1888 1436 603 41 0 1847 0 vsize: 7552 [startup+1190.02 s] Raw data (loadavg): 1.01 0.99 0.92 2/54 13422 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1458 0 0 0 119000 14 0 0 25 0 1 0 546962214 7733248 1436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1888 1436 603 41 0 1847 0 vsize: 7552 [startup+1200.02 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 13422 Raw data (stat): 13367 (minisat+) R 13366 28546 28545 0 -1 0 1458 0 0 0 120000 14 0 0 25 0 1 0 546962214 7733248 1436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1888 1436 603 41 0 1847 0 vsize: 7552 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.02 s] Raw data (loadavg): 1.00 0.99 0.92 1/54 13422 Raw data (stat): 13367 (minisat+) Z 13366 28546 28545 0 -1 12 1461 0 0 0 120001 14 0 0 25 0 1 0 546962214 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.02 CPU time (s): 1200.16 CPU user time (s): 1200.01 CPU system time (s): 0.146977 CPU usage (%): 100.011 Max. virtual memory (Kb): 7552 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####