Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii16d1.opb |
MD5SUM | 38e9597c5e2c643da0b2660ad99fee98 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 984 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2460 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 2460 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 2460 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 2460 |
Total number of constraints | 17131 |
Number of constraints which are clauses | 17131 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 16 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc20 THE 2005-05-25 16:22:50 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21724 boxname=wulflinc20 idbench=142 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 38e9597c5e2c643da0b2660ad99fee98 /oldhome/oroussel/tmp/wulflinc20/normalized-ii16d1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-ii16d1.opb IDLAUNCH: 21724 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 171072 kB Buffers: 38096 kB Cached: 795344 kB SwapCached: 716 kB Active: 79500 kB Inactive: 760732 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 170820 kB SwapTotal: 2097892 kB SwapFree: 2096336 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5072 kB Slab: 17716 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 16:43:20 (client local time) WITH STATUS 152 IN 1229.87 SECONDS stats: 21724 7 1229.87 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 17131 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 17131 50250 | 5710 0 0 nan | 0.000 % | c | 100 | 17131 50250 | 6281 100 6615 66.2 | 0.002 % | c ============================================================================== c [1mFound solution: 1175[0m c ---[ 0]---> Adder-cost: 4908 maxlim: 1285 bits: 12/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 242 | 51424 172708 | 17141 242 11848 49.0 | 0.002 % | c | 342 | 51424 172708 | 18855 342 15768 46.1 | 0.054 % | c | 493 | 51424 172708 | 20740 493 18494 37.5 | 0.054 % | c | 718 | 51424 172708 | 22814 718 23542 32.8 | 0.054 % | c | 1055 | 51424 172708 | 25096 1055 31670 30.0 | 0.054 % | c | 1561 | 51424 172708 | 27605 1561 53412 34.2 | 0.054 % | c ============================================================================== c [1mFound solution: 1167[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1293 bits: 12/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1870 | 51431 172757 | 17143 1870 63548 34.0 | 0.054 % | c | 1972 | 51431 172757 | 18857 1972 66630 33.8 | 0.095 % | c | 2123 | 51431 172757 | 20743 2123 70814 33.4 | 0.095 % | c | 2348 | 51431 172757 | 22817 2348 82107 35.0 | 0.095 % | c | 2685 | 51431 172757 | 25099 2685 101766 37.9 | 0.095 % | c | 3191 | 51431 172757 | 27608 3191 127775 40.0 | 0.095 % | c | 3950 | 51431 172757 | 30369 3950 170948 43.3 | 0.095 % | c | 5091 | 51431 172757 | 33406 5091 231776 45.5 | 0.095 % | c | 6800 | 51431 172757 | 36747 6800 326077 48.0 | 0.095 % | c | 9362 | 51431 172757 | 40422 9362 547540 58.5 | 0.095 % | c | 13207 | 51431 172757 | 44464 13207 846347 64.1 | 0.095 % | c | 18973 | 51431 172757 | 48910 18973 1253179 66.1 | 0.095 % | c | 27623 | 51431 172757 | 53802 27623 2145141 77.7 | 0.095 % | c | 40597 | 51431 172757 | 59182 40597 2840382 70.0 | 0.095 % | c | 60060 | 51431 172757 | 65100 60060 5258041 87.5 | 0.095 % | c | 89253 | 51431 172757 | 71610 40580 4873379 120.1 | 0.095 % | c | 133043 | 51431 172757 | 78771 24222 6689998 276.2 | 0.095 % | c ============================================================================== c [1mFound solution: 1166[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1294 bits: 12/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 136924 | 51436 172782 | 17145 28103 6869545 244.4 | 0.095 % | c | 137024 | 51436 172782 | 18859 14152 2038217 144.0 | 0.108 % | c | 137174 | 51436 172782 | 20745 14302 2044721 143.0 | 0.108 % | c | 137402 | 51436 172782 | 22819 14530 2050938 141.2 | 0.108 % | c | 137739 | 51436 172782 | 25101 14867 2067598 139.1 | 0.108 % | c | 138245 | 51436 172782 | 27612 15373 2097637 136.4 | 0.109 % | c | 139006 | 51436 172782 | 30373 16134 2224149 137.9 | 0.108 % | c | 140146 | 51436 172782 | 33410 17274 2301061 133.2 | 0.108 % | c | 141854 | 51436 172782 | 36751 18982 2423320 127.7 | 0.108 % | c | 144418 | 51436 172782 | 40427 21546 2723725 126.4 | 0.108 % | c | 148263 | 51436 172782 | 44469 25391 3025490 119.2 | 0.108 % | c | 154029 | 51436 172782 | 48916 31157 3530370 113.3 | 0.108 % | c | 162678 | 51436 172782 | 53808 39806 4035469 101.4 | 0.108 % | c | 175653 | 51436 172782 | 59189 52781 7390252 140.0 | 0.108 % | c | 195114 | 51436 172782 | 65108 21984 2647550 120.4 | 0.108 % | c ============================================================================== c [1mFound solution: 1165[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1295 bits: 12/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 196982 | 51437 172791 | 17145 23852 2789586 117.0 | 0.108 % | c | 197082 | 51437 172791 | 18859 12026 626540 52.1 | 0.122 % | c | 197233 | 51437 172791 | 20745 12177 630433 51.8 | 0.122 % | c | 197459 | 51437 172791 | 22819 12403 637135 51.4 | 0.122 % | c | 197796 | 51437 172791 | 25101 12740 643470 50.5 | 0.122 % | c | 198302 | 51437 172791 | 27612 13246 690753 52.1 | 0.122 % | c | 199061 | 51437 172791 | 30373 14005 710408 50.7 | 0.122 % | c | 200200 | 51437 172791 | 33410 15144 868507 57.3 | 0.122 % | c ============================================================================== c [1mFound solution: 1161[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1299 bits: 12/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 200627 | 51442 172818 | 17147 15571 885970 56.9 | 0.122 % | c | 200727 | 51442 172818 | 18861 15671 888824 56.7 | 0.136 % | c | 200877 | 51442 172818 | 20747 15821 894042 56.5 | 0.136 % | c | 201102 | 51442 172818 | 22822 16046 905424 56.4 | 0.136 % | c | 201441 | 51442 172818 | 25104 16385 934774 57.1 | 0.136 % | c | 201948 | 51442 172818 | 27615 16892 963177 57.0 | 0.136 % | c | 202708 | 51442 172818 | 30376 17652 1015231 57.5 | 0.136 % | c | 203850 | 51442 172818 | 33414 18794 1043199 55.5 | 0.136 % | c | 205558 | 51442 172818 | 36756 20502 1144782 55.8 | 0.136 % | c | 208120 | 51442 172818 | 40431 23064 1291347 56.0 | 0.136 % | c | 211965 | 51442 172818 | 44474 26909 1721187 64.0 | 0.136 % | c | 217731 | 51442 172818 | 48922 32675 2036883 62.3 | 0.136 % | c | 226383 | 51442 172818 | 53814 41327 3408377 82.5 | 0.136 % | c | 239357 | 51442 172818 | 59196 54301 5879760 108.3 | 0.136 % | c ============================================================================== c [1mFound solution: 1154[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1306 bits: 12/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 240816 | 51445 172853 | 17148 55760 5940635 106.5 | 0.136 % | c | 240916 | 51445 172853 | 18862 15717 2415460 153.7 | 0.176 % | c | 241066 | 51445 172853 | 20749 15867 2417824 152.4 | 0.176 % | c | 241291 | 51445 172853 | 22823 16092 2425272 150.7 | 0.176 % | c | 241629 | 51445 172853 | 25106 16430 2437532 148.4 | 0.176 % | c | 242135 | 51445 172853 | 27617 16936 2452415 144.8 | 0.176 % | c | 242895 | 51445 172853 | 30378 17696 2534931 143.2 | 0.176 % | c | 244035 | 51445 172853 | 33416 18836 2579846 137.0 | 0.176 % | c | 245743 | 51445 172853 | 36758 20544 2638077 128.4 | 0.176 % | c | 248305 | 51445 172853 | 40434 23106 2833642 122.6 | 0.176 % | c | 252149 | 51445 172853 | 44477 26950 3100703 115.1 | 0.176 % | c | 257916 | 51445 172853 | 48925 32717 3423063 104.6 | 0.176 % | c | 266567 | 51445 172853 | 53817 41368 4516951 109.2 | 0.176 % | c | 279545 | 51445 172853 | 59199 54346 6453268 118.7 | 0.176 % | c | 299007 | 51445 172853 | 65119 29714 2443174 82.2 | 0.176 % | c | 328201 | 51445 172853 | 71631 58908 7738040 131.4 | 0.176 % | c | 371993 | 51445 172853 | 78794 48072 5308433 110.4 | 0.176 % | c | 437681 | 51445 172853 | 86674 46181 10099368 218.7 | 0.176 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 6558 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.88 0.95 0.98 2/54 6554 Raw data (stat): 6554 (runsolver) R 6553 25399 25398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 840286796 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.0011 s] Raw data (loadavg): 0.90 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0014 s] Raw data (loadavg): 0.91 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0015 s] Raw data (loadavg): 0.92 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0022 s] Raw data (loadavg): 0.94 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0026 s] Raw data (loadavg): 0.95 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0037 s] Raw data (loadavg): 0.95 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0044 s] Raw data (loadavg): 0.96 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0047 s] Raw data (loadavg): 0.97 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0061 s] Raw data (loadavg): 0.97 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.007 s] Raw data (loadavg): 0.97 0.95 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.007 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.008 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.008 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.008 s] Raw data (loadavg): 0.99 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.009 s] Raw data (loadavg): 0.99 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.01 s] Raw data (loadavg): 0.99 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.01 s] Raw data (loadavg): 0.99 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.01 s] Raw data (loadavg): 0.99 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.011 s] Raw data (loadavg): 0.99 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.01 s] Raw data (loadavg): 0.99 0.96 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.72 s] Raw data (loadavg): 0.99 0.97 0.98 1/53 6558 Raw data (stat): 6554 (minisat+_script) S 6553 25399 25398 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840286796 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.72 CPU time (s): 1229.87 CPU user time (s): 1229.08 CPU system time (s): 0.793879 CPU usage (%): 100.012 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####