Name | normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.ex.mem.LdValue.ucl.opb |
MD5SUM | ccbca61851d5d361647c00bb58b30d92 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 129 |
Number of bits of the biggest number in a constraint | 8 |
Biggest sum of numbers in a constraint | 510 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 77106 |
Total number of constraints | 218779 |
Number of constraints which are clauses | 205559 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 13220 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 15 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-05-11 14:48:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2720 boxname=wulflinc31 idbench=303 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: ccbca61851d5d361647c00bb58b30d92 /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.mem.LdValue.ucl.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.mem.LdValue.ucl.opb IDLAUNCH: 2720 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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 : 3 cpu MHz : 451.153 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 915104 kB Buffers: 1972 kB Cached: 91144 kB SwapCached: 6164 kB Active: 64180 kB Inactive: 36488 kB HighTotal: 131008 kB HighFree: 41132 kB LowTotal: 903652 kB LowFree: 873972 kB SwapTotal: 2097892 kB SwapFree: 2091156 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5576 kB Slab: 13132 kB Committed_AS: 63860 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-11 14:51:04 (client local time) WITH STATUS 0 IN 162.287 SECONDS stats: 2720 7 162.287 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c INFO: No cost function. Find solution and finish. c Initial problem consists of 77106 variables and 218779 constraints. #### 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.93 1.01 0.99 2/55 31050 Raw data (stat): 31050 (runsolver) R 31049 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 718726504 1056768 100 4294967295 134512640 135381576 3221221664 3221216880 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 1032 [startup+10.0011 s] Raw data (loadavg): 0.94 1.01 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 24527 0 0 0 943 52 0 0 25 0 1 0 718726504 42930176 7180 4294967295 134512640 134714508 3221221776 3221219828 1077782939 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 10481 7180 1111 63 0 10418 0 vsize: 41924 [startup+20.001 s] Raw data (loadavg): 0.95 1.01 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 122486 0 0 0 1763 232 0 0 25 0 1 0 718726504 59994112 11342 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 14647 11349 1111 63 0 14584 0 vsize: 58588 [startup+30.0019 s] Raw data (loadavg): 0.95 1.01 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 341802 0 0 0 2379 616 0 0 25 0 1 0 718726504 70823936 13877 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 17291 13882 1111 63 0 17228 0 vsize: 69164 [startup+40.0018 s] Raw data (loadavg): 0.96 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 563331 0 0 0 2995 1000 0 0 25 0 1 0 718726504 79790080 16085 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 19480 16090 1111 63 0 19417 0 vsize: 77920 [startup+50.003 s] Raw data (loadavg): 0.97 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 783047 0 0 0 3596 1400 0 0 25 0 1 0 718726504 87805952 18065 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 21437 18065 1111 63 0 21374 0 vsize: 85748 [startup+60.0042 s] Raw data (loadavg): 0.97 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 995846 0 0 0 4207 1788 0 0 25 0 1 0 718726504 94654464 19777 4294967295 134512640 134714508 3221221776 3221219816 1077377266 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 23109 19777 1111 63 0 23046 0 vsize: 92436 [startup+70.0049 s] Raw data (loadavg): 0.97 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 1206603 0 0 0 4811 2185 0 0 25 0 1 0 718726504 102187008 21587 4294967295 134512640 134714508 3221221776 3221220080 134568032 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 24948 21587 1111 63 0 24885 0 vsize: 99792 [startup+80.0058 s] Raw data (loadavg): 0.98 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 1420062 0 0 0 5424 2572 0 0 25 0 1 0 718726504 108441600 23132 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 26475 23132 1111 63 0 26412 0 vsize: 105900 [startup+90.0068 s] Raw data (loadavg): 0.98 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 1626595 0 0 0 6023 2973 0 0 25 0 1 0 718726504 113885184 24489 4294967295 134512640 134714508 3221221776 3221220052 1077414449 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 27804 24489 1111 63 0 27741 0 vsize: 111216 [startup+100.008 s] Raw data (loadavg): 0.98 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 1831201 0 0 0 6639 3357 0 0 25 0 1 0 718726504 120229888 25823 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 29353 25823 1111 63 0 29290 0 vsize: 117412 [startup+110.009 s] Raw data (loadavg): 0.99 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 2034380 0 0 0 7250 3746 0 0 25 0 1 0 718726504 125100032 27061 4294967295 134512640 134714508 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 30542 27061 1111 63 0 30479 0 vsize: 122168 [startup+120.009 s] Raw data (loadavg): 0.99 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 2236820 0 0 0 7868 4128 0 0 25 0 1 0 718726504 130273280 28303 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 31805 28303 1111 63 0 31742 0 vsize: 127220 [startup+130.009 s] Raw data (loadavg): 0.99 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 2436267 0 0 0 8484 4513 0 0 25 0 1 0 718726504 134758400 29448 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 32900 29448 1111 63 0 32837 0 vsize: 131600 [startup+140.011 s] Raw data (loadavg): 0.99 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 2517547 0 0 0 9325 4671 0 0 25 0 1 0 718726504 153403392 34892 4294967295 134512640 134714508 3221221776 3221220736 134584694 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 37452 34892 1111 63 0 37389 0 vsize: 149808 [startup+150.012 s] Raw data (loadavg): 0.99 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 2720701 0 0 0 9828 5168 0 0 25 0 1 0 718726504 545730560 131798 4294967295 134512640 134714508 3221221776 3221220504 134672932 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 133235 131798 1111 63 0 133172 0 vsize: 532940 [startup+160.012 s] Raw data (loadavg): 0.99 1.00 0.99 2/55 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 2825803 0 0 0 10581 5415 0 0 25 0 1 0 718726504 747585536 181040 4294967295 134512640 134714508 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 182516 181040 1111 63 0 182453 0 vsize: 730064 [startup+162.33 s] Raw data (loadavg): 0.99 1.00 0.99 1/54 31050 Raw data (stat): 31050 (bsolo_lpr_cuts) R 31049 7876 7672 0 -1 0 2825803 0 0 0 10581 5415 0 0 25 0 1 0 718726504 747585536 181040 4294967295 134512640 134714508 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 182516 181040 1111 63 0 182453 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 162.33 CPU time (s): 162.287 CPU user time (s): 106.523 CPU system time (s): 55.7645 CPU usage (%): 99.9739 Max. virtual memory (Kb): 730064 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####