Name | web/uclid_pb_benchmarks/normalized-ooo.tag14.ucl.opb |
MD5SUM | e4be8a88d340bbbbfb27e034f74a6524 |
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 | 65 |
Number of bits of the biggest number in a constraint | 7 |
Biggest sum of numbers in a constraint | 254 |
Number of bits of the biggest sum of numbers | 8 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 148.053 |
Number of variables | 40605 |
Total number of constraints | 118930 |
Number of constraints which are clauses | 117190 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 1740 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 13 |
LAUNCH ON wulflinc29 THE 2005-09-18 19:56:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3850 boxname=wulflinc29 idbench=334 idsolver=4 numberseed=0 MD5SUM SOLVER: 21c3ffd7205c96d5f0784fd273b92938 /oldhome/oroussel/solvers/PBS4 MD5SUM BENCH: e4be8a88d340bbbbfb27e034f74a6524 /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb REAL COMMAND: PBS4 /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb IDLAUNCH: 3850 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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.020 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: 907196 kB Buffers: 33568 kB Cached: 64104 kB SwapCached: 792 kB Active: 32724 kB Inactive: 67684 kB HighTotal: 131008 kB HighFree: 65800 kB LowTotal: 903652 kB LowFree: 841396 kB SwapTotal: 2097892 kB SwapFree: 2096664 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5740 kB Slab: 21372 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:00:20 (client local time) WITH STATUS 20 IN 229.438 SECONDS stats: 3850 7 229.438 20
c PBS v4 by Bashar Al-Rawi & Fadi Aloul c Solving /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb ...... s UNSATISFIABLE c Done, CPU Time=224.083
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 18 0 0 0 0 0 0 0 22 0 1 0 1843934176 978944 2 4294967295 134512640 135450776 3221224576 3221224576 134512960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24531/statm): 239 2 232 232 0 7 0 [pid=24531] vsize: 956 open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-ooo.tag14.ucl.opb [startup+10.0027 s] Raw data (loadavg): 0.89 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 5578 0 0 0 969 19 0 0 25 0 1 0 1843934176 21721088 4562 4294967295 134512640 135450776 3221224576 3221223296 134539285 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 5303 4562 232 232 0 5071 0 [pid=24531] vsize: 21212 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 21212 [startup+20.0035 s] Raw data (loadavg): 0.90 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 6412 0 0 0 1958 25 0 0 25 0 1 0 1843934176 25526272 5363 4294967295 134512640 135450776 3221224576 3221223376 134547495 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 6232 5363 232 232 0 6000 0 [pid=24531] vsize: 24928 Current children cumulated CPU time (s) 19.83 Current children cumulated vsize (Kb) 24928 [startup+30.0042 s] Raw data (loadavg): 0.92 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 7034 0 0 0 2941 32 0 0 25 0 1 0 1843934176 28803072 5985 4294967295 134512640 135450776 3221224576 3221222912 134533833 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 7032 5985 232 232 0 6800 0 [pid=24531] vsize: 28128 Current children cumulated CPU time (s) 29.73 Current children cumulated vsize (Kb) 28128 [startup+40.004 s] Raw data (loadavg): 0.93 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 7582 0 0 0 3924 38 0 0 25 0 1 0 1843934176 31965184 6533 4294967295 134512640 135450776 3221224576 3221223424 134540058 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 7804 6533 232 232 0 7572 0 [pid=24531] vsize: 31216 Current children cumulated CPU time (s) 39.62 Current children cumulated vsize (Kb) 31216 [startup+50.0048 s] Raw data (loadavg): 0.94 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 7816 0 0 0 4909 42 0 0 25 0 1 0 1843934176 32911360 6767 4294967295 134512640 135450776 3221224576 3221222912 134533833 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24531/statm): 8035 6767 232 232 0 7803 0 [pid=24531] vsize: 32140 Current children cumulated CPU time (s) 49.51 Current children cumulated vsize (Kb) 32140 [startup+60.0046 s] Raw data (loadavg): 0.95 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 7929 0 0 0 5889 49 0 0 25 0 1 0 1843934176 37376000 6880 4294967295 134512640 135450776 3221224576 3221222912 134533864 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24531/statm): 9125 6880 232 232 0 8893 0 [pid=24531] vsize: 36500 Current children cumulated CPU time (s) 59.38 Current children cumulated vsize (Kb) 36500 [startup+70.0054 s] Raw data (loadavg): 0.96 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8081 0 0 0 6874 54 0 0 25 0 1 0 1843934176 38051840 7032 4294967295 134512640 135450776 3221224576 3221223296 134539307 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9290 7032 232 232 0 9058 0 [pid=24531] vsize: 37160 Current children cumulated CPU time (s) 69.28 Current children cumulated vsize (Kb) 37160 [startup+80.0061 s] Raw data (loadavg): 0.96 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8190 0 0 0 7861 58 0 0 25 0 1 0 1843934176 38322176 7141 4294967295 134512640 135450776 3221224576 3221223296 134539323 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9356 7141 232 232 0 9124 0 [pid=24531] vsize: 37424 Current children cumulated CPU time (s) 79.19 Current children cumulated vsize (Kb) 37424 [startup+90.0059 s] Raw data (loadavg): 0.97 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8295 0 0 0 8845 65 0 0 25 0 1 0 1843934176 38592512 7246 4294967295 134512640 135450776 3221224576 3221223424 134540101 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9422 7246 232 232 0 9190 0 [pid=24531] vsize: 37688 Current children cumulated CPU time (s) 89.1 Current children cumulated vsize (Kb) 37688 [startup+100.007 s] Raw data (loadavg): 0.97 0.97 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8403 0 0 0 9835 68 0 0 25 0 1 0 1843934176 38727680 7354 4294967295 134512640 135450776 3221224576 3221223296 134539321 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9455 7354 232 232 0 9223 0 [pid=24531] vsize: 37820 Current children cumulated CPU time (s) 99.03 Current children cumulated vsize (Kb) 37820 [startup+110.007 s] Raw data (loadavg): 1.05 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8544 0 0 0 10819 73 0 0 25 0 1 0 1843934176 38862848 7415 4294967295 134512640 135450776 3221224576 3221223296 134539413 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9488 7415 232 232 0 9256 0 [pid=24531] vsize: 37952 Current children cumulated CPU time (s) 108.92 Current children cumulated vsize (Kb) 37952 [startup+120.008 s] Raw data (loadavg): 1.04 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8789 0 0 0 11808 78 0 0 25 0 1 0 1843934176 39534592 7547 4294967295 134512640 135450776 3221224576 3221223296 134539465 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9652 7547 232 232 0 9420 0 [pid=24531] vsize: 38608 Current children cumulated CPU time (s) 118.86 Current children cumulated vsize (Kb) 38608 [startup+130.008 s] Raw data (loadavg): 1.04 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 8793 0 0 0 12790 84 0 0 25 0 1 0 1843934176 39534592 7551 4294967295 134512640 135450776 3221224576 3221223296 134539536 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9652 7551 232 232 0 9420 0 [pid=24531] vsize: 38608 Current children cumulated CPU time (s) 128.74 Current children cumulated vsize (Kb) 38608 [startup+140.008 s] Raw data (loadavg): 1.03 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9059 0 0 0 13777 90 0 0 25 0 1 0 1843934176 39800832 7657 4294967295 134512640 135450776 3221224576 3221223296 134539591 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9717 7657 232 232 0 9485 0 [pid=24531] vsize: 38868 Current children cumulated CPU time (s) 138.67 Current children cumulated vsize (Kb) 38868 [startup+150.009 s] Raw data (loadavg): 1.03 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9325 0 0 0 14765 95 0 0 25 0 1 0 1843934176 39800832 7923 4294967295 134512640 135450776 3221224576 3221223296 134539323 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9717 7923 232 232 0 9485 0 [pid=24531] vsize: 38868 Current children cumulated CPU time (s) 148.6 Current children cumulated vsize (Kb) 38868 [startup+160.008 s] Raw data (loadavg): 1.02 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9533 0 0 0 15758 98 0 0 25 0 1 0 1843934176 39800832 8051 4294967295 134512640 135450776 3221224576 3221223296 134539307 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9717 8051 232 232 0 9485 0 [pid=24531] vsize: 38868 Current children cumulated CPU time (s) 158.56 Current children cumulated vsize (Kb) 38868 [startup+170.008 s] Raw data (loadavg): 1.02 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9622 0 0 0 16740 103 0 0 25 0 1 0 1843934176 39800832 8140 4294967295 134512640 135450776 3221224576 3221223296 134539418 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9717 8140 232 232 0 9485 0 [pid=24531] vsize: 38868 Current children cumulated CPU time (s) 168.43 Current children cumulated vsize (Kb) 38868 [startup+180.009 s] Raw data (loadavg): 1.01 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9714 0 0 0 17721 110 0 0 25 0 1 0 1843934176 39800832 8152 4294967295 134512640 135450776 3221224576 3221223296 134539392 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9717 8152 232 232 0 9485 0 [pid=24531] vsize: 38868 Current children cumulated CPU time (s) 178.31 Current children cumulated vsize (Kb) 38868 [startup+190.009 s] Raw data (loadavg): 1.01 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9801 0 0 0 18712 114 0 0 25 0 1 0 1843934176 39800832 8159 4294967295 134512640 135450776 3221224576 3221223296 134539413 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 9717 8159 232 232 0 9485 0 [pid=24531] vsize: 38868 Current children cumulated CPU time (s) 188.26 Current children cumulated vsize (Kb) 38868 [startup+200.01 s] Raw data (loadavg): 1.01 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 9886 0 0 0 19695 119 0 0 25 0 1 0 1843934176 39800832 8164 4294967295 134512640 135450776 3221224576 3221223296 134539323 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24531/statm): 9717 8164 232 232 0 9485 0 [pid=24531] vsize: 38868 Current children cumulated CPU time (s) 198.14 Current children cumulated vsize (Kb) 38868 [startup+210.01 s] Raw data (loadavg): 1.01 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 10772 0 0 0 20685 124 0 0 25 0 1 0 1843934176 42946560 8201 4294967295 134512640 135450776 3221224576 3221223296 134539536 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24531/statm): 10485 8201 232 232 0 10253 0 [pid=24531] vsize: 41940 Current children cumulated CPU time (s) 208.09 Current children cumulated vsize (Kb) 41940 [startup+220.01 s] Raw data (loadavg): 1.01 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 11051 0 0 0 21675 129 0 0 25 0 1 0 1843934176 42946560 8480 4294967295 134512640 135450776 3221224576 3221223280 134536415 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24531/statm): 10485 8480 232 232 0 10253 0 [pid=24531] vsize: 41940 Current children cumulated CPU time (s) 218.04 Current children cumulated vsize (Kb) 41940 [startup+230.011 s] Raw data (loadavg): 1.00 0.99 0.99 2/56 24531 Raw data (/proc/24531/stat): 24531 (PBS4) R 24530 24531 19818 0 -1 0 11310 0 0 0 22668 132 0 0 25 0 1 0 1843934176 51601408 8739 4294967295 134512640 135450776 3221224576 3221223296 134539307 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24531/statm): 12598 8739 232 232 0 12366 0 [pid=24531] vsize: 50392 Current children cumulated CPU time (s) 228 Current children cumulated vsize (Kb) 50392 One traced child (pid=24531) exited with status: 20 All traced children have exited ! Game is over. Child status: 20 Real time (s): 231.456 CPU time (s): 229.438 CPU user time (s): 228.096 CPU system time (s): 1.3418 CPU usage (%): 99.1283 Max. virtual memory (cumulated for all children) (Kb): 50392
ERROR: no interpretation found !