Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-sentoy.opb |
MD5SUM | 4df3e7eb358d27d446e34b975724a6c1 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -7772 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 60 |
Biggest coefficient in the objective function | 974 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 9460 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 6000 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 26162 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.01884 |
Number of variables | 60 |
Total number of constraints | 90 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 30 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 60 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc8 THE 2005-04-21 17:13:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17261 boxname=wulflinc8 idbench=1328 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4df3e7eb358d27d446e34b975724a6c1 /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-sentoy.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-sentoy.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-sentoy.opb IDLAUNCH: 17261 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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 : 2 cpu MHz : 451.007 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: 831540 kB Buffers: 8944 kB Cached: 172480 kB SwapCached: 0 kB Active: 30044 kB Inactive: 154308 kB HighTotal: 131008 kB HighFree: 21504 kB LowTotal: 903652 kB LowFree: 810036 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6952 kB Slab: 13124 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 17:33:03 (client local time) WITH STATUS 10 IN 1200.31 SECONDS stats: 17261 7 1200.31 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 30 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 29]---> Adder-cost: 448 maxlim: 11620 bits: 15/14 c ---[ 28]---> Adder-cost: 408 maxlim: 6087 bits: 14/13 c ---[ 27]---> Adder-cost: 432 maxlim: 9310 bits: 14/14 c ---[ 26]---> Adder-cost: 468 maxlim: 11096 bits: 15/14 c ---[ 25]---> Adder-cost: 444 maxlim: 10275 bits: 14/14 c ---[ 24]---> Adder-cost: 458 maxlim: 10302 bits: 14/14 c ---[ 23]---> Adder-cost: 436 maxlim: 13436 bits: 15/14 c ---[ 22]---> Adder-cost: 428 maxlim: 9755 bits: 14/14 c ---[ 21]---> Adder-cost: 412 maxlim: 6448 bits: 14/13 c ---[ 20]---> Adder-cost: 464 maxlim: 10002 bits: 14/14 c ---[ 19]---> Adder-cost: 426 maxlim: 9583 bits: 14/14 c ---[ 18]---> Adder-cost: 424 maxlim: 9848 bits: 14/14 c ---[ 17]---> Adder-cost: 364 maxlim: 5722 bits: 14/13 c ---[ 16]---> Adder-cost: 452 maxlim: 10594 bits: 15/14 c ---[ 15]---> Adder-cost: 434 maxlim: 10081 bits: 14/14 c ---[ 14]---> Adder-cost: 442 maxlim: 9196 bits: 14/14 c ---[ 13]---> Adder-cost: 456 maxlim: 12391 bits: 15/14 c ---[ 12]---> Adder-cost: 450 maxlim: 14161 bits: 15/14 c ---[ 11]---> Adder-cost: 418 maxlim: 12220 bits: 15/14 c ---[ 10]---> Adder-cost: 420 maxlim: 12782 bits: 15/14 c ---[ 9]---> Adder-cost: 460 maxlim: 11486 bits: 15/14 c ---[ 8]---> Adder-cost: 436 maxlim: 8903 bits: 14/14 c ---[ 7]---> Adder-cost: 456 maxlim: 10103 bits: 14/14 c ---[ 6]---> Adder-cost: 380 maxlim: 6238 bits: 14/13 c ---[ 5]---> Adder-cost: 430 maxlim: 10469 bits: 15/14 c ---[ 4]---> Adder-cost: 438 maxlim: 9149 bits: 14/14 c ---[ 3]---> Adder-cost: 420 maxlim: 13773 bits: 15/14 c ---[ 2]---> Adder-cost: 448 maxlim: 9436 bits: 14/14 c ---[ 1]---> Adder-cost: 456 maxlim: 8907 bits: 14/14 c ---[ 0]---> Adder-cost: 408 maxlim: 13608 bits: 15/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 89253 318894 | 29751 0 0 nan | 0.000 % | c | 100 | 89253 318894 | 32726 100 1024 10.2 | 1.712 % | c ============================================================================== c [1mFound solution: -1341[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 391 maxlim: 1341 bits: 12/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 191 | 91914 328410 | 30638 191 1682 8.8 | 1.712 % | c | 291 | 91914 328410 | 33701 291 5081 17.5 | 1.713 % | c | 442 | 91914 328410 | 37071 442 6547 14.8 | 1.713 % | c | 667 | 91914 328410 | 40779 667 9757 14.6 | 1.713 % | c | 1005 | 91914 328410 | 44857 1005 25715 25.6 | 1.713 % | c | 1512 | 91914 328410 | 49342 1512 35570 23.5 | 1.713 % | c ============================================================================== c [1mFound solution: -2964[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 5 maxlim: 2964 bits: 13/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1687 | 91959 328591 | 30653 1687 40255 23.9 | 1.713 % | c | 1789 | 91959 328591 | 33718 1789 41500 23.2 | 1.763 % | c | 1939 | 91959 328591 | 37090 1939 49114 25.3 | 1.763 % | c | 2164 | 91959 328591 | 40799 2164 53289 24.6 | 1.763 % | c | 2502 | 91959 328591 | 44879 2502 65456 26.2 | 1.763 % | c | 3008 | 91953 328574 | 49366 3007 82188 27.3 | 1.770 % | c | 3767 | 91953 328574 | 54303 3766 119856 31.8 | 1.770 % | c | 4906 | 91953 328574 | 59734 4905 138064 28.1 | 1.770 % | c | 6614 | 91953 328574 | 65707 6613 213845 32.3 | 1.770 % | c | 9177 | 91953 328574 | 72278 9176 324329 35.3 | 1.770 % | c | 13023 | 91947 328557 | 79505 13021 494473 38.0 | 1.778 % | c | 18790 | 91947 328557 | 87456 18788 814579 43.4 | 1.778 % | c ============================================================================== c [1mFound solution: -4257[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 2 maxlim: 4257 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23549 | 91961 328620 | 30653 23547 1019723 43.3 | 1.778 % | c | 23649 | 91961 328620 | 33718 23647 1020545 43.2 | 1.806 % | c | 23799 | 91961 328620 | 37090 23797 1025206 43.1 | 1.806 % | c | 24024 | 91961 328620 | 40799 24022 1029449 42.9 | 1.806 % | c | 24362 | 91961 328620 | 44879 24360 1043679 42.8 | 1.806 % | c | 24868 | 91961 328620 | 49366 24866 1055658 42.5 | 1.806 % | c | 25630 | 91961 328620 | 54303 25628 1083665 42.3 | 1.806 % | c | 26770 | 91961 328620 | 59734 26768 1139583 42.6 | 1.806 % | c | 28479 | 91961 328620 | 65707 28477 1195792 42.0 | 1.806 % | c | 31041 | 91961 328620 | 72278 31039 1340127 43.2 | 1.806 % | c | 34887 | 91961 328620 | 79505 34885 1524955 43.7 | 1.806 % | c | 40654 | 91955 328603 | 87456 40651 1777207 43.7 | 1.813 % | c | 49304 | 91955 328603 | 96202 49301 2369545 48.1 | 1.813 % | c | 62280 | 91955 328603 | 105822 62277 3051067 49.0 | 1.813 % | c | 81741 | 91955 328603 | 116404 81738 3924591 48.0 | 1.813 % | c ============================================================================== c [1mFound solution: -4363[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 4363 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86781 | 91958 328635 | 30652 86778 4107084 47.3 | 1.813 % | c | 86881 | 91958 328635 | 33717 15694 503426 32.1 | 1.835 % | c | 87033 | 91958 328635 | 37088 15846 505886 31.9 | 1.835 % | c | 87258 | 91958 328635 | 40797 16071 508525 31.6 | 1.835 % | c | 87596 | 91958 328635 | 44877 16409 523526 31.9 | 1.835 % | c | 88103 | 91958 328635 | 49365 16916 534759 31.6 | 1.835 % | c | 88863 | 91958 328635 | 54301 17676 561876 31.8 | 1.835 % | c | 90003 | 91958 328635 | 59732 18816 603645 32.1 | 1.835 % | c | 91711 | 91958 328635 | 65705 20524 670414 32.7 | 1.835 % | c | 94273 | 91958 328635 | 72275 23086 791440 34.3 | 1.835 % | c | 98118 | 91958 328635 | 79503 26931 955009 35.5 | 1.835 % | c | 103884 | 91958 328635 | 87453 32697 1219534 37.3 | 1.835 % | c | 112534 | 91952 328618 | 96199 41346 1687230 40.8 | 1.842 % | c | 125508 | 91952 328618 | 105819 54320 2269064 41.8 | 1.842 % | c | 144969 | 91952 328618 | 116400 73781 3488461 47.3 | 1.842 % | c | 174161 | 91952 328618 | 128041 102973 5276301 51.2 | 1.842 % | c | 217950 | 91946 328601 | 140845 33573 1485357 44.2 | 1.850 % | c ============================================================================== c [1mFound solution: -4408[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 4408 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 219901 | 91953 328655 | 30651 35524 1564118 44.0 | 1.850 % | c | 220004 | 91953 328655 | 33716 12785 498331 39.0 | 1.878 % | c | 220154 | 91953 328655 | 37087 12935 501650 38.8 | 1.878 % | c | 220379 | 91953 328655 | 40796 13160 506260 38.5 | 1.878 % | c | 220716 | 91953 328655 | 44876 13497 515113 38.2 | 1.878 % | c | 221224 | 91953 328655 | 49363 14005 526284 37.6 | 1.878 % | c | 221983 | 91953 328655 | 54300 14764 548896 37.2 | 1.878 % | c | 223122 | 91953 328655 | 59730 15903 584935 36.8 | 1.878 % | c | 224832 | 91953 328655 | 65703 17613 641419 36.4 | 1.878 % | #### 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.92 0.97 0.91 2/54 1335 Raw data (stat): 1335 (runsolver) R 1334 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 475002476 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0012 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2053 0 0 0 991 7 0 0 25 0 1 0 475002476 10334208 2022 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2523 2022 603 41 0 2482 0 vsize: 10092 [startup+20.0013 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2183 0 0 0 1990 7 0 0 25 0 1 0 475002476 10895360 2152 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2660 2152 603 41 0 2619 0 vsize: 10640 [startup+30.0014 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2329 0 0 0 2989 8 0 0 25 0 1 0 475002476 11427840 2298 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2790 2298 603 41 0 2749 0 vsize: 11160 [startup+40.0022 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2465 0 0 0 3989 8 0 0 25 0 1 0 475002476 11968512 2434 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2922 2434 603 41 0 2881 0 vsize: 11688 [startup+50.0026 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2597 0 0 0 4989 8 0 0 25 0 1 0 475002476 12505088 2566 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3053 2566 603 41 0 3012 0 vsize: 12212 [startup+60.0037 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2689 0 0 0 5989 9 0 0 25 0 1 0 475002476 12910592 2658 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3152 2658 603 41 0 3111 0 vsize: 12608 [startup+70.0045 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2784 0 0 0 6989 9 0 0 25 0 1 0 475002476 13381632 2753 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3267 2753 603 41 0 3226 0 vsize: 13068 [startup+80.0049 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 2885 0 0 0 7988 10 0 0 25 0 1 0 475002476 13787136 2854 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3366 2854 603 41 0 3325 0 vsize: 13464 [startup+90.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3012 0 0 0 8988 10 0 0 25 0 1 0 475002476 14327808 2981 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3498 2981 603 41 0 3457 0 vsize: 13992 [startup+100.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3146 0 0 0 9988 10 0 0 25 0 1 0 475002476 14864384 3115 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3629 3115 603 41 0 3588 0 vsize: 14516 [startup+110.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3264 0 0 0 10988 11 0 0 25 0 1 0 475002476 15265792 3233 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3727 3233 603 41 0 3686 0 vsize: 14908 [startup+120.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3355 0 0 0 11988 11 0 0 25 0 1 0 475002476 15667200 3324 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3825 3324 603 41 0 3784 0 vsize: 15300 [startup+130.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3498 0 0 0 12987 12 0 0 25 0 1 0 475002476 16203776 3467 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3956 3467 603 41 0 3915 0 vsize: 15824 [startup+140.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3617 0 0 0 13987 12 0 0 25 0 1 0 475002476 16736256 3586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4086 3586 603 41 0 4045 0 vsize: 16344 [startup+150.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3689 0 0 0 14987 12 0 0 25 0 1 0 475002476 17006592 3658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4152 3658 603 41 0 4111 0 vsize: 16608 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3775 0 0 0 15987 12 0 0 25 0 1 0 475002476 17399808 3744 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4248 3744 603 41 0 4207 0 vsize: 16992 [startup+170.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3880 0 0 0 16987 13 0 0 25 0 1 0 475002476 17936384 3849 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4379 3849 603 41 0 4338 0 vsize: 17516 [startup+180.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 3963 0 0 0 17986 13 0 0 25 0 1 0 475002476 18202624 3932 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4444 3932 603 41 0 4403 0 vsize: 17776 [startup+190.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4040 0 0 0 18986 13 0 0 25 0 1 0 475002476 18472960 4009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4510 4009 603 41 0 4469 0 vsize: 18040 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4121 0 0 0 19986 13 0 0 25 0 1 0 475002476 18878464 4090 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4609 4090 603 41 0 4568 0 vsize: 18436 [startup+210.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4219 0 0 0 20986 14 0 0 25 0 1 0 475002476 19283968 4188 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4708 4188 603 41 0 4667 0 vsize: 18832 [startup+220.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4315 0 0 0 21986 14 0 0 25 0 1 0 475002476 19689472 4284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4807 4284 603 41 0 4766 0 vsize: 19228 [startup+230.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4416 0 0 0 22986 15 0 0 25 0 1 0 475002476 20094976 4385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4906 4385 603 41 0 4865 0 vsize: 19624 [startup+240.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4515 0 0 0 23986 15 0 0 25 0 1 0 475002476 20496384 4484 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5004 4484 603 41 0 4963 0 vsize: 20016 [startup+250.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4627 0 0 0 24986 15 0 0 25 0 1 0 475002476 20897792 4596 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5102 4596 603 41 0 5061 0 vsize: 20408 [startup+260.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4740 0 0 0 25986 15 0 0 25 0 1 0 475002476 21299200 4709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5200 4709 603 41 0 5159 0 vsize: 20800 [startup+270.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4866 0 0 0 26985 16 0 0 25 0 1 0 475002476 21835776 4835 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5331 4835 603 41 0 5290 0 vsize: 21324 [startup+280.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 4964 0 0 0 27985 16 0 0 25 0 1 0 475002476 22245376 4933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5431 4933 603 41 0 5390 0 vsize: 21724 [startup+290.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5059 0 0 0 28985 16 0 0 25 0 1 0 475002476 22646784 5028 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5529 5028 603 41 0 5488 0 vsize: 22116 [startup+300.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5166 0 0 0 29985 16 0 0 25 0 1 0 475002476 23048192 5135 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5627 5135 603 41 0 5586 0 vsize: 22508 [startup+310.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5257 0 0 0 30985 16 0 0 25 0 1 0 475002476 23453696 5226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5726 5226 603 41 0 5685 0 vsize: 22904 [startup+320.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5345 0 0 0 31985 17 0 0 25 0 1 0 475002476 23855104 5314 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5824 5314 603 41 0 5783 0 vsize: 23296 [startup+330.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5440 0 0 0 32985 17 0 0 25 0 1 0 475002476 24121344 5409 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5889 5409 603 41 0 5848 0 vsize: 23556 [startup+340.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5533 0 0 0 33985 17 0 0 25 0 1 0 475002476 24522752 5502 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5987 5502 603 41 0 5946 0 vsize: 23948 [startup+350.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5665 0 0 0 34985 18 0 0 25 0 1 0 475002476 25063424 5634 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6119 5634 603 41 0 6078 0 vsize: 24476 [startup+360.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5804 0 0 0 35985 18 0 0 25 0 1 0 475002476 25862144 5773 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6314 5773 603 41 0 6273 0 vsize: 25256 [startup+370.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 5935 0 0 0 36985 18 0 0 25 0 1 0 475002476 26398720 5904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6445 5904 603 41 0 6404 0 vsize: 25780 [startup+380.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6105 0 0 0 37984 19 0 0 25 0 1 0 475002476 27066368 6074 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6608 6074 603 41 0 6567 0 vsize: 26432 [startup+390.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6219 0 0 0 38984 19 0 0 25 0 1 0 475002476 27607040 6188 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6740 6188 603 41 0 6699 0 vsize: 26960 [startup+400.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6354 0 0 0 39984 20 0 0 25 0 1 0 475002476 28139520 6323 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6870 6323 603 41 0 6829 0 vsize: 27480 [startup+410.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6488 0 0 0 40984 20 0 0 25 0 1 0 475002476 28680192 6457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7002 6457 603 41 0 6961 0 vsize: 28008 [startup+420.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6614 0 0 0 41984 20 0 0 25 0 1 0 475002476 29216768 6583 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7133 6583 603 41 0 7092 0 vsize: 28532 [startup+430.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6760 0 0 0 42984 20 0 0 25 0 1 0 475002476 29753344 6729 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7264 6729 603 41 0 7223 0 vsize: 29056 [startup+440.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6896 0 0 0 43984 20 0 0 25 0 1 0 475002476 30289920 6865 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7395 6865 603 41 0 7354 0 vsize: 29580 [startup+450.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 44984 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+460.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 45985 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+470.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 46995 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+480.119 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 47995 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+490.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 48996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+500.121 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 49996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+510.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 50996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+520.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 51996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+530.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 52996 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+540.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 53997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+550.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 54997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+560.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 55997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+570.124 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 56997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+580.124 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 57997 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+590.125 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 58998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+600.125 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 59998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+610.125 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 60998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+620.126 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 61998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+630.126 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 62998 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+640.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 63999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+650.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 64999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+660.127 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 65999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+670.128 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 66999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+680.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 67999 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+690.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 69000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+700.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 70000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+710.129 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 71000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+720.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 72000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+730.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 73000 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+740.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 74001 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+750.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 75001 20 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+760.131 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 76000 21 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+770.132 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 76999 21 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+780.133 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 77999 21 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+790.134 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6926 0 0 0 79000 21 0 0 25 0 1 0 475002476 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7476 6895 603 41 0 7435 0 vsize: 29904 [startup+800.133 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 6972 0 0 0 80000 21 0 0 25 0 1 0 475002476 30756864 6941 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7509 6941 603 41 0 7468 0 vsize: 30036 [startup+810.134 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7084 0 0 0 81000 21 0 0 25 0 1 0 475002476 31293440 7053 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7640 7053 603 41 0 7599 0 vsize: 30560 [startup+820.135 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7216 0 0 0 82000 21 0 0 25 0 1 0 475002476 31834112 7185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7772 7185 603 41 0 7731 0 vsize: 31088 [startup+830.135 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7298 0 0 0 83000 22 0 0 25 0 1 0 475002476 32096256 7267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7836 7267 603 41 0 7795 0 vsize: 31344 [startup+840.135 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7361 0 0 0 84000 22 0 0 25 0 1 0 475002476 32366592 7330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7902 7330 603 41 0 7861 0 vsize: 31608 [startup+850.136 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7431 0 0 0 85000 22 0 0 25 0 1 0 475002476 32636928 7400 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7968 7400 603 41 0 7927 0 vsize: 31872 [startup+860.137 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7517 0 0 0 86000 22 0 0 25 0 1 0 475002476 33034240 7486 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8065 7486 603 41 0 8024 0 vsize: 32260 [startup+870.137 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7602 0 0 0 87000 23 0 0 25 0 1 0 475002476 33435648 7571 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8163 7571 603 41 0 8122 0 vsize: 32652 [startup+880.137 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7685 0 0 0 88000 23 0 0 25 0 1 0 475002476 33705984 7654 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8229 7654 603 41 0 8188 0 vsize: 32916 [startup+890.137 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7759 0 0 0 89000 23 0 0 25 0 1 0 475002476 33968128 7728 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8293 7728 603 41 0 8252 0 vsize: 33172 [startup+900.137 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7858 0 0 0 90000 23 0 0 25 0 1 0 475002476 34369536 7827 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8391 7827 603 41 0 8350 0 vsize: 33564 [startup+910.138 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 7975 0 0 0 91000 23 0 0 25 0 1 0 475002476 34910208 7944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8523 7944 603 41 0 8482 0 vsize: 34092 [startup+920.138 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8076 0 0 0 92000 23 0 0 25 0 1 0 475002476 35311616 8045 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8621 8045 603 41 0 8580 0 vsize: 34484 [startup+930.138 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8160 0 0 0 93000 24 0 0 25 0 1 0 475002476 35581952 8129 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8687 8129 603 41 0 8646 0 vsize: 34748 [startup+940.139 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8249 0 0 0 94000 24 0 0 25 0 1 0 475002476 35979264 8218 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8784 8218 603 41 0 8743 0 vsize: 35136 [startup+950.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8341 0 0 0 95000 24 0 0 25 0 1 0 475002476 36380672 8310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8882 8310 603 41 0 8841 0 vsize: 35528 [startup+960.141 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8435 0 0 0 96000 25 0 0 25 0 1 0 475002476 36777984 8404 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8979 8404 603 41 0 8938 0 vsize: 35916 [startup+970.142 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8588 0 0 0 96999 25 0 0 25 0 1 0 475002476 37318656 8557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9111 8557 603 41 0 9070 0 vsize: 36444 [startup+980.141 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8805 0 0 0 97998 26 0 0 25 0 1 0 475002476 38260736 8774 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9341 8774 603 41 0 9300 0 vsize: 37364 [startup+990.142 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 8933 0 0 0 98997 27 0 0 25 0 1 0 475002476 38801408 8902 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9473 8902 603 41 0 9432 0 vsize: 37892 [startup+1000.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9027 0 0 0 99997 27 0 0 25 0 1 0 475002476 39067648 8996 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9538 8996 603 41 0 9497 0 vsize: 38152 [startup+1010.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9127 0 0 0 100997 27 0 0 25 0 1 0 475002476 39473152 9096 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9637 9096 603 41 0 9596 0 vsize: 38548 [startup+1020.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9204 0 0 0 101997 28 0 0 25 0 1 0 475002476 39874560 9173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9735 9173 603 41 0 9694 0 vsize: 38940 [startup+1030.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9273 0 0 0 102997 28 0 0 25 0 1 0 475002476 40144896 9242 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9801 9242 603 41 0 9760 0 vsize: 39204 [startup+1040.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9353 0 0 0 103997 28 0 0 25 0 1 0 475002476 40415232 9322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9867 9322 603 41 0 9826 0 vsize: 39468 [startup+1050.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9431 0 0 0 104997 29 0 0 25 0 1 0 475002476 40820736 9400 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9966 9400 603 41 0 9925 0 vsize: 39864 [startup+1060.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9520 0 0 0 105997 29 0 0 25 0 1 0 475002476 41091072 9489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10032 9489 603 41 0 9991 0 vsize: 40128 [startup+1070.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9607 0 0 0 106997 29 0 0 25 0 1 0 475002476 41488384 9576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10129 9576 603 41 0 10088 0 vsize: 40516 [startup+1080.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9683 0 0 0 107997 29 0 0 25 0 1 0 475002476 41754624 9652 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10194 9652 603 41 0 10153 0 vsize: 40776 [startup+1090.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9765 0 0 0 108997 30 0 0 25 0 1 0 475002476 42160128 9734 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10293 9734 603 41 0 10252 0 vsize: 41172 [startup+1100.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9853 0 0 0 109996 30 0 0 25 0 1 0 475002476 42422272 9822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10357 9822 603 41 0 10316 0 vsize: 41428 [startup+1110.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 110997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 [startup+1120.14 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 111997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 [startup+1130.15 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 112997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 [startup+1140.15 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 113997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 [startup+1150.15 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 114997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 [startup+1160.15 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 115998 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 [startup+1170.15 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 116998 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223544 1075350251 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 [startup+1180.15 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 117997 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 [startup+1190.15 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 118998 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 [startup+1200.15 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1335 Raw data (stat): 1335 (minisat+) R 1334 26667 26666 0 -1 0 9907 0 0 0 119998 30 0 0 25 0 1 0 475002476 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10421 9876 603 41 0 10380 0 vsize: 41684 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.17 s] Raw data (loadavg): 1.00 0.99 0.91 1/54 1335 Raw data (stat): 1335 (minisat+) Z 1334 26667 26666 0 -1 12 9910 0 0 0 119998 32 0 0 25 0 1 0 475002476 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.17 CPU time (s): 1200.31 CPU user time (s): 1199.98 CPU system time (s): 0.328949 CPU usage (%): 100.012 Max. virtual memory (Kb): 41684 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####