Name | normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-agg.opb |
MD5SUM | 3acb5fc9a1a51b5b0d62841ba7c01d77 |
Bench Category | optimization, big integers (OPTBIGINT) |
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 | 3930 |
Biggest coefficient in the objective function | 5373004087296 |
Number of bits for the biggest coefficient in the objective function | 43 |
Sum of the numbers in the objective function | 556141355997381 |
Number of bits of the sum of numbers in the objective function | 49 |
Biggest number in a constraint | 22763326668800000 |
Number of bits of the biggest number in a constraint | 55 |
Biggest sum of numbers in a constraint | 46271983665442689 |
Number of bits of the biggest sum of numbers | 56 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.043992 |
Number of variables | 4890 |
Total number of constraints | 441 |
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 | 441 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 540 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc1 THE 2005-05-27 06:16:41 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23164 boxname=wulflinc1 idbench=808 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3acb5fc9a1a51b5b0d62841ba7c01d77 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-agg.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-agg.opb IDLAUNCH: 23164 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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.053 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: 883172 kB Buffers: 33408 kB Cached: 93060 kB SwapCached: 692 kB Active: 64432 kB Inactive: 64332 kB HighTotal: 131008 kB HighFree: 35168 kB LowTotal: 903652 kB LowFree: 848004 kB SwapTotal: 2097136 kB SwapFree: 2095440 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5780 kB Slab: 17044 kB Committed_AS: 92716 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-27 06:28:05 (client local time) WITH STATUS 134 IN 683.778 SECONDS stats: 23164 7 683.778 134 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c PARSE ERROR! [line 479] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... GNU MP: Cannot allocate memory (size=1073789824) c Parsing PB file... c Converting 269 PB-constraints to clauses... c -- Unit propagations: p c -- Detecting intervals from adjacent constraints: =######################## c -- Clauses(.)/Splits(s): sssssssssssssssssss c ---[ 284]---> BDD-cost:257378 c ---[ 283]---> BDD-cost:14703 c ---[ 280]---> BDD-cost: 28 c ---[ 276]---> BDD-cost:59419 c ---[ 275]---> BDD-cost: 28 c ---[ 274]---> BDD-cost:144289 c ---[ 271]---> BDD-cost: 25 c ---[ 262]---> BDD-cost: 27 c ---[ 259]---> BDD-cost:127786 c ---[ 258]---> BDD-cost:121916 c ---[ 251]---> BDD-cost: 1444 c ---[ 249]---> BDD-cost:18918 c ---[ 248]---> BDD-cost: 23 c ---[ 244]---> BDD-cost:415325 c ---[ 243]---> BDD-cost:41321 c ---[ 242]---> BDD-cost:77381 c ---[ 239]---> BDD-cost:452146 c ---[ 238]---> BDD-cost:83111 c ---[ 234]---> BDD-cost: 6518 c ---[ 228]---> BDD-cost:29033 c ---[ 218]---> BDD-cost: 103 c ---[ 217]---> BDD-cost:627022 c ---[ 216]---> BDD-cost: 103 c ---[ 214]---> BDD-cost: 98 c ---[ 210]---> BDD-cost:15148 c ---[ 200]---> BDD-cost:2683053 c ---[ 199]---> BDD-cost:219387 c ---[ 198]---> BDD-cost:897845 c ---[ 196]---> BDD-cost: 20 c ---[ 195]---> BDD-cost:397433 c ---[ 186]---> BDD-cost:14035 c ---[ 185]---> BDD-cost: 21 c ---[ 184]---> BDD-cost:71593 c ---[ 182]---> BDD-cost:20766 c ---[ 181]---> BDD-cost:1210552 c ---[ 177]---> BDD-cost:380940 c ---[ 175]---> BDD-cost:623454 c ---[ 174]---> BDD-cost:322180 c ---[ 173]---> BDD-cost: 113 c ---[ 172]---> BDD-cost:205508 c ---[ 171]---> BDD-cost:203980 c ---[ 170]---> BDD-cost: 117 c ---[ 169]---> BDD-cost: 112 c ---[ 168]---> BDD-cost:886059 c ---[ 167]---> BDD-cost:438452 c ---[ 165]---> BDD-cost:165158 c ---[ 164]---> BDD-cost:527824 c ---[ 163]---> BDD-cost:459264 c ---[ 162]---> BDD-cost:200603 c ---[ 161]---> BDD-cost:77045 c ---[ 160]---> BDD-cost:60511 c ---[ 159]---> BDD-cost:850025 c ---[ 156]---> BDD-cost:97892 c ---[ 155]---> BDD-cost:636913 c ---[ 154]---> BDD-cost:101925 c ---[ 153]---> BDD-cost:108579 c ---[ 152]---> BDD-cost:159230 c ---[ 151]---> BDD-cost:135371 c ---[ 150]---> BDD-cost:122479 c ---[ 149]---> BDD-cost:119127 c ---[ 148]---> BDD-cost:413719 c ---[ 147]---> BDD-cost:533948 c ---[ 144]---> BDD-cost:253520 c ---[ 142]---> BDD-cost:88784 c ---[ 141]---> BDD-cost:421682 c ---[ 140]---> /oldhome/oroussel/solvers/minisat+_script: line 16: 1696 Aborted $XDIR/minisat+_bignum_static* "$@" #### 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.92 0.98 0.93 2/55 1691 Raw data (stat): 1691 (runsolver) R 1690 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 738854154 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.001 s] Raw data (loadavg): 0.86 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+20.0017 s] Raw data (loadavg): 0.88 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+30.0014 s] Raw data (loadavg): 0.90 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+40.0011 s] Raw data (loadavg): 0.91 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+50.0009 s] Raw data (loadavg): 0.93 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+60.0017 s] Raw data (loadavg): 0.94 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+70.0014 s] Raw data (loadavg): 0.95 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+80.0012 s] Raw data (loadavg): 0.95 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+90.001 s] Raw data (loadavg): 0.96 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+100.001 s] Raw data (loadavg): 0.97 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+110.002 s] Raw data (loadavg): 0.97 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+120.002 s] Raw data (loadavg): 0.97 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+130.002 s] Raw data (loadavg): 0.98 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+140.002 s] Raw data (loadavg): 0.98 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+150.002 s] Raw data (loadavg): 0.98 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+160.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+170.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+180.001 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+190.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+200.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+210.002 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+220.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+230.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+240.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+250.003 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+260.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+270.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+280.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+310.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+320.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+330.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+340.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+350.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+360.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+370.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+380.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+390.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+400.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+410.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+420.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+430.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+440.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+450.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+460.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+470.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+480.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+490.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+500.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+510.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+520.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+530.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+540.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+550.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+560.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+570.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+580.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+590.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+600.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+610.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+620.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+630.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+640.05 s] Raw data (loadavg): 1.07 0.99 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+650.051 s] Raw data (loadavg): 1.06 0.99 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+660.052 s] Raw data (loadavg): 1.05 0.99 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+670.051 s] Raw data (loadavg): 1.04 0.99 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+680.051 s] Raw data (loadavg): 1.04 0.99 0.93 2/56 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+683.697 s] Raw data (loadavg): 1.04 0.99 0.93 1/54 1696 Raw data (stat): 1691 (minisat+_script) S 1690 8378 8377 0 -1 0 300 697 0 0 0 0 18 2 17 0 1 0 738854154 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 0 Child status: 134 Real time (s): 683.697 CPU time (s): 683.778 CPU user time (s): 675.243 CPU system time (s): 8.5347 CPU usage (%): 100.012 Max. virtual memory (Kb): 2128 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####