Name | normalized-opb/submitted/een/normalized-p0548.opb |
MD5SUM | 422c0da7d5380a26c4dac413428db5c9 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 14670 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 416 |
Biggest coefficient in the objective function | 11000 |
Number of bits for the biggest coefficient in the objective function | 14 |
Sum of the numbers in the objective function | 96797 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 11000 |
Number of bits of the biggest number in a constraint | 14 |
Biggest sum of numbers in a constraint | 96797 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1230.14 |
Number of variables | 527 |
Total number of constraints | 156 |
Number of constraints which are clauses | 40 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 116 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 134 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc10 THE 2005-04-14 21:37:40 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=5231 boxname=wulflinc10 idbench=403 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 422c0da7d5380a26c4dac413428db5c9 /oldhome/oroussel/tmp/wulflinc10/normalized-p0548.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc10/normalized-p0548.opb IDLAUNCH: 5231 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 2 cpu MHz : 450.999 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: 827428 kB Buffers: 36000 kB Cached: 150972 kB SwapCached: 164 kB Active: 74580 kB Inactive: 115432 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 827176 kB SwapTotal: 2097136 kB SwapFree: 2096972 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6920 kB Slab: 11556 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 21:57:42 (client local time) WITH STATUS 10 IN 1200.19 SECONDS stats: 5231 7 1200.19 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 156 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................ss.ssssss.s.s. c ---[ 125]---> BDD-cost: 3 c ---[ 124]---> BDD-cost: 3 c ---[ 123]---> BDD-cost: 3 c ---[ 122]---> BDD-cost: 3 c ---[ 121]---> BDD-cost: 3 c ---[ 120]---> BDD-cost: 3 c ---[ 119]---> BDD-cost: 3 c ---[ 118]---> BDD-cost: 3 c ---[ 117]---> BDD-cost: 3 c ---[ 116]---> BDD-cost: 3 c ---[ 115]---> BDD-cost: 3 c ---[ 114]---> BDD-cost: 3 c ---[ 113]---> BDD-cost: 3 c ---[ 112]---> BDD-cost: 3 c ---[ 111]---> BDD-cost: 3 c ---[ 110]---> BDD-cost: 3 c ---[ 109]---> BDD-cost: 3 c ---[ 108]---> BDD-cost: 3 c ---[ 107]---> BDD-cost: 3 c ---[ 106]---> BDD-cost: 3 c ---[ 105]---> BDD-cost: 3 c ---[ 104]---> BDD-cost: 3 c ---[ 103]---> BDD-cost: 5 c ---[ 102]---> BDD-cost: 8 c ---[ 101]---> BDD-cost: 6 c ---[ 100]---> BDD-cost: 8 c ---[ 99]---> BDD-cost: 6 c ---[ 98]---> BDD-cost: 7 c ---[ 96]---> BDD-cost: 19 c ---[ 93]---> BDD-cost: 8 c ---[ 92]---> BDD-cost: 15 c ---[ 91]---> BDD-cost: 15 c ---[ 90]---> BDD-cost: 4 c ---[ 89]---> BDD-cost: 24 c ---[ 88]---> BDD-cost: 14 c ---[ 87]---> BDD-cost: 12 c ---[ 86]---> BDD-cost: 28 c ---[ 85]---> BDD-cost: 13 c ---[ 83]---> BDD-cost: 7 c ---[ 82]---> BDD-cost: 14 c ---[ 81]---> BDD-cost: 9 c ---[ 80]---> BDD-cost: 25 c ---[ 76]---> BDD-cost: 32 c ---[ 75]---> BDD-cost: 10 c ---[ 74]---> BDD-cost: 19 c ---[ 72]---> BDD-cost: 24 c ---[ 70]---> BDD-cost: 23 c ---[ 69]---> BDD-cost: 8 c ---[ 68]---> BDD-cost: 27 c ---[ 67]---> BDD-cost: 9 c ---[ 66]---> BDD-cost: 11 c ---[ 65]---> BDD-cost: 56 c ---[ 64]---> BDD-cost: 50 c ---[ 63]---> BDD-cost: 20 c ---[ 61]---> BDD-cost: 33 c ---[ 60]---> BDD-cost: 12 c ---[ 58]---> BDD-cost: 9 c ---[ 57]---> BDD-cost: 34 c ---[ 56]---> BDD-cost: 33 c ---[ 55]---> BDD-cost: 23 c ---[ 54]---> BDD-cost: 75 c ---[ 53]---> BDD-cost: 24 c ---[ 52]---> BDD-cost: 37 c ---[ 51]---> BDD-cost: 37 c ---[ 50]---> BDD-cost: 95 c ---[ 49]---> BDD-cost: 11 c ---[ 48]---> BDD-cost: 107 c ---[ 47]---> BDD-cost: 115 c ---[ 46]---> BDD-cost: 120 c ---[ 45]---> BDD-cost: 104 c ---[ 44]---> BDD-cost: 29 c ---[ 43]---> BDD-cost: 51 c ---[ 42]---> BDD-cost: 35 c ---[ 41]---> BDD-cost: 24 c ---[ 39]---> BDD-cost: 61 c ---[ 38]---> BDD-cost: 109 c ---[ 37]---> BDD-cost: 153 c ---[ 36]---> BDD-cost: 120 c ---[ 35]---> BDD-cost: 13 c ---[ 34]---> BDD-cost: 25 c ---[ 33]---> BDD-cost: 121 c ---[ 32]---> BDD-cost: 32 c ---[ 31]---> BDD-cost: 70 c ---[ 30]---> BDD-cost: 56 c ---[ 29]---> BDD-cost: 78 c ---[ 28]---> BDD-cost: 84 c ---[ 27]---> BDD-cost: 36 c ---[ 26]---> BDD-cost: 91 c ---[ 25]---> BDD-cost: 42 c ---[ 23]---> BDD-cost: 39 c ---[ 22]---> BDD-cost: 128 c ---[ 21]---> BDD-cost: 61 c ---[ 19]---> BDD-cost: 85 c ---[ 18]---> BDD-cost: 55 c ---[ 17]---> BDD-cost: 79 c ---[ 16]---> Sorter-cost: 1212 Base: 2 3 2 3 c ---[ 15]---> BDD-cost: 26 c ---[ 14]---> Adder-cost: 171 maxlim: 103 bits: 8/7 c ---[ 13]---> Adder-cost: 190 maxlim: 736 bits: 10/10 c ---[ 12]---> BDD-cost: 49 c ---[ 11]---> BDD-cost: 49 c ---[ 10]---> Adder-cost: 750 maxlim: 2650 bits: 13/12 c ---[ 9]---> BDD-cost: 2 c ---[ 8]---> BDD-cost: 2 c ---[ 7]---> BDD-cost: 9 c ---[ 6]---> BDD-cost: 2 c ---[ 5]---> BDD-cost: 4 c ---[ 4]---> BDD-cost: 7 c ---[ 3]---> BDD-cost: 5 c ---[ 2]---> BDD-cost: 11 c ---[ 1]---> BDD-cost: 9 c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 19074 57624 | 6358 0 0 nan | 0.000 % | c | 100 | 19074 57624 | 6993 100 383 3.8 | 2.252 % | c | 250 | 19050 57540 | 7693 243 1471 6.1 | 2.288 % | c | 475 | 19050 57540 | 8462 468 4052 8.7 | 2.288 % | c | 812 | 19011 57410 | 9308 799 7772 9.7 | 2.361 % | c | 1321 | 19011 57410 | 10239 1308 21339 16.3 | 2.361 % | c | 2080 | 19011 57410 | 11263 2067 39807 19.3 | 2.361 % | c | 3219 | 19002 57379 | 12389 3203 61387 19.2 | 2.379 % | c | 4929 | 18969 57279 | 13628 4905 111590 22.8 | 2.434 % | c | 7491 | 18952 57224 | 14991 7466 185570 24.9 | 2.470 % | c | 11335 | 18952 57224 | 16491 11310 302929 26.8 | 2.470 % | c | 17101 | 18905 57066 | 18140 8619 230651 26.8 | 2.579 % | c | 25754 | 18905 57066 | 19954 17272 547223 31.7 | 2.579 % | c | 38729 | 18877 56968 | 21949 20002 728606 36.4 | 2.633 % | c | 58190 | 18855 56892 | 24144 17072 501826 29.4 | 2.688 % | c | 87383 | 18855 56892 | 26558 21476 1433413 66.7 | 2.688 % | c ============================================================================== c [1mFound solution: 52559[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 2954 maxlim: 44238 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115060 | 39469 130542 | 13156 21856 1211248 55.4 | 2.688 % | c | 115160 | 39469 130542 | 14471 11028 574450 52.1 | 1.865 % | c | 115310 | 39469 130542 | 15918 11178 576227 51.6 | 1.865 % | c | 115535 | 39469 130542 | 17510 11403 580967 50.9 | 1.865 % | c | 115872 | 39469 130542 | 19261 11740 589305 50.2 | 1.865 % | c | 116378 | 39469 130542 | 21187 12246 599863 49.0 | 1.865 % | c | 117137 | 39469 130542 | 23306 13005 616416 47.4 | 1.865 % | c | 118277 | 39469 130542 | 25637 14145 652577 46.1 | 1.865 % | c | 119985 | 39469 130542 | 28201 15853 698827 44.1 | 1.865 % | c | 122547 | 39469 130542 | 31021 18415 771171 41.9 | 1.865 % | c | 126392 | 39469 130542 | 34123 22260 874497 39.3 | 1.865 % | c | 132160 | 39469 130542 | 37535 28028 1200711 42.8 | 1.865 % | c | 140809 | 39469 130542 | 41289 36677 1563685 42.6 | 1.865 % | c | 153784 | 39469 130542 | 45418 21376 978593 45.8 | 1.865 % | c | 173246 | 39469 130542 | 49959 40838 1783298 43.7 | 1.865 % | c | 202439 | 39469 130542 | 54955 34214 1463768 42.8 | 1.865 % | c | 246229 | 39469 130542 | 60451 37728 1678400 44.5 | 1.865 % | c | 311913 | 39469 130542 | 66496 56527 2405637 42.6 | 1.865 % | c | 410440 | 39469 130542 | 73146 55718 2558579 45.9 | 1.865 % | c | 558229 | 39469 130542 | 80460 33120 1706066 51.5 | 1.865 % | #### 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.85 0.94 0.90 2/54 6191 Raw data (stat): 6191 (runsolver) R 6190 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429674464 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.0004 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 1547 0 0 0 995 3 0 0 25 0 1 0 429674464 8048640 1517 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1965 1517 603 41 0 1924 0 vsize: 7860 [startup+20.0009 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 1832 0 0 0 1994 4 0 0 25 0 1 0 429674464 9121792 1802 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2227 1802 603 41 0 2186 0 vsize: 8908 [startup+30.0001 s] Raw data (loadavg): 0.91 0.94 0.90 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 2007 0 0 0 2993 4 0 0 25 0 1 0 429674464 9932800 1977 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2425 1977 603 41 0 2384 0 vsize: 9700 [startup+39.9997 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 2133 0 0 0 3992 5 0 0 25 0 1 0 429674464 10330112 2103 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2522 2103 603 41 0 2481 0 vsize: 10088 [startup+49.9996 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 2583 0 0 0 4991 7 0 0 25 0 1 0 429674464 12214272 2553 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2982 2553 603 41 0 2941 0 vsize: 11928 [startup+59.9999 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 2677 0 0 0 5991 7 0 0 25 0 1 0 429674464 12619776 2647 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3081 2647 603 41 0 3040 0 vsize: 12324 [startup+70 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 3001 0 0 0 6989 9 0 0 25 0 1 0 429674464 13967360 2971 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3410 2971 603 41 0 3369 0 vsize: 13640 [startup+80.0003 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 3001 0 0 0 7988 9 0 0 25 0 1 0 429674464 13967360 2971 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3410 2971 603 41 0 3369 0 vsize: 13640 [startup+90.0005 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 4338 0 0 0 8985 12 0 0 25 0 1 0 429674464 18755584 4008 4294967295 134512640 134672761 3221224640 3221223824 134559417 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4579 4008 603 41 0 4538 0 vsize: 18316 [startup+100 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 4496 0 0 0 9985 13 0 0 25 0 1 0 429674464 19427328 4166 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4743 4166 603 41 0 4702 0 vsize: 18972 [startup+110.001 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5003 0 0 0 10984 14 0 0 25 0 1 0 429674464 21557248 4673 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5263 4673 603 41 0 5222 0 vsize: 21052 [startup+120.001 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5094 0 0 0 11984 14 0 0 25 0 1 0 429674464 21958656 4764 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5361 4764 603 41 0 5320 0 vsize: 21444 [startup+130.001 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5094 0 0 0 12984 14 0 0 25 0 1 0 429674464 21958656 4764 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5361 4764 603 41 0 5320 0 vsize: 21444 [startup+140.002 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5160 0 0 0 13984 14 0 0 25 0 1 0 429674464 22228992 4830 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5427 4830 603 41 0 5386 0 vsize: 21708 [startup+150.002 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5494 0 0 0 14984 15 0 0 25 0 1 0 429674464 23580672 5164 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5757 5164 603 41 0 5716 0 vsize: 23028 [startup+160.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5624 0 0 0 15984 15 0 0 25 0 1 0 429674464 24125440 5294 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5890 5294 603 41 0 5849 0 vsize: 23560 [startup+170.002 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5624 0 0 0 16984 15 0 0 25 0 1 0 429674464 24125440 5294 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5890 5294 603 41 0 5849 0 vsize: 23560 [startup+180.002 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5652 0 0 0 17984 15 0 0 25 0 1 0 429674464 24289280 5322 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5930 5322 603 41 0 5889 0 vsize: 23720 [startup+190.002 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5652 0 0 0 18984 15 0 0 25 0 1 0 429674464 24289280 5322 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5930 5322 603 41 0 5889 0 vsize: 23720 [startup+200.002 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5652 0 0 0 19984 15 0 0 25 0 1 0 429674464 24289280 5322 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5930 5322 603 41 0 5889 0 vsize: 23720 [startup+210.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5715 0 0 0 20984 15 0 0 25 0 1 0 429674464 24559616 5385 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5996 5385 603 41 0 5955 0 vsize: 23984 [startup+220.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5800 0 0 0 21984 15 0 0 25 0 1 0 429674464 24961024 5470 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6094 5470 603 41 0 6053 0 vsize: 24376 [startup+230.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5811 0 0 0 22984 16 0 0 25 0 1 0 429674464 24961024 5481 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6094 5481 603 41 0 6053 0 vsize: 24376 [startup+240.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5811 0 0 0 23985 16 0 0 25 0 1 0 429674464 24961024 5481 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6094 5481 603 41 0 6053 0 vsize: 24376 [startup+250.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5826 0 0 0 24985 16 0 0 25 0 1 0 429674464 25120768 5496 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6133 5496 603 41 0 6092 0 vsize: 24532 [startup+260.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 5917 0 0 0 25985 16 0 0 25 0 1 0 429674464 25391104 5587 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6199 5587 603 41 0 6158 0 vsize: 24796 [startup+270.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6192 0 0 0 26984 17 0 0 25 0 1 0 429674464 26599424 5862 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6494 5862 603 41 0 6453 0 vsize: 25976 [startup+280.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6363 0 0 0 27984 17 0 0 25 0 1 0 429674464 27287552 6033 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6662 6033 603 41 0 6621 0 vsize: 26648 [startup+290.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6376 0 0 0 28984 17 0 0 25 0 1 0 429674464 27287552 6046 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6662 6046 603 41 0 6621 0 vsize: 26648 [startup+300.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6376 0 0 0 29984 17 0 0 25 0 1 0 429674464 27287552 6046 4294967295 134512640 134672761 3221224640 3221223808 134561003 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6662 6046 603 41 0 6621 0 vsize: 26648 [startup+310.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6377 0 0 0 30984 17 0 0 25 0 1 0 429674464 27287552 6047 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6662 6047 603 41 0 6621 0 vsize: 26648 [startup+320.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6411 0 0 0 31984 17 0 0 25 0 1 0 429674464 27430912 6081 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6697 6081 603 41 0 6656 0 vsize: 26788 [startup+330.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6412 0 0 0 32984 17 0 0 25 0 1 0 429674464 27430912 6082 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6697 6082 603 41 0 6656 0 vsize: 26788 [startup+340.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6429 0 0 0 33985 17 0 0 25 0 1 0 429674464 27578368 6099 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6733 6099 603 41 0 6692 0 vsize: 26932 [startup+350.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6454 0 0 0 34984 18 0 0 25 0 1 0 429674464 27725824 6124 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6769 6124 603 41 0 6728 0 vsize: 27076 [startup+360.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6676 0 0 0 35982 19 0 0 25 0 1 0 429674464 28835840 6346 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7040 6346 603 41 0 6999 0 vsize: 28160 [startup+370.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6694 0 0 0 36982 19 0 0 25 0 1 0 429674464 28971008 6364 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7073 6364 603 41 0 7032 0 vsize: 28292 [startup+380.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6694 0 0 0 37982 19 0 0 25 0 1 0 429674464 28971008 6364 4294967295 134512640 134672761 3221224640 3221223808 134560979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7073 6364 603 41 0 7032 0 vsize: 28292 [startup+390.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6705 0 0 0 38983 19 0 0 25 0 1 0 429674464 28971008 6375 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7073 6375 603 41 0 7032 0 vsize: 28292 [startup+400.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6717 0 0 0 39983 19 0 0 25 0 1 0 429674464 29122560 6387 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7110 6387 603 41 0 7069 0 vsize: 28440 [startup+410.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6719 0 0 0 40983 19 0 0 25 0 1 0 429674464 29122560 6389 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7110 6389 603 41 0 7069 0 vsize: 28440 [startup+420.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6738 0 0 0 41983 19 0 0 25 0 1 0 429674464 29122560 6408 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7110 6408 603 41 0 7069 0 vsize: 28440 [startup+430.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6760 0 0 0 42983 19 0 0 25 0 1 0 429674464 29286400 6430 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7150 6430 603 41 0 7109 0 vsize: 28600 [startup+440.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6859 0 0 0 43983 19 0 0 25 0 1 0 429674464 29691904 6529 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7249 6529 603 41 0 7208 0 vsize: 28996 [startup+450.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6859 0 0 0 44983 19 0 0 25 0 1 0 429674464 29691904 6529 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7249 6529 603 41 0 7208 0 vsize: 28996 [startup+460.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6862 0 0 0 45984 19 0 0 25 0 1 0 429674464 29691904 6532 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7249 6532 603 41 0 7208 0 vsize: 28996 [startup+470.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6870 0 0 0 46984 19 0 0 25 0 1 0 429674464 29691904 6540 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7249 6540 603 41 0 7208 0 vsize: 28996 [startup+480.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6871 0 0 0 47984 19 0 0 25 0 1 0 429674464 29691904 6541 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7249 6541 603 41 0 7208 0 vsize: 28996 [startup+490.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6871 0 0 0 48984 19 0 0 25 0 1 0 429674464 29691904 6541 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7249 6541 603 41 0 7208 0 vsize: 28996 [startup+500.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 6893 0 0 0 49984 19 0 0 25 0 1 0 429674464 29839360 6563 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7285 6563 603 41 0 7244 0 vsize: 29140 [startup+510.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7009 0 0 0 50983 20 0 0 25 0 1 0 429674464 30388224 6679 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7419 6679 603 41 0 7378 0 vsize: 29676 [startup+520.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7270 0 0 0 51982 21 0 0 25 0 1 0 429674464 31461376 6940 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7681 6940 603 41 0 7640 0 vsize: 30724 [startup+530.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7364 0 0 0 52982 22 0 0 25 0 1 0 429674464 31862784 7034 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7779 7034 603 41 0 7738 0 vsize: 31116 [startup+540.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7384 0 0 0 53982 22 0 0 25 0 1 0 429674464 31862784 7054 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7779 7054 603 41 0 7738 0 vsize: 31116 [startup+550.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7408 0 0 0 54982 22 0 0 25 0 1 0 429674464 32026624 7078 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7819 7078 603 41 0 7778 0 vsize: 31276 [startup+560.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7416 0 0 0 55982 22 0 0 25 0 1 0 429674464 32026624 7086 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7819 7086 603 41 0 7778 0 vsize: 31276 [startup+570.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7434 0 0 0 56982 22 0 0 25 0 1 0 429674464 32190464 7104 4294967295 134512640 134672761 3221224640 3221223808 134560976 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7104 603 41 0 7818 0 vsize: 31436 [startup+580.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7434 0 0 0 57982 22 0 0 25 0 1 0 429674464 32190464 7104 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7104 603 41 0 7818 0 vsize: 31436 [startup+590.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7447 0 0 0 58983 22 0 0 25 0 1 0 429674464 32190464 7117 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7117 603 41 0 7818 0 vsize: 31436 [startup+600.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 59983 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7118 603 41 0 7818 0 vsize: 31436 [startup+610.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 60983 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7118 603 41 0 7818 0 vsize: 31436 [startup+620.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 61983 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7118 603 41 0 7818 0 vsize: 31436 [startup+630.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 62984 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7118 603 41 0 7818 0 vsize: 31436 [startup+640.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 63984 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7118 603 41 0 7818 0 vsize: 31436 [startup+650.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7448 0 0 0 64984 22 0 0 25 0 1 0 429674464 32190464 7118 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7118 603 41 0 7818 0 vsize: 31436 [startup+660.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7454 0 0 0 65984 22 0 0 25 0 1 0 429674464 32190464 7124 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7859 7124 603 41 0 7818 0 vsize: 31436 [startup+670.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7464 0 0 0 66984 22 0 0 25 0 1 0 429674464 32354304 7134 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7899 7134 603 41 0 7858 0 vsize: 31596 [startup+680.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7479 0 0 0 67984 22 0 0 25 0 1 0 429674464 32354304 7149 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7899 7149 603 41 0 7858 0 vsize: 31596 [startup+690.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 7748 0 0 0 68984 22 0 0 25 0 1 0 429674464 33415168 7418 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8158 7418 603 41 0 8117 0 vsize: 32632 [startup+700.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8085 0 0 0 69983 23 0 0 25 0 1 0 429674464 34881536 7755 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8516 7755 603 41 0 8475 0 vsize: 34064 [startup+710.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8311 0 0 0 70983 24 0 0 25 0 1 0 429674464 35844096 7981 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8751 7981 603 41 0 8710 0 vsize: 35004 [startup+720.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8505 0 0 0 71982 25 0 0 25 0 1 0 429674464 36638720 8175 4294967295 134512640 134672761 3221224640 3221223744 134559760 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8945 8175 603 41 0 8904 0 vsize: 35780 [startup+730.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8505 0 0 0 72982 25 0 0 25 0 1 0 429674464 36638720 8175 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8945 8175 603 41 0 8904 0 vsize: 35780 [startup+740.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8505 0 0 0 73982 25 0 0 25 0 1 0 429674464 36638720 8175 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8945 8175 603 41 0 8904 0 vsize: 35780 [startup+750.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8523 0 0 0 74981 26 0 0 25 0 1 0 429674464 36638720 8193 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8945 8193 603 41 0 8904 0 vsize: 35780 [startup+760.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8530 0 0 0 75982 26 0 0 25 0 1 0 429674464 36782080 8200 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8980 8200 603 41 0 8939 0 vsize: 35920 [startup+770.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8541 0 0 0 76982 26 0 0 25 0 1 0 429674464 36782080 8211 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8980 8211 603 41 0 8939 0 vsize: 35920 [startup+780.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8558 0 0 0 77982 26 0 0 25 0 1 0 429674464 36782080 8228 4294967295 134512640 134672761 3221224640 3221223824 134559581 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8980 8228 603 41 0 8939 0 vsize: 35920 [startup+790.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8559 0 0 0 78982 26 0 0 25 0 1 0 429674464 36782080 8229 4294967295 134512640 134672761 3221224640 3221223700 1075349617 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8980 8229 603 41 0 8939 0 vsize: 35920 [startup+800.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8580 0 0 0 79982 26 0 0 25 0 1 0 429674464 36925440 8250 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9015 8250 603 41 0 8974 0 vsize: 36060 [startup+810.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8602 0 0 0 80982 26 0 0 25 0 1 0 429674464 37089280 8272 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9055 8272 603 41 0 9014 0 vsize: 36220 [startup+820.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8603 0 0 0 81982 26 0 0 25 0 1 0 429674464 37089280 8273 4294967295 134512640 134672761 3221224640 3221223744 134560070 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9055 8273 603 41 0 9014 0 vsize: 36220 [startup+830.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8614 0 0 0 82982 26 0 0 25 0 1 0 429674464 37089280 8284 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9055 8284 603 41 0 9014 0 vsize: 36220 [startup+840.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8615 0 0 0 83983 26 0 0 25 0 1 0 429674464 37089280 8285 4294967295 134512640 134672761 3221224640 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9055 8285 603 41 0 9014 0 vsize: 36220 [startup+850.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8637 0 0 0 84983 26 0 0 25 0 1 0 429674464 37285888 8307 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8307 603 41 0 9062 0 vsize: 36412 [startup+860.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8653 0 0 0 85983 26 0 0 25 0 1 0 429674464 37285888 8323 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8323 603 41 0 9062 0 vsize: 36412 [startup+870.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8657 0 0 0 86983 26 0 0 25 0 1 0 429674464 37285888 8327 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8327 603 41 0 9062 0 vsize: 36412 [startup+880.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8659 0 0 0 87984 26 0 0 25 0 1 0 429674464 37285888 8329 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8329 603 41 0 9062 0 vsize: 36412 [startup+890.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8661 0 0 0 88984 26 0 0 25 0 1 0 429674464 37285888 8331 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8331 603 41 0 9062 0 vsize: 36412 [startup+900.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8663 0 0 0 89984 26 0 0 25 0 1 0 429674464 37285888 8333 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9103 8333 603 41 0 9062 0 vsize: 36412 [startup+910.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8690 0 0 0 90984 26 0 0 25 0 1 0 429674464 37482496 8360 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9151 8360 603 41 0 9110 0 vsize: 36604 [startup+920.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8709 0 0 0 91984 26 0 0 25 0 1 0 429674464 37679104 8379 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8379 603 41 0 9158 0 vsize: 36796 [startup+930.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8712 0 0 0 92984 26 0 0 25 0 1 0 429674464 37679104 8382 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8382 603 41 0 9158 0 vsize: 36796 [startup+940.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8713 0 0 0 93985 26 0 0 25 0 1 0 429674464 37679104 8383 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8383 603 41 0 9158 0 vsize: 36796 [startup+950.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8718 0 0 0 94985 26 0 0 25 0 1 0 429674464 37679104 8388 4294967295 134512640 134672761 3221224640 3221223808 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8388 603 41 0 9158 0 vsize: 36796 [startup+960.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8727 0 0 0 95985 26 0 0 25 0 1 0 429674464 37679104 8397 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8397 603 41 0 9158 0 vsize: 36796 [startup+970.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 96985 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8399 603 41 0 9158 0 vsize: 36796 [startup+980.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 97985 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223744 134554662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8399 603 41 0 9158 0 vsize: 36796 [startup+990.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 98986 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8399 603 41 0 9158 0 vsize: 36796 [startup+1000.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 99986 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8399 603 41 0 9158 0 vsize: 36796 [startup+1010.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 100986 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8399 603 41 0 9158 0 vsize: 36796 [startup+1020.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8729 0 0 0 101986 26 0 0 25 0 1 0 429674464 37679104 8399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8399 603 41 0 9158 0 vsize: 36796 [startup+1030.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8733 0 0 0 102986 26 0 0 25 0 1 0 429674464 37679104 8403 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8403 603 41 0 9158 0 vsize: 36796 [startup+1040.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8743 0 0 0 103986 26 0 0 25 0 1 0 429674464 37679104 8413 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8413 603 41 0 9158 0 vsize: 36796 [startup+1050.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8743 0 0 0 104987 26 0 0 25 0 1 0 429674464 37679104 8413 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8413 603 41 0 9158 0 vsize: 36796 [startup+1060.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8743 0 0 0 105987 26 0 0 25 0 1 0 429674464 37679104 8413 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8413 603 41 0 9158 0 vsize: 36796 [startup+1070.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8743 0 0 0 106987 26 0 0 25 0 1 0 429674464 37679104 8413 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9199 8413 603 41 0 9158 0 vsize: 36796 [startup+1080.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8767 0 0 0 107987 27 0 0 25 0 1 0 429674464 37875712 8437 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8437 603 41 0 9206 0 vsize: 36988 [startup+1090.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8770 0 0 0 108987 27 0 0 25 0 1 0 429674464 37875712 8440 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8440 603 41 0 9206 0 vsize: 36988 [startup+1100.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8771 0 0 0 109987 27 0 0 25 0 1 0 429674464 37875712 8441 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8441 603 41 0 9206 0 vsize: 36988 [startup+1110.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8771 0 0 0 110988 27 0 0 25 0 1 0 429674464 37875712 8441 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8441 603 41 0 9206 0 vsize: 36988 [startup+1120.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8771 0 0 0 111988 27 0 0 25 0 1 0 429674464 37875712 8441 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8441 603 41 0 9206 0 vsize: 36988 [startup+1130.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8773 0 0 0 112988 27 0 0 25 0 1 0 429674464 37875712 8443 4294967295 134512640 134672761 3221224640 3221223824 134558771 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8443 603 41 0 9206 0 vsize: 36988 [startup+1140.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 113988 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8455 603 41 0 9206 0 vsize: 36988 [startup+1150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 114989 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8455 603 41 0 9206 0 vsize: 36988 [startup+1160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 115989 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8455 603 41 0 9206 0 vsize: 36988 [startup+1170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 116989 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8455 603 41 0 9206 0 vsize: 36988 [startup+1180.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8785 0 0 0 117989 27 0 0 25 0 1 0 429674464 37875712 8455 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8455 603 41 0 9206 0 vsize: 36988 [startup+1190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8786 0 0 0 118990 27 0 0 25 0 1 0 429674464 37875712 8456 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8456 603 41 0 9206 0 vsize: 36988 [startup+1200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 6191 Raw data (stat): 6191 (minisat+) R 6190 25347 25346 0 -1 0 8788 0 0 0 119990 27 0 0 25 0 1 0 429674464 37875712 8458 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9247 8458 603 41 0 9206 0 vsize: 36988 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 6191 Raw data (stat): 6191 (minisat+) Z 6190 25347 25346 0 -1 12 8791 0 0 0 119990 28 0 0 25 0 1 0 429674464 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.03 CPU time (s): 1200.19 CPU user time (s): 1199.9 CPU system time (s): 0.287956 CPU usage (%): 100.013 Max. virtual memory (Kb): 36988 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####