Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-n3701.opb |
MD5SUM | c5e85fef75cd61b11166b8854f4a9cf3 |
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 | 105000 |
Biggest coefficient in the objective function | 4194304 |
Number of bits for the biggest coefficient in the objective function | 23 |
Sum of the numbers in the objective function | 39244285251 |
Number of bits of the sum of numbers in the objective function | 36 |
Biggest number in a constraint | 4194304 |
Number of bits of the biggest number in a constraint | 23 |
Biggest sum of numbers in a constraint | 39244285251 |
Number of bits of the biggest sum of numbers | 36 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.963853 |
Number of variables | 105000 |
Total number of constraints | 5150 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 5150 |
Minimum length of a constraint | 21 |
Maximum length of a constraint | 2000 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-06-16 19:14:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=26163 boxname=wulflinc6 idbench=1463 idsolver=18 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c5e85fef75cd61b11166b8854f4a9cf3 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-n3701.opb REAL COMMAND: pb2sat-v2 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-n3701.opb IDLAUNCH: 26163 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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.042 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: 662744 kB Buffers: 19804 kB Cached: 328788 kB SwapCached: 996 kB Active: 36316 kB Inactive: 314388 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 662492 kB SwapTotal: 2097136 kB SwapFree: 2095200 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5092 kB Slab: 15528 kB Committed_AS: 63844 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-16 19:21:07 (client local time) WITH STATUS 1 IN 405.896 SECONDS stats: 26163 7 405.896 1 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c This solver internally uses Chaff 2004.11.15 Simplified Unexpected exception : St9bad_alloc #### 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 Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.92 0.97 0.91 2/54 25490 Raw data (stat): 25490 (runsolver) D 25489 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 18 0 1 0 973199456 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 3225161850 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0004 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 2200 0 0 0 993 6 0 0 25 0 1 0 973199456 8093696 1524 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 1976 1525 301 301 0 1675 0 vsize: 7904 [startup+20.0016 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 2755 0 0 0 1991 7 0 0 25 0 1 0 973199456 9580544 2070 4294967295 134512640 135730672 3221224576 3221221664 134561656 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2339 2070 301 301 0 2038 0 vsize: 9356 [startup+30.0012 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 3880 0 0 0 2988 10 0 0 25 0 1 0 973199456 13414400 2483 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3275 2483 301 301 0 2974 0 vsize: 13100 [startup+40.0017 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 4123 0 0 0 3987 12 0 0 25 0 1 0 973199456 14090240 2722 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3440 2722 301 301 0 3139 0 vsize: 13760 [startup+50.0028 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 4376 0 0 0 4987 12 0 0 25 0 1 0 973199456 14766080 2971 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3605 2971 301 301 0 3304 0 vsize: 14420 [startup+60.0026 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 4604 0 0 0 5987 13 0 0 25 0 1 0 973199456 15306752 3195 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3737 3195 301 301 0 3436 0 vsize: 14948 [startup+70.0031 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 4814 0 0 0 6986 14 0 0 25 0 1 0 973199456 15847424 3401 4294967295 134512640 135730672 3221224576 3221221664 134561664 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3869 3401 301 301 0 3568 0 vsize: 15476 [startup+80.0043 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 5009 0 0 0 7986 14 0 0 25 0 1 0 973199456 16388096 3593 4294967295 134512640 135730672 3221224576 3221221664 134561664 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4001 3593 301 301 0 3700 0 vsize: 16004 [startup+90.0041 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 5192 0 0 0 8986 15 0 0 25 0 1 0 973199456 16928768 3773 4294967295 134512640 135730672 3221224576 3221221664 134561664 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4133 3773 301 301 0 3832 0 vsize: 16532 [startup+100.005 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 5366 0 0 0 9985 15 0 0 25 0 1 0 973199456 17334272 3945 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4232 3945 301 301 0 3931 0 vsize: 16928 [startup+110.006 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 7446 0 0 0 10981 20 0 0 25 0 1 0 973199456 25407488 4612 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6203 4612 301 301 0 5902 0 vsize: 24812 [startup+120.007 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 7502 0 0 0 11981 20 0 0 25 0 1 0 973199456 25407488 4665 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6203 4665 301 301 0 5902 0 vsize: 24812 [startup+130.007 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 7555 0 0 0 12982 20 0 0 25 0 1 0 973199456 25407488 4716 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6203 4716 301 301 0 5902 0 vsize: 24812 [startup+140.007 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 7606 0 0 0 13982 20 0 0 25 0 1 0 973199456 25407488 4765 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6203 4765 301 301 0 5902 0 vsize: 24812 [startup+150.008 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 7683 0 0 0 14982 21 0 0 25 0 1 0 973199456 25407488 4839 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6203 4839 301 301 0 5902 0 vsize: 24812 [startup+160.009 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 7732 0 0 0 15982 21 0 0 25 0 1 0 973199456 25407488 4886 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6203 4886 301 301 0 5902 0 vsize: 24812 [startup+170.009 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 7866 0 0 0 16981 22 0 0 25 0 1 0 973199456 25812992 5018 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6302 5018 301 301 0 6001 0 vsize: 25208 [startup+180.01 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 7994 0 0 0 17981 22 0 0 25 0 1 0 973199456 26218496 5144 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6401 5144 301 301 0 6100 0 vsize: 25604 [startup+190.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 8121 0 0 0 18981 23 0 0 25 0 1 0 973199456 26488832 5269 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6467 5269 301 301 0 6166 0 vsize: 25868 [startup+200.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 8244 0 0 0 19981 23 0 0 25 0 1 0 973199456 26759168 5390 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6533 5390 301 301 0 6232 0 vsize: 26132 [startup+210.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 8365 0 0 0 20981 23 0 0 25 0 1 0 973199456 27164672 5509 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6632 5509 301 301 0 6331 0 vsize: 26528 [startup+220.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 8482 0 0 0 21981 23 0 0 25 0 1 0 973199456 27435008 5624 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6698 5624 301 301 0 6397 0 vsize: 26792 [startup+230.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 8599 0 0 0 22981 24 0 0 25 0 1 0 973199456 27705344 5739 4294967295 134512640 135730672 3221224576 3221221664 134561664 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6764 5739 301 301 0 6463 0 vsize: 27056 [startup+240.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 8712 0 0 0 23980 24 0 0 25 0 1 0 973199456 28110848 5850 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6863 5850 301 301 0 6562 0 vsize: 27452 [startup+250.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 8821 0 0 0 24980 25 0 0 25 0 1 0 973199456 28381184 5958 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6929 5958 301 301 0 6628 0 vsize: 27716 [startup+260.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 8931 0 0 0 25980 25 0 0 25 0 1 0 973199456 28651520 6066 4294967295 134512640 135730672 3221224576 3221221664 134561656 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6995 6066 301 301 0 6694 0 vsize: 27980 [startup+270.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 9038 0 0 0 26980 26 0 0 25 0 1 0 973199456 28921856 6171 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7061 6171 301 301 0 6760 0 vsize: 28244 [startup+280.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 9144 0 0 0 27980 26 0 0 25 0 1 0 973199456 29192192 6275 4294967295 134512640 135730672 3221224576 3221221712 134576267 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 7127 6275 301 301 0 6826 0 vsize: 28508 [startup+290.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 9248 0 0 0 28980 27 0 0 25 0 1 0 973199456 29462528 6378 4294967295 134512640 135730672 3221224576 3221221664 134561656 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7193 6378 301 301 0 6892 0 vsize: 28772 [startup+300.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 9349 0 0 0 29980 27 0 0 25 0 1 0 973199456 29732864 6477 4294967295 134512640 135730672 3221224576 3221221664 134561667 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7259 6477 301 301 0 6958 0 vsize: 29036 [startup+310.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 24847 0 0 0 30945 62 0 0 25 0 1 0 973199456 77484032 16536 4294967295 134512640 135730672 3221224576 3220632944 134770685 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 18917 16537 301 301 0 18616 0 vsize: 75668 [startup+320.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 53746 0 0 0 31877 130 0 0 25 0 1 0 973199456 174850048 31410 4294967295 134512640 135730672 3221224576 3220305460 135281175 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 42688 31410 301 301 0 42387 0 vsize: 170752 [startup+330.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 81231 0 0 0 32824 184 0 0 25 0 1 0 973199456 243355648 49487 4294967295 134512640 135730672 3221224576 3220462768 134777016 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 59413 49488 301 301 0 59112 0 vsize: 237652 [startup+340.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 105392 0 0 0 33769 239 0 0 25 0 1 0 973199456 327241728 61150 4294967295 134512640 135730672 3221224576 3220558192 134786278 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 79893 61150 301 301 0 79592 0 vsize: 319572 [startup+350.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 126142 0 0 0 34727 282 0 0 25 0 1 0 973199456 484315136 81416 4294967295 134512640 135730672 3221224576 3220373628 135301630 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 118241 81416 301 301 0 117940 0 vsize: 472964 [startup+360.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 180439 0 0 0 35612 396 0 0 25 0 1 0 973199456 546373632 91817 4294967295 134512640 135730672 3221224576 3220886368 135284078 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 133392 91818 301 301 0 133091 0 vsize: 533568 [startup+370.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 192194 0 0 0 36583 426 0 0 25 0 1 0 973199456 579928064 103361 4294967295 134512640 135730672 3221224576 3220486896 134788717 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 141584 103361 301 301 0 141283 0 vsize: 566336 [startup+380.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 206979 0 0 0 37551 458 0 0 25 0 1 0 973199456 584794112 117903 4294967295 134512640 135730672 3221224576 3221221664 134561669 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 142772 117903 301 301 0 142471 0 vsize: 571088 [startup+390.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 222890 0 0 0 38518 492 0 0 25 0 1 0 973199456 596553728 133580 4294967295 134512640 135730672 3221224576 3220606016 134786302 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 145643 133580 301 301 0 145342 0 vsize: 582572 [startup+400.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 237788 0 0 0 39485 525 0 0 25 0 1 0 973199456 662700032 148280 4294967295 134512640 135730672 3221224576 3220832088 134787727 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 161792 148281 301 301 0 161491 0 vsize: 647168 [startup+405.81 s] Raw data (loadavg): 1.00 0.99 0.91 1/53 25490 Raw data (stat): 25490 (pb2sat-v2) R 25489 25568 25567 0 -1 0 237788 0 0 0 39485 525 0 0 25 0 1 0 973199456 662700032 148280 4294967295 134512640 135730672 3221224576 3220832088 134787727 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 161792 148281 301 301 0 161491 0 vsize: 0 Child status: 1 Real time (s): 405.809 CPU time (s): 405.896 CPU user time (s): 400.316 CPU system time (s): 5.58015 CPU usage (%): 100.022 Max. virtual memory (Kb): 647168 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####