Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-nw04.opb |
MD5SUM | a5c401bba5afccf02c7b40cb1c595b15 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 87482 |
Biggest coefficient in the objective function | 5220 |
Number of bits for the biggest coefficient in the objective function | 13 |
Sum of the numbers in the objective function | 120189580 |
Number of bits of the sum of numbers in the objective function | 27 |
Biggest number in a constraint | 5220 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 120189580 |
Number of bits of the biggest sum of numbers | 27 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 1.13683 |
Number of variables | 87482 |
Total number of constraints | 87518 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 87518 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 42032 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc12 THE 2005-04-21 23:02:25 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13681 boxname=wulflinc12 idbench=1053 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: a5c401bba5afccf02c7b40cb1c595b15 /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-nw04.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-nw04.opb IDLAUNCH: 13681 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 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.091 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: 207192 kB Buffers: 33488 kB Cached: 771600 kB SwapCached: 508 kB Active: 173344 kB Inactive: 633932 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 206940 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5276 kB Slab: 14548 kB Committed_AS: 63584 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 23:19:53 (client local time) WITH STATUS 0 IN 1048.01 SECONDS stats: 13681 7 1048.01 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### #### 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.87 0.97 0.92 2/54 7902 Raw data (stat): 7902 (runsolver) R 7901 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490660446 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+9.99992 s] Raw data (loadavg): 0.89 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 22973 0 0 0 936 63 0 0 25 0 1 0 490660446 64581632 7176 4294967295 134512640 134672761 3221224624 3220462112 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15767 7176 603 41 0 15726 0 vsize: 63068 [startup+20.0012 s] Raw data (loadavg): 0.91 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 22973 0 0 0 1936 63 0 0 25 0 1 0 490660446 64581632 7176 4294967295 134512640 134672761 3221224624 3220774592 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15767 7176 603 41 0 15726 0 vsize: 63068 [startup+30.0031 s] Raw data (loadavg): 0.92 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 23318 0 0 0 2935 64 0 0 25 0 1 0 490660446 65994752 7521 4294967295 134512640 134672761 3221224624 3220608224 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16112 7521 603 41 0 16071 0 vsize: 64448 [startup+40.0044 s] Raw data (loadavg): 0.93 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 23706 0 0 0 3934 65 0 0 25 0 1 0 490660446 69140480 7909 4294967295 134512640 134672761 3221224624 3220490064 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16880 7909 603 41 0 16839 0 vsize: 67520 [startup+50.0112 s] Raw data (loadavg): 0.94 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 23947 0 0 0 4934 66 0 0 25 0 1 0 490660446 69771264 8150 4294967295 134512640 134672761 3221224624 3220417392 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17034 8150 603 41 0 16993 0 vsize: 68136 [startup+60.0115 s] Raw data (loadavg): 0.95 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 24684 0 0 0 5933 67 0 0 25 0 1 0 490660446 71118848 8557 4294967295 134512640 134672761 3221224624 3220907072 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17363 8557 603 41 0 17322 0 vsize: 69452 [startup+70.0109 s] Raw data (loadavg): 0.96 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 24781 0 0 0 6932 68 0 0 25 0 1 0 490660446 71118848 8654 4294967295 134512640 134672761 3221224624 3220776128 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17363 8654 603 41 0 17322 0 vsize: 69452 [startup+80.0117 s] Raw data (loadavg): 0.96 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 24841 0 0 0 7931 69 0 0 25 0 1 0 490660446 71118848 8714 4294967295 134512640 134672761 3221224624 3219896880 134594089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17363 8714 603 41 0 17322 0 vsize: 69452 [startup+90.012 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 25087 0 0 0 8931 70 0 0 25 0 1 0 490660446 74571776 8877 4294967295 134512640 134672761 3221224624 3220522992 134594103 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18206 8877 603 41 0 18165 0 vsize: 72824 [startup+100.012 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 25457 0 0 0 9930 70 0 0 25 0 1 0 490660446 75186176 9122 4294967295 134512640 134672761 3221224624 3220908992 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18356 9122 603 41 0 18315 0 vsize: 73424 [startup+110.014 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 25672 0 0 0 10929 71 0 0 25 0 1 0 490660446 75624448 9295 4294967295 134512640 134672761 3221224624 3220872800 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18463 9295 603 41 0 18422 0 vsize: 73852 [startup+120.014 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 27455 0 0 0 11925 76 0 0 25 0 1 0 490660446 79683584 10336 4294967295 134512640 134672761 3221224624 3220467200 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19454 10336 603 41 0 19413 0 vsize: 77816 [startup+130.015 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 27597 0 0 0 12924 77 0 0 25 0 1 0 490660446 79986688 10436 4294967295 134512640 134672761 3221224624 3221182496 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19528 10436 603 41 0 19487 0 vsize: 78112 [startup+140.015 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 27601 0 0 0 13924 77 0 0 25 0 1 0 490660446 79986688 10440 4294967295 134512640 134672761 3221224624 3219958416 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19528 10440 603 41 0 19487 0 vsize: 78112 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 27678 0 0 0 14924 77 0 0 25 0 1 0 490660446 80121856 10517 4294967295 134512640 134672761 3221224624 3219438080 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19561 10517 603 41 0 19520 0 vsize: 78244 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28089 0 0 0 15923 78 0 0 25 0 1 0 490660446 80568320 10680 4294967295 134512640 134672761 3221224624 3219914580 134594036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19670 10680 603 41 0 19629 0 vsize: 78680 [startup+170.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28361 0 0 0 16922 79 0 0 25 0 1 0 490660446 81313792 10910 4294967295 134512640 134672761 3221224624 3220895072 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19852 10910 603 41 0 19811 0 vsize: 79408 [startup+180.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28389 0 0 0 17922 80 0 0 25 0 1 0 490660446 81313792 10938 4294967295 134512640 134672761 3221224624 3220387248 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19852 10938 603 41 0 19811 0 vsize: 79408 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7902 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28503 0 0 0 18921 81 0 0 25 0 1 0 490660446 81719296 11052 4294967295 134512640 134672761 3221224624 3220196960 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19951 11052 603 41 0 19910 0 vsize: 79804 [startup+200.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28919 0 0 0 19919 83 0 0 25 0 1 0 490660446 82038784 11220 4294967295 134512640 134672761 3221224624 3220631552 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20029 11220 603 41 0 19988 0 vsize: 80116 [startup+210.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29050 0 0 0 20919 83 0 0 25 0 1 0 490660446 82341888 11309 4294967295 134512640 134672761 3221224624 3220696176 134594084 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20103 11309 603 41 0 20062 0 vsize: 80412 [startup+220.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29377 0 0 0 21918 84 0 0 25 0 1 0 490660446 83083264 11553 4294967295 134512640 134672761 3221224624 3221109344 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20284 11553 603 41 0 20243 0 vsize: 81136 [startup+230.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29680 0 0 0 22917 85 0 0 25 0 1 0 490660446 83230720 11649 4294967295 134512640 134672761 3221224624 3220733312 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20320 11649 603 41 0 20279 0 vsize: 81280 [startup+240.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29721 0 0 0 23917 85 0 0 25 0 1 0 490660446 83365888 11690 4294967295 134512640 134672761 3221224624 3220519632 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20353 11690 603 41 0 20312 0 vsize: 81412 [startup+250.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29721 0 0 0 24917 85 0 0 25 0 1 0 490660446 83365888 11690 4294967295 134512640 134672761 3221224624 3219045456 134594089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20353 11690 603 41 0 20312 0 vsize: 81412 [startup+260.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30091 0 0 0 25916 87 0 0 25 0 1 0 490660446 90398720 11977 4294967295 134512640 134672761 3221224624 3221200352 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22070 11977 603 41 0 22029 0 vsize: 88280 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30389 0 0 0 26915 87 0 0 25 0 1 0 490660446 90595328 12068 4294967295 134512640 134672761 3221224624 3220717568 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22118 12068 603 41 0 22077 0 vsize: 88472 [startup+280.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30431 0 0 0 27915 88 0 0 25 0 1 0 490660446 90730496 12110 4294967295 134512640 134672761 3221224624 3220511664 134594131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22151 12110 603 41 0 22110 0 vsize: 88604 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30431 0 0 0 28914 89 0 0 25 0 1 0 490660446 90730496 12110 4294967295 134512640 134672761 3221224624 3219250512 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22151 12110 603 41 0 22110 0 vsize: 88604 [startup+300.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30788 0 0 0 29913 90 0 0 25 0 1 0 490660446 91471872 12384 4294967295 134512640 134672761 3221224624 3220974848 134594261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22332 12384 603 41 0 22291 0 vsize: 89328 [startup+310.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31007 0 0 0 30912 91 0 0 25 0 1 0 490660446 91508736 12438 4294967295 134512640 134672761 3221224624 3220512896 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22341 12438 603 41 0 22300 0 vsize: 89364 [startup+320.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31148 0 0 0 31912 92 0 0 25 0 1 0 490660446 91811840 12537 4294967295 134512640 134672761 3221224624 3220661328 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22415 12537 603 41 0 22374 0 vsize: 89660 [startup+330.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31148 0 0 0 32912 92 0 0 25 0 1 0 490660446 91811840 12537 4294967295 134512640 134672761 3221224624 3219843312 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22415 12537 603 41 0 22374 0 vsize: 89660 [startup+340.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31468 0 0 0 33910 93 0 0 25 0 1 0 490660446 92553216 12774 4294967295 134512640 134672761 3221224624 3220504832 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22596 12774 603 41 0 22555 0 vsize: 90384 [startup+350.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31694 0 0 0 34909 95 0 0 25 0 1 0 490660446 92495872 12835 4294967295 134512640 134672761 3221224624 3220047200 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22582 12835 603 41 0 22541 0 vsize: 90328 [startup+360.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31854 0 0 0 35909 95 0 0 25 0 1 0 490660446 92798976 12953 4294967295 134512640 134672761 3221224624 3220975424 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22656 12953 603 41 0 22615 0 vsize: 90624 [startup+370.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31874 0 0 0 36909 95 0 0 25 0 1 0 490660446 92934144 12973 4294967295 134512640 134672761 3221224624 3220228848 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22689 12973 603 41 0 22648 0 vsize: 90756 [startup+380.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31874 0 0 0 37909 95 0 0 25 0 1 0 490660446 92934144 12973 4294967295 134512640 134672761 3221224624 3218890320 134594092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22689 12973 603 41 0 22648 0 vsize: 90756 [startup+390.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 34870 0 0 0 38902 102 0 0 25 0 1 0 490660446 99078144 14568 4294967295 134512640 134672761 3221224624 3220896032 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24189 14568 603 41 0 24148 0 vsize: 96756 [startup+400.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35128 0 0 0 39902 103 0 0 25 0 1 0 490660446 99274752 14661 4294967295 134512640 134672761 3221224624 3220222976 134594217 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24237 14661 603 41 0 24196 0 vsize: 96948 [startup+410.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35276 0 0 0 40902 103 0 0 25 0 1 0 490660446 99577856 14767 4294967295 134512640 134672761 3221224624 3221010272 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24311 14767 603 41 0 24270 0 vsize: 97244 [startup+420.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35294 0 0 0 41901 103 0 0 25 0 1 0 490660446 99577856 14785 4294967295 134512640 134672761 3221224624 3220150800 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24311 14785 603 41 0 24270 0 vsize: 97244 [startup+430.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35294 0 0 0 42901 104 0 0 25 0 1 0 490660446 99577856 14785 4294967295 134512640 134672761 3221224624 3218977488 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24311 14785 603 41 0 24270 0 vsize: 97244 [startup+440.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35640 0 0 0 43900 105 0 0 25 0 1 0 490660446 100454400 15048 4294967295 134512640 134672761 3221224624 3220628768 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24525 15048 603 41 0 24484 0 vsize: 98100 [startup+450.027 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36040 0 0 0 44899 106 0 0 25 0 1 0 490660446 100962304 15248 4294967295 134512640 134672761 3221224624 3219305216 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24649 15248 603 41 0 24608 0 vsize: 98596 [startup+460.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36200 0 0 0 45899 107 0 0 25 0 1 0 490660446 101265408 15366 4294967295 134512640 134672761 3221224624 3220243232 134594261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24723 15366 603 41 0 24682 0 vsize: 98892 [startup+470.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36246 0 0 0 46899 107 0 0 25 0 1 0 490660446 101400576 15412 4294967295 134512640 134672761 3221224624 3220800320 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24756 15412 603 41 0 24715 0 vsize: 99024 [startup+480.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36279 0 0 0 47899 107 0 0 25 0 1 0 490660446 101535744 15445 4294967295 134512640 134672761 3221224624 3221205344 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24789 15445 603 41 0 24748 0 vsize: 99156 [startup+490.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36281 0 0 0 48899 107 0 0 25 0 1 0 490660446 101535744 15447 4294967295 134512640 134672761 3221224624 3219622800 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24789 15447 603 41 0 24748 0 vsize: 99156 [startup+500.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36281 0 0 0 49899 108 0 0 25 0 1 0 490660446 101535744 15447 4294967295 134512640 134672761 3221224624 3219156912 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24789 15447 603 41 0 24748 0 vsize: 99156 [startup+510.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36281 0 0 0 50899 108 0 0 25 0 1 0 490660446 101535744 15447 4294967295 134512640 134672761 3221224624 3218187120 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24789 15447 603 41 0 24748 0 vsize: 99156 [startup+520.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36630 0 0 0 51898 109 0 0 25 0 1 0 490660446 102412288 15713 4294967295 134512640 134672761 3221224624 3220043552 134594212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25003 15713 603 41 0 24962 0 vsize: 100012 [startup+530.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36751 0 0 0 52897 110 0 0 25 0 1 0 490660446 102682624 15834 4294967295 134512640 134672761 3221224624 3221029280 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25069 15834 603 41 0 25028 0 vsize: 100276 [startup+540.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37037 0 0 0 53896 111 0 0 25 0 1 0 490660446 102879232 15918 4294967295 134512640 134672761 3221224624 3219486752 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25117 15918 603 41 0 25076 0 vsize: 100468 [startup+550.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37184 0 0 0 54896 111 0 0 25 0 1 0 490660446 103182336 16023 4294967295 134512640 134672761 3221224624 3220270784 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25191 16023 603 41 0 25150 0 vsize: 100764 [startup+560.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37225 0 0 0 55895 111 0 0 25 0 1 0 490660446 103317504 16064 4294967295 134512640 134672761 3221224624 3220776992 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25224 16064 603 41 0 25183 0 vsize: 100896 [startup+570.034 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37257 0 0 0 56895 112 0 0 25 0 1 0 490660446 103317504 16096 4294967295 134512640 134672761 3221224624 3221155712 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25224 16096 603 41 0 25183 0 vsize: 100896 [startup+580.035 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37262 0 0 0 57895 112 0 0 25 0 1 0 490660446 103317504 16101 4294967295 134512640 134672761 3221224624 3219584496 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25224 16101 603 41 0 25183 0 vsize: 100896 [startup+590.035 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37262 0 0 0 58895 112 0 0 25 0 1 0 490660446 103317504 16101 4294967295 134512640 134672761 3221224624 3219195312 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25224 16101 603 41 0 25183 0 vsize: 100896 [startup+600.036 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37262 0 0 0 59895 112 0 0 25 0 1 0 490660446 103317504 16101 4294967295 134512640 134672761 3221224624 3218649840 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25224 16101 603 41 0 25183 0 vsize: 100896 [startup+610.036 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37468 0 0 0 60895 113 0 0 25 0 1 0 490660446 103788544 16224 4294967295 134512640 134672761 3221224624 3218181632 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25339 16224 603 41 0 25298 0 vsize: 101356 [startup+620.037 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37654 0 0 0 61894 113 0 0 25 0 1 0 490660446 104329216 16410 4294967295 134512640 134672761 3221224624 3220443104 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25471 16410 603 41 0 25430 0 vsize: 101884 [startup+630.037 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37727 0 0 0 62894 114 0 0 25 0 1 0 490660446 104464384 16483 4294967295 134512640 134672761 3221224624 3221208704 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25504 16483 603 41 0 25463 0 vsize: 102016 [startup+640.038 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38060 0 0 0 63893 115 0 0 25 0 1 0 490660446 104579072 16574 4294967295 134512640 134672761 3221224624 3219873056 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25532 16574 603 41 0 25491 0 vsize: 102128 [startup+650.039 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38116 0 0 0 64893 115 0 0 25 0 1 0 490660446 104714240 16630 4294967295 134512640 134672761 3221224624 3220548896 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25565 16630 603 41 0 25524 0 vsize: 102260 [startup+660.04 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38154 0 0 0 65893 115 0 0 25 0 1 0 490660446 104849408 16668 4294967295 134512640 134672761 3221224624 3221014304 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25598 16668 603 41 0 25557 0 vsize: 102392 [startup+670.039 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38171 0 0 0 66893 115 0 0 25 0 1 0 490660446 104849408 16685 4294967295 134512640 134672761 3221224624 3219805104 134594089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25598 16685 603 41 0 25557 0 vsize: 102392 [startup+680.04 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38171 0 0 0 67893 116 0 0 25 0 1 0 490660446 104849408 16685 4294967295 134512640 134672761 3221224624 3219409392 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25598 16685 603 41 0 25557 0 vsize: 102392 [startup+690.04 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38171 0 0 0 68892 116 0 0 25 0 1 0 490660446 104849408 16685 4294967295 134512640 134672761 3221224624 3218844432 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25598 16685 603 41 0 25557 0 vsize: 102392 [startup+700.041 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38413 0 0 0 69891 117 0 0 25 0 1 0 490660446 105455616 16844 4294967295 134512640 134672761 3221224624 3218745344 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25746 16844 603 41 0 25705 0 vsize: 102984 [startup+710.042 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38569 0 0 0 70891 118 0 0 25 0 1 0 490660446 105861120 17000 4294967295 134512640 134672761 3221224624 3220633760 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25845 17000 603 41 0 25804 0 vsize: 103380 [startup+720.043 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38801 0 0 0 71891 118 0 0 25 0 1 0 490660446 105762816 17032 4294967295 134512640 134672761 3221224624 3218895392 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25821 17032 603 41 0 25780 0 vsize: 103284 [startup+730.043 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38965 0 0 0 72890 119 0 0 25 0 1 0 490660446 106065920 17154 4294967295 134512640 134672761 3221224624 3220079456 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25895 17154 603 41 0 25854 0 vsize: 103580 [startup+740.044 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39015 0 0 0 73890 119 0 0 25 0 1 0 490660446 106201088 17204 4294967295 134512640 134672761 3221224624 3220688000 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25928 17204 603 41 0 25887 0 vsize: 103712 [startup+750.044 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39050 0 0 0 74890 119 0 0 25 0 1 0 490660446 106336256 17239 4294967295 134512640 134672761 3221224624 3221119520 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25961 17239 603 41 0 25920 0 vsize: 103844 [startup+760.045 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39058 0 0 0 75890 120 0 0 25 0 1 0 490660446 106336256 17247 4294967295 134512640 134672761 3221224624 3219709392 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25961 17247 603 41 0 25920 0 vsize: 103844 [startup+770.045 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39058 0 0 0 76890 120 0 0 25 0 1 0 490660446 106336256 17247 4294967295 134512640 134672761 3221224624 3219279120 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25961 17247 603 41 0 25920 0 vsize: 103844 [startup+780.046 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39058 0 0 0 77890 120 0 0 25 0 1 0 490660446 106336256 17247 4294967295 134512640 134672761 3221224624 3218436912 134594089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25961 17247 603 41 0 25920 0 vsize: 103844 [startup+790.045 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39372 0 0 0 78889 121 0 0 25 0 1 0 490660446 107077632 17478 4294967295 134512640 134672761 3221224624 3219611552 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26142 17478 603 41 0 26101 0 vsize: 104568 [startup+800.047 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39477 0 0 0 79889 121 0 0 25 0 1 0 490660446 107347968 17583 4294967295 134512640 134672761 3221224624 3220887296 134594217 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26208 17583 603 41 0 26167 0 vsize: 104832 [startup+810.048 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39713 0 0 0 80889 122 0 0 25 0 1 0 490660446 119758848 17619 4294967295 134512640 134672761 3221224624 3219409760 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29238 17619 603 41 0 29197 0 vsize: 116952 [startup+820.047 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39870 0 0 0 81888 122 0 0 25 0 1 0 490660446 120197120 17734 4294967295 134512640 134672761 3221224624 3220299200 134594223 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29345 17734 603 41 0 29304 0 vsize: 117380 [startup+830.047 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39914 0 0 0 82888 123 0 0 25 0 1 0 490660446 120332288 17778 4294967295 134512640 134672761 3221224624 3220839968 134594223 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29378 17778 603 41 0 29337 0 vsize: 117512 [startup+840.048 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39945 0 0 0 83887 123 0 0 25 0 1 0 490660446 120332288 17809 4294967295 134512640 134672761 3221224624 3220775568 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29378 17809 603 41 0 29337 0 vsize: 117512 [startup+850.049 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39945 0 0 0 84887 124 0 0 25 0 1 0 490660446 120332288 17809 4294967295 134512640 134672761 3221224624 3219590352 134594131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29378 17809 603 41 0 29337 0 vsize: 117512 [startup+860.05 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39945 0 0 0 85887 124 0 0 25 0 1 0 490660446 120332288 17809 4294967295 134512640 134672761 3221224624 3219103440 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29378 17809 603 41 0 29337 0 vsize: 117512 [startup+870.049 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39945 0 0 0 86886 125 0 0 25 0 1 0 490660446 120332288 17809 4294967295 134512640 134672761 3221224624 3218090448 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29378 17809 603 41 0 29337 0 vsize: 117512 [startup+880.05 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40311 0 0 0 87886 125 0 0 25 0 1 0 490660446 121208832 18092 4294967295 134512640 134672761 3221224624 3220248608 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29592 18092 603 41 0 29551 0 vsize: 118368 [startup+890.05 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40386 0 0 0 88886 125 0 0 25 0 1 0 490660446 121344000 18167 4294967295 134512640 134672761 3221224624 3221163296 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29625 18167 603 41 0 29584 0 vsize: 118500 [startup+900.051 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40760 0 0 0 89885 127 0 0 25 0 1 0 490660446 121868288 18334 4294967295 134512640 134672761 3221224624 3219200288 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29753 18334 603 41 0 29712 0 vsize: 119012 [startup+910.051 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40900 0 0 0 90884 127 0 0 25 0 1 0 490660446 122171392 18432 4294967295 134512640 134672761 3221224624 3219896864 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29827 18432 603 41 0 29786 0 vsize: 119308 [startup+920.052 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40939 0 0 0 91884 128 0 0 25 0 1 0 490660446 122171392 18471 4294967295 134512640 134672761 3221224624 3220372256 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29827 18471 603 41 0 29786 0 vsize: 119308 [startup+930.053 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40969 0 0 0 92884 128 0 0 25 0 1 0 490660446 122306560 18501 4294967295 134512640 134672761 3221224624 3220731776 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29860 18501 603 41 0 29819 0 vsize: 119440 [startup+940.052 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40992 0 0 0 93883 129 0 0 25 0 1 0 490660446 122441728 18524 4294967295 134512640 134672761 3221224624 3221021792 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18524 603 41 0 29852 0 vsize: 119572 [startup+950.054 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 94883 129 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3220111824 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+960.054 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 95883 129 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3219113136 134594095 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+970.053 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 96883 129 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3218831376 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+980.054 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 97883 130 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3218502288 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+990.055 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 98883 130 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3217991568 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+1000.05 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 99883 130 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3217402896 134594089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41369 0 0 0 100882 131 0 0 25 0 1 0 490660446 123318272 18818 4294967295 134512640 134672761 3221224624 3219559040 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30107 18818 603 41 0 30066 0 vsize: 120428 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41460 0 0 0 101882 132 0 0 25 0 1 0 490660446 123453440 18909 4294967295 134512640 134672761 3221224624 3220550624 134594212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30140 18909 603 41 0 30099 0 vsize: 120560 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41533 0 0 0 102882 132 0 0 25 0 1 0 490660446 123723776 18982 4294967295 134512640 134672761 3221224624 3221138432 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30206 18982 603 41 0 30165 0 vsize: 120824 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 42114 0 0 0 103880 133 0 0 25 0 1 0 490660446 124223488 19272 4294967295 134512640 134672761 3221224624 3220483056 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30328 19272 603 41 0 30287 0 vsize: 121312 [startup+1047.93 s] Raw data (loadavg): 0.99 0.97 0.92 1/53 7904 Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 42114 0 0 0 103880 133 0 0 25 0 1 0 490660446 124223488 19272 4294967295 134512640 134672761 3221224624 3220483056 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30328 19272 603 41 0 30287 0 vsize: 0 Child ended because it received signal 11 (SIGSEGV) Real time (s): 1047.92 CPU time (s): 1048.01 CPU user time (s): 1045.93 CPU system time (s): 2.08168 CPU usage (%): 100.008 Max. virtual memory (Kb): 121312 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####