Name | normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.unbounded.all.ucl.opb |
MD5SUM | e8f0ca38acbe8c57203147fb9147be3a |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
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 | 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 | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 487.167 |
Number of variables | 84836 |
Total number of constraints | 245062 |
Number of constraints which are clauses | 233598 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 11464 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 15 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-05-11 16:22:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2728 boxname=wulflinc31 idbench=304 idsolver=1 numberseed=0 MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef /oldhome/oroussel/solvers/bsolo_lpr MD5SUM BENCH: e8f0ca38acbe8c57203147fb9147be3a /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.unbounded.all.ucl.opb REAL COMMAND: bsolo_lpr /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.unbounded.all.ucl.opb IDLAUNCH: 2728 /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: 902876 kB Buffers: 8744 kB Cached: 98260 kB SwapCached: 4380 kB Active: 65544 kB Inactive: 47308 kB HighTotal: 131008 kB HighFree: 33208 kB LowTotal: 903652 kB LowFree: 869668 kB SwapTotal: 2097892 kB SwapFree: 2092948 kB Dirty: 36 kB Writeback: 0 kB Mapped: 5584 kB Slab: 13160 kB Committed_AS: 63840 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-11 16:25:57 (client local time) WITH STATUS 0 IN 232.566 SECONDS stats: 2728 7 232.566 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 84836 variables and 245062 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 0.98 0.99 2/55 31553 Raw data (stat): 31553 (runsolver) R 31552 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 719288929 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 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.0014 s] Raw data (loadavg): 0.94 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 21306 0 0 0 944 49 0 0 25 0 1 0 719288929 43913216 7419 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 10721 7419 1111 63 0 10658 0 vsize: 42884 [startup+20.0023 s] Raw data (loadavg): 0.95 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 101150 0 0 0 1796 198 0 0 25 0 1 0 719288929 61300736 11684 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 14966 11684 1111 63 0 14903 0 vsize: 59864 [startup+30.0018 s] Raw data (loadavg): 0.95 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 323265 0 0 0 2405 589 0 0 25 0 1 0 719288929 72273920 14291 4294967295 134512640 134714508 3221221776 3221220080 134568044 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 17645 14291 1111 63 0 17582 0 vsize: 70580 [startup+40.0032 s] Raw data (loadavg): 0.96 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 546583 0 0 0 3005 988 0 0 25 0 1 0 719288929 81510400 16556 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 19900 16556 1111 63 0 19837 0 vsize: 79600 [startup+50.0041 s] Raw data (loadavg): 0.97 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 766628 0 0 0 3605 1389 0 0 25 0 1 0 719288929 89526272 18494 4294967295 134512640 134714508 3221221776 3221220080 134568032 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 21857 18494 1111 63 0 21794 0 vsize: 87428 [startup+60.0046 s] Raw data (loadavg): 0.97 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 984867 0 0 0 4210 1784 0 0 25 0 1 0 719288929 96727040 20291 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 23615 20291 1111 63 0 23552 0 vsize: 94460 [startup+70.0049 s] Raw data (loadavg): 0.97 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 1202239 0 0 0 4815 2179 0 0 25 0 1 0 719288929 104394752 22143 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 25487 22143 1111 63 0 25424 0 vsize: 101948 [startup+80.0059 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 1416198 0 0 0 5423 2572 0 0 25 0 1 0 719288929 110260224 23627 4294967295 134512640 134714508 3221221776 3221219436 1077271470 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 26919 23627 1111 63 0 26856 0 vsize: 107676 [startup+90.0064 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 1627289 0 0 0 6033 2962 0 0 25 0 1 0 719288929 116219904 25064 4294967295 134512640 134714508 3221221776 3221220344 134524122 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 28374 25064 1111 63 0 28311 0 vsize: 113496 [startup+100.007 s] Raw data (loadavg): 0.98 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 1837604 0 0 0 6633 3361 0 0 25 0 1 0 719288929 122679296 26486 4294967295 134512640 134714508 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 29951 26486 1111 63 0 29888 0 vsize: 119804 [startup+110.009 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 2044725 0 0 0 7242 3753 0 0 25 0 1 0 719288929 127975424 27729 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 31244 27729 1111 63 0 31181 0 vsize: 124976 [startup+120.01 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 2251193 0 0 0 7850 4145 0 0 25 0 1 0 719288929 132567040 28913 4294967295 134512640 134714508 3221221776 3221219788 1077360259 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 32365 28913 1111 63 0 32302 0 vsize: 129460 [startup+130.011 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 2455661 0 0 0 8468 4527 0 0 25 0 1 0 719288929 137617408 30095 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 33598 30095 1111 63 0 33535 0 vsize: 134392 [startup+140.011 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 2655716 0 0 0 9087 4908 0 0 25 0 1 0 719288929 141967360 31166 4294967295 134512640 134714508 3221221776 3221220080 134568044 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 34660 31166 1111 63 0 34597 0 vsize: 138640 [startup+150.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 2854281 0 0 0 9694 5302 0 0 25 0 1 0 719288929 146309120 32225 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 35720 32225 1111 63 0 35657 0 vsize: 142880 [startup+160.013 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 3052133 0 0 0 10307 5688 0 0 25 0 1 0 719288929 150380544 33211 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 36714 33211 1111 63 0 36651 0 vsize: 146856 [startup+170.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 3144847 0 0 0 11116 5880 0 0 25 0 1 0 719288929 191639552 45310 4294967295 134512640 134714508 3221221776 3221220504 134672946 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 46787 45310 1111 63 0 46724 0 vsize: 187148 [startup+180.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 3315025 0 0 0 11717 6279 0 0 25 0 1 0 719288929 330346496 79036 4294967295 134512640 134714508 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 80651 79036 1111 63 0 80588 0 vsize: 322604 [startup+190.016 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 3531314 0 0 0 12192 6804 0 0 25 0 1 0 719288929 641552384 155138 4294967295 134512640 134714508 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 156629 155138 1111 63 0 156566 0 vsize: 626516 [startup+200.017 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 3656421 0 0 0 12877 7119 0 0 25 0 1 0 719288929 448925696 107937 4294967295 134512640 134714508 3221221776 3221220416 134606468 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 109601 107937 1111 63 0 109538 0 vsize: 438404 [startup+210.018 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 3782616 0 0 0 13574 7423 0 0 25 0 1 0 719288929 444846080 107142 4294967295 134512640 134714508 3221221776 3221220356 134587950 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 108605 107142 1111 63 0 108542 0 vsize: 434420 [startup+220.019 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 3896664 0 0 0 14301 7696 0 0 25 0 1 0 719288929 460144640 110883 4294967295 134512640 134714508 3221221776 3221220304 134542851 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 112340 110883 1111 63 0 112277 0 vsize: 449360 [startup+230.019 s] Raw data (loadavg): 0.99 0.98 0.99 2/55 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 4086872 0 0 0 14830 8166 0 0 25 0 1 0 719288929 725454848 175595 4294967295 134512640 134714508 3221221776 3221220416 134606485 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 177113 175595 1111 63 0 177050 0 vsize: 708452 [startup+232.62 s] Raw data (loadavg): 0.99 0.98 0.99 1/54 31553 Raw data (stat): 31553 (bsolo_lpr) R 31552 7876 7672 0 -1 0 4086872 0 0 0 14830 8166 0 0 25 0 1 0 719288929 725454848 175595 4294967295 134512640 134714508 3221221776 3221220416 134606485 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 177113 175595 1111 63 0 177050 0 vsize: 0 Child ended because it received signal 6 (SIGABRT) Real time (s): 232.619 CPU time (s): 232.566 CPU user time (s): 149.152 CPU system time (s): 83.4133 CPU usage (%): 99.9771 Max. virtual memory (Kb): 708452 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####