Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-2.opb |
MD5SUM | 409f1cf0658f035df65cb61f3e4f598e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -28 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 595 |
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 | 595 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 595 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 595 |
Total number of constraints | 27847 |
Number of constraints which are clauses | 27847 |
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 | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc23 THE 2005-04-13 21:29:10 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2876 boxname=wulflinc23 idbench=320 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 409f1cf0658f035df65cb61f3e4f598e /oldhome/oroussel/tmp/wulflinc23/normalized-frb35-17-2.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc23/normalized-frb35-17-2.opb IDLAUNCH: 2876 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 902224 kB Buffers: 34112 kB Cached: 55524 kB SwapCached: 192 kB Active: 47432 kB Inactive: 45212 kB HighTotal: 131008 kB HighFree: 71708 kB LowTotal: 903652 kB LowFree: 830516 kB SwapTotal: 2097136 kB SwapFree: 2096944 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6908 kB Slab: 34352 kB Committed_AS: 63472 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 21:49:12 (client local time) WITH STATUS 10 IN 1200.14 SECONDS stats: 2876 7 1200.14 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 27847 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 | 27847 55694 | 9282 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -24[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:26814 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 56112 122082 | 18704 0 0 nan | 0.000 % | c | 100 | 55441 120669 | 20574 62 485 7.8 | 1.950 % | c | 252 | 54383 118381 | 22631 186 1801 9.7 | 5.130 % | c | 477 | 53349 116119 | 24895 313 3077 9.8 | 8.306 % | c | 814 | 51759 112535 | 27384 516 5065 9.8 | 13.461 % | c | 1321 | 49950 108452 | 30122 920 9543 10.4 | 19.341 % | c ============================================================================== c [1mFound solution: -26[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1658 | 48453 105089 | 16151 1166 13758 11.8 | 19.341 % | c | 1758 | 48207 104544 | 17766 1257 15573 12.4 | 25.098 % | c | 1908 | 47653 103297 | 19542 1386 16993 12.3 | 26.885 % | c | 2133 | 47022 101840 | 21496 1582 20176 12.8 | 29.018 % | c | 2471 | 45334 97977 | 23646 1783 22714 12.7 | 34.745 % | c | 2977 | 43116 92786 | 26011 2128 28051 13.2 | 41.789 % | c ============================================================================== c [1mFound solution: -27[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3108 | 42804 92166 | 14268 2242 29536 13.2 | 41.789 % | c | 3208 | 42633 91773 | 15694 2311 32120 13.9 | 43.581 % | c | 3358 | 42086 90483 | 17264 2410 34663 14.4 | 45.442 % | c | 3583 | 41186 88373 | 18990 2527 36936 14.6 | 48.512 % | c | 3920 | 39875 85257 | 20889 2675 39865 14.9 | 53.073 % | c | 4427 | 38250 81393 | 22978 2937 45919 15.6 | 58.815 % | c | 5186 | 37415 79400 | 25276 3573 58638 16.4 | 61.715 % | c ============================================================================== c [1mFound solution: -28[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5777 | 36536 77244 | 12178 3923 69803 17.8 | 61.715 % | c | 5877 | 36375 76873 | 13395 4009 70834 17.7 | 65.308 % | c | 6027 | 36111 76265 | 14735 4119 72852 17.7 | 66.182 % | c | 6252 | 35833 75598 | 16208 4304 78604 18.3 | 67.328 % | c | 6590 | 35525 74869 | 17829 4581 87877 19.2 | 68.259 % | c | 7096 | 35132 73939 | 19612 5015 102250 20.4 | 69.626 % | c | 7855 | 35004 73641 | 21574 5721 119858 21.0 | 70.063 % | c | 8994 | 34621 72729 | 23731 6710 156327 23.3 | 71.405 % | c | 10702 | 34449 72319 | 26104 8303 266846 32.1 | 72.007 % | c ============================================================================== c [1mFound solution: -29[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10930 | 34398 72230 | 11466 8491 276955 32.6 | 72.007 % | c | 11030 | 34307 72002 | 12612 8543 279040 32.7 | 72.564 % | c | 11180 | 34307 72002 | 13873 8693 286044 32.9 | 72.564 % | c | 11405 | 34227 71812 | 15261 8862 292699 33.0 | 72.846 % | c | 11743 | 33985 71231 | 16787 9032 296460 32.8 | 73.704 % | c | 12250 | 33985 71231 | 18466 9539 330834 34.7 | 73.704 % | c | 13010 | 33963 71183 | 20312 10270 353365 34.4 | 73.770 % | c | 14149 | 33552 70232 | 22343 11249 423515 37.6 | 75.141 % | c | 15857 | 33222 69433 | 24578 12762 568784 44.6 | 76.291 % | c | 18419 | 33120 69188 | 27036 15273 761555 49.9 | 76.651 % | c | 22263 | 32930 68727 | 29739 18985 1120606 59.0 | 77.344 % | c ============================================================================== c [1mFound solution: -30[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26467 | 32657 68028 | 10885 22867 1465252 64.1 | 77.344 % | c | 26567 | 32647 68006 | 11973 22966 1468382 63.9 | 78.332 % | c | 26717 | 32647 68006 | 13170 23116 1476425 63.9 | 78.332 % | c | 26942 | 32647 68006 | 14487 23341 1495373 64.1 | 78.332 % | c | 27279 | 32477 67592 | 15936 23347 1512616 64.8 | 78.938 % | c | 27785 | 32364 67313 | 17530 23764 1543363 64.9 | 79.364 % | c | 28544 | 32254 67045 | 19283 24353 1597203 65.6 | 79.764 % | c | 29683 | 32254 67045 | 21211 25492 1710400 67.1 | 79.764 % | c | 31391 | 32254 67045 | 23332 27200 1919412 70.6 | 79.764 % | c | 33955 | 32254 67045 | 25666 29764 2101826 70.6 | 79.764 % | c ============================================================================== c [1mFound solution: -31[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35137 | 31980 66414 | 10660 30812 2169138 70.4 | 79.764 % | c | 35238 | 31946 66328 | 11726 15491 930133 60.0 | 80.939 % | c | 35389 | 31915 66258 | 12898 15639 935925 59.8 | 81.041 % | c | 35614 | 31915 66258 | 14188 15864 948886 59.8 | 81.041 % | c | 35951 | 31915 66258 | 15607 16201 965361 59.6 | 81.041 % | c | 36458 | 31915 66258 | 17168 16708 996138 59.6 | 81.041 % | c | 37217 | 31915 66258 | 18884 17467 1044393 59.8 | 81.041 % | c | 38357 | 31910 66247 | 20773 18600 1113004 59.8 | 81.056 % | c | 40065 | 31845 66095 | 22850 20288 1216954 60.0 | 81.276 % | c | 42627 | 31804 65994 | 25135 22834 1375865 60.3 | 81.429 % | c | 46471 | 31804 65994 | 27649 26678 1735048 65.0 | 81.429 % | c | 52237 | 31510 65286 | 30414 32374 2209723 68.3 | 82.477 % | c | 60886 | 31481 65217 | 33455 40961 2771939 67.7 | 82.579 % | c | 73860 | 31477 65205 | 36801 19710 946500 48.0 | 82.600 % | c | 93322 | 31477 65205 | 40481 39172 2462580 62.9 | 82.600 % | c ============================================================================== c [1mFound solution: -32[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 98887 | 31443 65100 | 10481 44676 2833202 63.4 | 82.600 % | c | 98987 | 31443 65100 | 11529 17731 914127 51.6 | 82.724 % | c | 99137 | 31443 65100 | 12682 17881 921601 51.5 | 82.724 % | c | 99362 | 31405 65004 | 13950 18104 938348 51.8 | 82.867 % | c | 99699 | 31381 64946 | 15345 18412 962309 52.3 | 82.954 % | c | 100205 | 31381 64946 | 16879 18918 1006461 53.2 | 82.954 % | c | 100964 | 31370 64919 | 18567 19674 1054745 53.6 | 82.995 % | c | 102103 | 31370 64919 | 20424 20813 1143158 54.9 | 82.995 % | c | 103813 | 31365 64908 | 22466 22519 1262523 56.1 | 83.011 % | c | 106376 | 31365 64908 | 24713 25082 1418165 56.5 | 83.011 % | c | 110222 | 31365 64908 | 27185 28928 1703939 58.9 | 83.011 % | c | 115988 | 31330 64825 | 29903 34689 2037716 58.7 | 83.133 % | c | 124637 | 31284 64708 | 32893 43252 2666638 61.7 | 83.307 % | c | 137612 | 31239 64605 | 36183 22486 988221 43.9 | 83.450 % | c | 157073 | 31239 64605 | 39801 41947 2056155 49.0 | 83.450 % | c | 186265 | 31236 64598 | 43781 31773 1941768 61.1 | 83.460 % | c | 230054 | 31231 64587 | 48159 32261 2906002 90.1 | 83.476 % | c ============================================================================== c [1mFound solution: -33[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 278557 | 31244 64621 | 10414 32296 2237077 69.3 | 83.476 % | c | 278658 | 31244 64621 | 11455 16249 954352 58.7 | 83.452 % | c | 278809 | 31244 64621 | 12600 16400 966097 58.9 | 83.452 % | c | 279034 | 31244 64621 | 13861 16625 981948 59.1 | 83.452 % | c | 279372 | 31244 64621 | 15247 16963 1000566 59.0 | 83.452 % | c | 279878 | 31244 64621 | 16771 17469 1034794 59.2 | 83.452 % | c | 280638 | 31244 64621 | 18449 18229 1067205 58.5 | 83.452 % | c | 281777 | 31244 64621 | 20293 19368 1125638 58.1 | 83.452 % | c | 283486 | 31244 64621 | 22323 21077 1208886 57.4 | 83.452 % | c | 286048 | 31244 64621 | 24555 23639 1365631 57.8 | 83.452 % | c | 289893 | 31244 64621 | 27011 27484 1608741 58.5 | 83.452 % | c | 295659 | 31207 64527 | 29712 33206 1964370 59.2 | 83.595 % | c | 304308 | 31207 64527 | 32683 41855 2460979 58.8 | 83.595 % | c | 317282 | 31197 64503 | 35951 22333 712494 31.9 | 83.630 % | c | 336743 | 31197 64503 | 39547 41794 1397205 33.4 | 83.630 % | c | 365935 | 31193 64493 | 43501 34344 952519 27.7 | 83.646 % | c | 409725 | 31143 64373 | 47852 34709 1222470 35.2 | 83.824 % | c | 475409 | 31136 64358 | 52637 54302 1647686 30.3 | 83.845 % | c | 573935 | 31106 64290 | 57900 50437 1608080 31.9 | 83.942 % | #### 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): 1.13 0.96 0.91 2/54 5925 Raw data (stat): 5925 (runsolver) R 5924 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479195323 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0005 s] Raw data (loadavg): 1.11 0.96 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 2304 0 0 0 992 6 0 0 25 0 1 0 479195323 11657216 2275 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2846 2275 603 41 0 2805 0 vsize: 11384 [startup+20.0006 s] Raw data (loadavg): 1.09 0.96 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 2387 0 0 0 1991 7 0 0 25 0 1 0 479195323 12025856 2358 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2936 2358 603 41 0 2895 0 vsize: 11744 [startup+30.0013 s] Raw data (loadavg): 1.08 0.96 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 3018 0 0 0 2988 10 0 0 25 0 1 0 479195323 14565376 2989 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3556 2989 603 41 0 3515 0 vsize: 14224 [startup+40.0013 s] Raw data (loadavg): 1.06 0.96 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 3694 0 0 0 3985 13 0 0 25 0 1 0 479195323 17321984 3665 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4229 3665 603 41 0 4188 0 vsize: 16916 [startup+50.0006 s] Raw data (loadavg): 1.05 0.96 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 4127 0 0 0 4984 15 0 0 25 0 1 0 479195323 19193856 4098 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4686 4098 603 41 0 4645 0 vsize: 18744 [startup+60.0003 s] Raw data (loadavg): 1.04 0.96 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 4628 0 0 0 5982 16 0 0 25 0 1 0 479195323 21196800 4599 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5175 4599 603 41 0 5134 0 vsize: 20700 [startup+70.0004 s] Raw data (loadavg): 1.04 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 4701 0 0 0 6982 16 0 0 25 0 1 0 479195323 21463040 4672 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5240 4672 603 41 0 5199 0 vsize: 20960 [startup+80.0006 s] Raw data (loadavg): 1.03 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 4701 0 0 0 7981 17 0 0 25 0 1 0 479195323 21463040 4672 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5240 4672 603 41 0 5199 0 vsize: 20960 [startup+90.0002 s] Raw data (loadavg): 1.03 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 4774 0 0 0 8981 18 0 0 25 0 1 0 479195323 21729280 4745 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5305 4745 603 41 0 5264 0 vsize: 21220 [startup+100 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 5166 0 0 0 9980 19 0 0 25 0 1 0 479195323 23461888 5137 4294967295 134512640 134672761 3221224624 3221223728 134559905 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5728 5137 603 41 0 5687 0 vsize: 22912 [startup+110 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 5524 0 0 0 10978 21 0 0 25 0 1 0 479195323 24920064 5495 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6084 5495 603 41 0 6043 0 vsize: 24336 [startup+120 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 5841 0 0 0 11976 22 0 0 25 0 1 0 479195323 26243072 5812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6407 5812 603 41 0 6366 0 vsize: 25628 [startup+130.001 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6132 0 0 0 12975 24 0 0 25 0 1 0 479195323 27443200 6103 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6700 6103 603 41 0 6659 0 vsize: 26800 [startup+140.001 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6193 0 0 0 13975 24 0 0 25 0 1 0 479195323 27578368 6164 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6733 6164 603 41 0 6692 0 vsize: 26932 [startup+150.001 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6193 0 0 0 14975 25 0 0 25 0 1 0 479195323 27578368 6164 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6733 6164 603 41 0 6692 0 vsize: 26932 [startup+160.001 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6193 0 0 0 15974 25 0 0 25 0 1 0 479195323 27578368 6164 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6733 6164 603 41 0 6692 0 vsize: 26932 [startup+170 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6193 0 0 0 16974 25 0 0 25 0 1 0 479195323 27578368 6164 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6733 6164 603 41 0 6692 0 vsize: 26932 [startup+180.001 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6193 0 0 0 17974 25 0 0 25 0 1 0 479195323 27578368 6164 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6733 6164 603 41 0 6692 0 vsize: 26932 [startup+190.002 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 18974 26 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+200.001 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 19974 26 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+210.001 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 20973 26 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+220.002 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 21973 27 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223808 134559512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+230.002 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 22973 27 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+240.002 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 23973 27 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223728 134560287 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+250.002 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 24972 28 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+260.002 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 25972 28 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+270.002 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 26972 29 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+280.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 27972 29 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+290.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 28971 30 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+300.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 29971 30 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+310.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6213 0 0 0 30971 30 0 0 25 0 1 0 479195323 27738112 6184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6184 603 41 0 6731 0 vsize: 27088 [startup+320.002 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6215 0 0 0 31970 31 0 0 25 0 1 0 479195323 27738112 6186 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6772 6186 603 41 0 6731 0 vsize: 27088 [startup+330.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6242 0 0 0 32970 31 0 0 25 0 1 0 479195323 27869184 6213 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6804 6213 603 41 0 6763 0 vsize: 27216 [startup+340.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6242 0 0 0 33970 31 0 0 25 0 1 0 479195323 27869184 6213 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6804 6213 603 41 0 6763 0 vsize: 27216 [startup+350.002 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6242 0 0 0 34969 32 0 0 25 0 1 0 479195323 27869184 6213 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6804 6213 603 41 0 6763 0 vsize: 27216 [startup+360.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6242 0 0 0 35969 32 0 0 25 0 1 0 479195323 27869184 6213 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6804 6213 603 41 0 6763 0 vsize: 27216 [startup+370.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6247 0 0 0 36969 33 0 0 25 0 1 0 479195323 27869184 6218 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6804 6218 603 41 0 6763 0 vsize: 27216 [startup+380.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6247 0 0 0 37969 33 0 0 25 0 1 0 479195323 27869184 6218 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6804 6218 603 41 0 6763 0 vsize: 27216 [startup+390.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6607 0 0 0 38967 34 0 0 25 0 1 0 479195323 29351936 6578 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7166 6578 603 41 0 7125 0 vsize: 28664 [startup+400.004 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 6975 0 0 0 39966 36 0 0 25 0 1 0 479195323 30961664 6946 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7559 6946 603 41 0 7518 0 vsize: 30236 [startup+410.004 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7432 0 0 0 40964 38 0 0 25 0 1 0 479195323 32833536 7403 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8016 7403 603 41 0 7975 0 vsize: 32064 [startup+420.003 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7854 0 0 0 41961 41 0 0 25 0 1 0 479195323 34422784 7825 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8404 7825 603 41 0 8363 0 vsize: 33616 [startup+430.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7871 0 0 0 42961 41 0 0 25 0 1 0 479195323 34553856 7842 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8436 7842 603 41 0 8395 0 vsize: 33744 [startup+440.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7871 0 0 0 43961 41 0 0 25 0 1 0 479195323 34553856 7842 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8436 7842 603 41 0 8395 0 vsize: 33744 [startup+450.004 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7871 0 0 0 44961 42 0 0 25 0 1 0 479195323 34553856 7842 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8436 7842 603 41 0 8395 0 vsize: 33744 [startup+460.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7871 0 0 0 45961 42 0 0 25 0 1 0 479195323 34553856 7842 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8436 7842 603 41 0 8395 0 vsize: 33744 [startup+470.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7871 0 0 0 46960 42 0 0 25 0 1 0 479195323 34553856 7842 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8436 7842 603 41 0 8395 0 vsize: 33744 [startup+480.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7871 0 0 0 47960 43 0 0 25 0 1 0 479195323 34553856 7842 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8436 7842 603 41 0 8395 0 vsize: 33744 [startup+490.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7871 0 0 0 48960 43 0 0 25 0 1 0 479195323 34553856 7842 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8436 7842 603 41 0 8395 0 vsize: 33744 [startup+500.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 7871 0 0 0 49960 43 0 0 25 0 1 0 479195323 34553856 7842 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8436 7842 603 41 0 8395 0 vsize: 33744 [startup+510.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8035 0 0 0 50959 44 0 0 25 0 1 0 479195323 35213312 8006 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8597 8006 603 41 0 8556 0 vsize: 34388 [startup+520.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8332 0 0 0 51958 45 0 0 25 0 1 0 479195323 36413440 8303 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8890 8303 603 41 0 8849 0 vsize: 35560 [startup+530.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8593 0 0 0 52956 47 0 0 25 0 1 0 479195323 37478400 8564 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9150 8564 603 41 0 9109 0 vsize: 36600 [startup+540.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 53956 48 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+550.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 54956 48 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+560.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 55956 48 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223760 134560637 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+570.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 56955 48 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+580.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 57956 48 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+590.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 58955 49 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+600.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 59955 49 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+610.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 60955 49 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+620.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 61955 49 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+630.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 62955 49 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223808 134559512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+640.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 63955 50 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+650.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 64954 50 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+660.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 65954 51 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+670.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 66954 51 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+680.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 67953 52 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+690.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 68953 52 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+700.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 69953 52 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+710.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 70953 53 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+720.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 71952 53 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+730.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 72953 53 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+740.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 73952 53 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+750.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8754 0 0 0 74952 54 0 0 25 0 1 0 479195323 38408192 8725 4294967295 134512640 134672761 3221224624 3221223760 134560598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8725 603 41 0 9336 0 vsize: 37508 [startup+760.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 75952 54 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+770.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 76952 54 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+780.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 77952 54 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+790.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 78952 54 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+800.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 79952 55 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+810.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 80951 55 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+820.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 81952 55 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+830.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 82951 55 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+840.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 83951 56 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+850.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 84951 56 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+860.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 85951 56 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+870.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 86951 57 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+880.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 87951 57 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+890.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 88950 57 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+900.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 89950 57 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+910.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 90950 58 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+920.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 91950 58 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+930.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 92949 59 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+940.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 93949 59 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+950.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 94949 60 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+960.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 95948 60 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+970.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 96948 60 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+980.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8755 0 0 0 97948 60 0 0 25 0 1 0 479195323 38408192 8726 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8726 603 41 0 9336 0 vsize: 37508 [startup+990.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8757 0 0 0 98948 61 0 0 25 0 1 0 479195323 38408192 8728 4294967295 134512640 134672761 3221224624 3221223796 134559060 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8728 603 41 0 9336 0 vsize: 37508 [startup+1000.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 99948 61 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1010.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 100947 62 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1020.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 101947 62 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1030.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 102947 62 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1040.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 103947 62 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1050.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 104946 63 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1060.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 105946 63 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1070.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 106946 63 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1080.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 107946 64 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1090.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8759 0 0 0 108946 64 0 0 25 0 1 0 479195323 38408192 8730 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8730 603 41 0 9336 0 vsize: 37508 [startup+1100.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 109946 64 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1110.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 110945 65 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1120.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 111945 65 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1130.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 112945 65 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223728 134560335 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1140.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 113945 66 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1150.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 114945 66 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1160.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 115944 66 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1170.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 116944 67 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1180.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 117944 67 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1190.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 118943 67 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 [startup+1200.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 5925 Raw data (stat): 5925 (minisat+) R 5924 3260 3259 0 -1 0 8760 0 0 0 119943 68 0 0 25 0 1 0 479195323 38408192 8731 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9377 8731 603 41 0 9336 0 vsize: 37508 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.04 s] Raw data (loadavg): 1.00 0.97 0.91 1/54 5925 Raw data (stat): 5925 (minisat+) Z 5924 3260 3259 0 -1 12 8763 0 0 0 119944 69 0 0 25 0 1 0 479195323 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.04 CPU time (s): 1200.14 CPU user time (s): 1199.44 CPU system time (s): 0.696894 CPU usage (%): 100.008 Max. virtual memory (Kb): 37508 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####