Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl15_16_pb.cnf.cr.opb |
MD5SUM | 3f8902c4e8af50006f671e2bddb3e9aa |
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 | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 17 |
Number of bits of the biggest sum of numbers | 5 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.013997 |
Number of variables | 480 |
Total number of constraints | 62 |
Number of constraints which are clauses | 32 |
Number of constraints which are cardinality constraints (but not clauses) | 30 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 15 |
Maximum length of a constraint | 16 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc13 THE 2005-04-13 23:26:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3765 boxname=wulflinc13 idbench=5 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3f8902c4e8af50006f671e2bddb3e9aa /oldhome/oroussel/tmp/wulflinc13/normalized-chnl15_16_pb.cnf.cr.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc13/normalized-chnl15_16_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc13/normalized-chnl15_16_pb.cnf.cr.opb IDLAUNCH: 3765 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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.242 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: 907348 kB Buffers: 34600 kB Cached: 73196 kB SwapCached: 392 kB Active: 53272 kB Inactive: 57796 kB HighTotal: 131008 kB HighFree: 53928 kB LowTotal: 903652 kB LowFree: 853420 kB SwapTotal: 2097136 kB SwapFree: 2096744 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 10652 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 23:46:30 (client local time) WITH STATUS 0 IN 1200.16 SECONDS stats: 3765 7 1200.16 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 62 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................ c ---[ 29]---> BDD-cost: 29 c ---[ 28]---> BDD-cost: 29 c ---[ 27]---> BDD-cost: 29 c ---[ 26]---> BDD-cost: 29 c ---[ 25]---> BDD-cost: 29 c ---[ 24]---> BDD-cost: 29 c ---[ 23]---> BDD-cost: 29 c ---[ 22]---> BDD-cost: 29 c ---[ 21]---> BDD-cost: 29 c ---[ 20]---> BDD-cost: 29 c ---[ 19]---> BDD-cost: 29 c ---[ 18]---> BDD-cost: 29 c ---[ 17]---> BDD-cost: 29 c ---[ 16]---> BDD-cost: 29 c ---[ 15]---> BDD-cost: 29 c ---[ 14]---> BDD-cost: 29 c ---[ 13]---> BDD-cost: 29 c ---[ 12]---> BDD-cost: 29 c ---[ 11]---> BDD-cost: 29 c ---[ 10]---> BDD-cost: 29 c ---[ 9]---> BDD-cost: 29 c ---[ 8]---> BDD-cost: 29 c ---[ 7]---> BDD-cost: 29 c ---[ 6]---> BDD-cost: 29 c ---[ 5]---> BDD-cost: 29 c ---[ 4]---> BDD-cost: 29 c ---[ 3]---> BDD-cost: 29 c ---[ 2]---> BDD-cost: 29 c ---[ 1]---> BDD-cost: 29 c ---[ 0]---> BDD-cost: 29 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 2162 6030 | 648 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/1320 c -- var.elim.: 1320/1320 c -- var.elim.: 592/592 c -- var.elim.: 136/136 c -- subsuming c -- var.elim.: 398/398 c -- var.elim.: 280/280 c -- var.elim.: 104/104 c -- var.elim.: 102/102 c -- var.elim.: 58/58 c -- var.elim.: 50/50 c -- var.elim.: 52/52 c -- var.elim.: 54/54 c -- var.elim.: 56/56 c -- var.elim.: 58/58 c -- var.elim.: 60/60 c -- var.elim.: 136/136 c -- subsuming c -- var.elim.: 550/550 c -- var.elim.: 474/474 c -- var.elim.: 122/122 c -- subsuming c -- var.elim.: 222/222 c -- var.elim.: 106/106 c -- var.elim.: 20/20 c | 0 | 1778 7024 | -- 0 -- -- | -- | -384/1084 c | 0 | 1778 7024 | 711 0 0 nan | 0.000 % | c | 101 | 1778 7024 | 782 101 5283 52.3 | 2.841 % | c | 255 | 1778 7024 | 860 255 13775 54.0 | 2.841 % | c | 481 | 1778 7024 | 946 481 27187 56.5 | 2.841 % | c | 818 | 1778 7024 | 1041 818 48481 59.3 | 2.841 % | c | 1327 | 1778 7024 | 1145 1327 81896 61.7 | 2.841 % | c | 2086 | 1778 7024 | 1259 1126 74705 66.3 | 2.841 % | c | 3225 | 1778 7024 | 1385 1182 86787 73.4 | 2.841 % | c | 4933 | 1778 7024 | 1524 1239 107657 86.9 | 2.841 % | c | 7497 | 1778 7024 | 1676 1408 140052 99.5 | 2.841 % | c | 11343 | 1778 7024 | 1844 1903 162058 85.2 | 2.841 % | c | 17110 | 1778 7024 | 2029 2080 203938 98.0 | 2.842 % | c | 25761 | 1778 7024 | 2232 1716 162311 94.6 | 2.841 % | c | 38737 | 1778 7024 | 2455 2281 238229 104.4 | 2.841 % | c | 58198 | 1778 7024 | 2700 2640 263793 99.9 | 2.841 % | c | 87392 | 1778 7024 | 2970 2217 241731 109.0 | 2.841 % | c | 131184 | 1778 7024 | 3267 2962 287620 97.1 | 2.841 % | c | 196870 | 1778 7024 | 3594 2453 248730 101.4 | 2.841 % | c | 295398 | 1778 #### 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.86 0.93 0.90 2/54 3691 Raw data (stat): 3691 (runsolver) R 3690 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421682725 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99997 s] Raw data (loadavg): 0.88 0.93 0.90 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 876 0 0 0 997 1 0 0 25 0 1 0 421682725 5062656 854 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1236 854 603 41 0 1195 0 vsize: 4944 [startup+20 s] Raw data (loadavg): 0.90 0.93 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 954 0 0 0 1996 2 0 0 25 0 1 0 421682725 5324800 932 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1300 932 603 41 0 1259 0 vsize: 5200 [startup+30.0003 s] Raw data (loadavg): 0.91 0.93 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1030 0 0 0 2996 2 0 0 25 0 1 0 421682725 5713920 1008 4294967295 134512640 134672761 3221224544 3221223584 134612835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1395 1008 603 41 0 1354 0 vsize: 5580 [startup+39.9999 s] Raw data (loadavg): 0.93 0.94 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1056 0 0 0 3995 2 0 0 25 0 1 0 421682725 5832704 1034 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1424 1034 603 41 0 1383 0 vsize: 5696 [startup+50.001 s] Raw data (loadavg): 0.94 0.94 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1126 0 0 0 4995 3 0 0 25 0 1 0 421682725 6098944 1104 4294967295 134512640 134672761 3221224544 3221223584 134612885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1489 1104 603 41 0 1448 0 vsize: 5956 [startup+60.0012 s] Raw data (loadavg): 0.95 0.94 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1140 0 0 0 5995 3 0 0 25 0 1 0 421682725 6098944 1118 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1489 1118 603 41 0 1448 0 vsize: 5956 [startup+70.0009 s] Raw data (loadavg): 0.95 0.94 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1202 0 0 0 6994 3 0 0 25 0 1 0 421682725 6369280 1180 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1555 1180 603 41 0 1514 0 vsize: 6220 [startup+80.002 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1202 0 0 0 7994 4 0 0 25 0 1 0 421682725 6369280 1180 4294967295 134512640 134672761 3221224544 3221223584 134603529 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1555 1180 603 41 0 1514 0 vsize: 6220 [startup+90.0012 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1202 0 0 0 8993 5 0 0 25 0 1 0 421682725 6369280 1180 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1555 1180 603 41 0 1514 0 vsize: 6220 [startup+100.002 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1262 0 0 0 9993 5 0 0 25 0 1 0 421682725 6635520 1240 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1620 1240 603 41 0 1579 0 vsize: 6480 [startup+110.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1272 0 0 0 10993 5 0 0 25 0 1 0 421682725 6635520 1250 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1620 1250 603 41 0 1579 0 vsize: 6480 [startup+120.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1287 0 0 0 11992 5 0 0 25 0 1 0 421682725 6758400 1265 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1650 1265 603 41 0 1609 0 vsize: 6600 [startup+130.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1298 0 0 0 12992 5 0 0 25 0 1 0 421682725 6758400 1276 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1650 1276 603 41 0 1609 0 vsize: 6600 [startup+140.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1325 0 0 0 13992 6 0 0 25 0 1 0 421682725 6885376 1303 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1681 1303 603 41 0 1640 0 vsize: 6724 [startup+150.003 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 14991 6 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1776 1406 603 41 0 1735 0 vsize: 7104 [startup+160.003 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 15991 6 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223408 1075349796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1776 1406 603 41 0 1735 0 vsize: 7104 [startup+170.003 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 16991 7 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1776 1406 603 41 0 1735 0 vsize: 7104 [startup+180.003 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 17990 7 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1776 1406 603 41 0 1735 0 vsize: 7104 [startup+190.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 18990 7 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1776 1406 603 41 0 1735 0 vsize: 7104 [startup+200.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1432 0 0 0 19990 7 0 0 25 0 1 0 421682725 7401472 1410 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1807 1410 603 41 0 1766 0 vsize: 7228 [startup+210.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1493 0 0 0 20989 8 0 0 25 0 1 0 421682725 7659520 1471 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1870 1471 603 41 0 1829 0 vsize: 7480 [startup+220.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1535 0 0 0 21989 8 0 0 25 0 1 0 421682725 7790592 1513 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1902 1513 603 41 0 1861 0 vsize: 7608 [startup+230.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1564 0 0 0 22990 8 0 0 25 0 1 0 421682725 7921664 1542 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1934 1542 603 41 0 1893 0 vsize: 7736 [startup+240.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1583 0 0 0 23990 8 0 0 25 0 1 0 421682725 8011776 1561 4294967295 134512640 134672761 3221224544 3221223728 134615514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1956 1561 603 41 0 1915 0 vsize: 7824 [startup+250.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1604 0 0 0 24990 8 0 0 25 0 1 0 421682725 8134656 1582 4294967295 134512640 134672761 3221224544 3221223600 134644275 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1986 1582 603 41 0 1945 0 vsize: 7944 [startup+260.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1608 0 0 0 25990 8 0 0 25 0 1 0 421682725 8134656 1586 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1986 1586 603 41 0 1945 0 vsize: 7944 [startup+270.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1608 0 0 0 26990 8 0 0 25 0 1 0 421682725 8134656 1586 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1986 1586 603 41 0 1945 0 vsize: 7944 [startup+280.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1612 0 0 0 27990 8 0 0 25 0 1 0 421682725 8134656 1590 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1986 1590 603 41 0 1945 0 vsize: 7944 [startup+290.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1616 0 0 0 28990 8 0 0 25 0 1 0 421682725 8134656 1594 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1986 1594 603 41 0 1945 0 vsize: 7944 [startup+300.003 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1616 0 0 0 29990 8 0 0 25 0 1 0 421682725 8134656 1594 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1986 1594 603 41 0 1945 0 vsize: 7944 [startup+310.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1616 0 0 0 30991 8 0 0 25 0 1 0 421682725 8134656 1594 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1986 1594 603 41 0 1945 0 vsize: 7944 [startup+320.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1668 0 0 0 31991 8 0 0 25 0 1 0 421682725 8392704 1646 4294967295 134512640 134672761 3221224544 3221223704 134614477 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2049 1646 603 41 0 2008 0 vsize: 8196 [startup+330.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1676 0 0 0 32991 8 0 0 25 0 1 0 421682725 8392704 1654 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2049 1654 603 41 0 2008 0 vsize: 8196 [startup+340.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1680 0 0 0 33991 8 0 0 25 0 1 0 421682725 8392704 1658 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2049 1658 603 41 0 2008 0 vsize: 8196 [startup+350.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1696 0 0 0 34991 8 0 0 25 0 1 0 421682725 8507392 1674 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2077 1674 603 41 0 2036 0 vsize: 8308 [startup+360.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1707 0 0 0 35991 8 0 0 25 0 1 0 421682725 8507392 1685 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2077 1685 603 41 0 2036 0 vsize: 8308 [startup+370.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1711 0 0 0 36992 8 0 0 25 0 1 0 421682725 8507392 1689 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2077 1689 603 41 0 2036 0 vsize: 8308 [startup+380.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1724 0 0 0 37992 8 0 0 25 0 1 0 421682725 8622080 1702 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1702 603 41 0 2064 0 vsize: 8420 [startup+390.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1724 0 0 0 38992 8 0 0 25 0 1 0 421682725 8622080 1702 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1702 603 41 0 2064 0 vsize: 8420 [startup+400.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1724 0 0 0 39992 8 0 0 25 0 1 0 421682725 8622080 1702 4294967295 134512640 134672761 3221224544 3221223640 134616347 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1702 603 41 0 2064 0 vsize: 8420 [startup+410.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1724 0 0 0 40992 8 0 0 25 0 1 0 421682725 8622080 1702 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1702 603 41 0 2064 0 vsize: 8420 [startup+420.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1727 0 0 0 41992 8 0 0 25 0 1 0 421682725 8622080 1705 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1705 603 41 0 2064 0 vsize: 8420 [startup+430.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 42993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1709 603 41 0 2064 0 vsize: 8420 [startup+440.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 43993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1709 603 41 0 2064 0 vsize: 8420 [startup+450.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 44993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1709 603 41 0 2064 0 vsize: 8420 [startup+460.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 45993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1709 603 41 0 2064 0 vsize: 8420 [startup+470.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 46993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1709 603 41 0 2064 0 vsize: 8420 [startup+480.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1743 0 0 0 47993 8 0 0 25 0 1 0 421682725 8622080 1721 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1721 603 41 0 2064 0 vsize: 8420 [startup+490.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1744 0 0 0 48993 8 0 0 25 0 1 0 421682725 8622080 1722 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2105 1722 603 41 0 2064 0 vsize: 8420 [startup+500.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1763 0 0 0 49993 8 0 0 25 0 1 0 421682725 8769536 1741 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2141 1741 603 41 0 2100 0 vsize: 8564 [startup+510.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1784 0 0 0 50994 8 0 0 25 0 1 0 421682725 8769536 1762 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2141 1762 603 41 0 2100 0 vsize: 8564 [startup+520.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1800 0 0 0 51994 8 0 0 25 0 1 0 421682725 8884224 1778 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2169 1778 603 41 0 2128 0 vsize: 8676 [startup+530.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1800 0 0 0 52994 8 0 0 25 0 1 0 421682725 8884224 1778 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2169 1778 603 41 0 2128 0 vsize: 8676 [startup+540.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1800 0 0 0 53994 8 0 0 25 0 1 0 421682725 8884224 1778 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2169 1778 603 41 0 2128 0 vsize: 8676 [startup+550.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1801 0 0 0 54994 8 0 0 25 0 1 0 421682725 8884224 1779 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2169 1779 603 41 0 2128 0 vsize: 8676 [startup+560.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1819 0 0 0 55994 9 0 0 25 0 1 0 421682725 9015296 1797 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2201 1797 603 41 0 2160 0 vsize: 8804 [startup+570.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1824 0 0 0 56994 9 0 0 25 0 1 0 421682725 9015296 1802 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2201 1802 603 41 0 2160 0 vsize: 8804 [startup+580.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1828 0 0 0 57995 9 0 0 25 0 1 0 421682725 9015296 1806 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2201 1806 603 41 0 2160 0 vsize: 8804 [startup+590.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1832 0 0 0 58995 9 0 0 25 0 1 0 421682725 9015296 1810 4294967295 134512640 134672761 3221224544 3221223728 134616006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2201 1810 603 41 0 2160 0 vsize: 8804 [startup+600.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1844 0 0 0 59995 9 0 0 25 0 1 0 421682725 9015296 1822 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2201 1822 603 41 0 2160 0 vsize: 8804 [startup+610.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1844 0 0 0 60995 9 0 0 25 0 1 0 421682725 9015296 1822 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2201 1822 603 41 0 2160 0 vsize: 8804 [startup+620.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1848 0 0 0 61995 9 0 0 25 0 1 0 421682725 9129984 1826 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2229 1826 603 41 0 2188 0 vsize: 8916 [startup+630.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1848 0 0 0 62995 9 0 0 25 0 1 0 421682725 9129984 1826 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2229 1826 603 41 0 2188 0 vsize: 8916 [startup+640.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1852 0 0 0 63996 9 0 0 25 0 1 0 421682725 9129984 1830 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2229 1830 603 41 0 2188 0 vsize: 8916 [startup+650.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1856 0 0 0 64996 9 0 0 25 0 1 0 421682725 9129984 1834 4294967295 134512640 134672761 3221224544 3221223640 134616356 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2229 1834 603 41 0 2188 0 vsize: 8916 [startup+660.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1860 0 0 0 65996 9 0 0 25 0 1 0 421682725 9129984 1838 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2229 1838 603 41 0 2188 0 vsize: 8916 [startup+670.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1868 0 0 0 66996 9 0 0 25 0 1 0 421682725 9129984 1846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2229 1846 603 41 0 2188 0 vsize: 8916 [startup+680.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1872 0 0 0 67996 9 0 0 25 0 1 0 421682725 9129984 1850 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2229 1850 603 41 0 2188 0 vsize: 8916 [startup+690.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1877 0 0 0 68996 9 0 0 25 0 1 0 421682725 9244672 1855 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2257 1855 603 41 0 2216 0 vsize: 9028 [startup+700.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1877 0 0 0 69997 9 0 0 25 0 1 0 421682725 9244672 1855 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2257 1855 603 41 0 2216 0 vsize: 9028 [startup+710.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1877 0 0 0 70997 9 0 0 25 0 1 0 421682725 9244672 1855 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2257 1855 603 41 0 2216 0 vsize: 9028 [startup+720.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1880 0 0 0 71997 9 0 0 25 0 1 0 421682725 9244672 1858 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2257 1858 603 41 0 2216 0 vsize: 9028 [startup+730.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1880 0 0 0 72997 9 0 0 25 0 1 0 421682725 9244672 1858 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2257 1858 603 41 0 2216 0 vsize: 9028 [startup+740.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2002 0 0 0 73997 9 0 0 25 0 1 0 421682725 9740288 1980 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2378 1980 603 41 0 2337 0 vsize: 9512 [startup+750.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2090 0 0 0 74997 10 0 0 25 0 1 0 421682725 10121216 2068 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2471 2068 603 41 0 2430 0 vsize: 9884 [startup+760.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2119 0 0 0 75997 10 0 0 25 0 1 0 421682725 10248192 2097 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2502 2097 603 41 0 2461 0 vsize: 10008 [startup+770.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2273 0 0 0 76996 10 0 0 25 0 1 0 421682725 10891264 2251 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2659 2251 603 41 0 2618 0 vsize: 10636 [startup+780.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2275 0 0 0 77997 10 0 0 25 0 1 0 421682725 10883072 2253 4294967295 134512640 134672761 3221224544 3221223584 134612880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2657 2253 603 41 0 2616 0 vsize: 10628 [startup+790.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2286 0 0 0 78997 10 0 0 25 0 1 0 421682725 10883072 2264 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2657 2264 603 41 0 2616 0 vsize: 10628 [startup+800.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2286 0 0 0 79997 10 0 0 25 0 1 0 421682725 10883072 2264 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2657 2264 603 41 0 2616 0 vsize: 10628 [startup+810.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2290 0 0 0 80997 10 0 0 25 0 1 0 421682725 10883072 2268 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2657 2268 603 41 0 2616 0 vsize: 10628 [startup+820.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2299 0 0 0 81997 10 0 0 25 0 1 0 421682725 10997760 2277 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2685 2277 603 41 0 2644 0 vsize: 10740 [startup+830.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2314 0 0 0 82998 10 0 0 25 0 1 0 421682725 10997760 2292 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2685 2292 603 41 0 2644 0 vsize: 10740 [startup+840.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2333 0 0 0 83998 10 0 0 25 0 1 0 421682725 11108352 2311 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2712 2311 603 41 0 2671 0 vsize: 10848 [startup+850.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2337 0 0 0 84998 10 0 0 25 0 1 0 421682725 11108352 2315 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2712 2315 603 41 0 2671 0 vsize: 10848 [startup+860.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2372 0 0 0 85998 10 0 0 25 0 1 0 421682725 11247616 2350 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2746 2350 603 41 0 2705 0 vsize: 10984 [startup+870.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2389 0 0 0 86998 10 0 0 25 0 1 0 421682725 11350016 2367 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2771 2367 603 41 0 2730 0 vsize: 11084 [startup+880.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2402 0 0 0 87998 10 0 0 25 0 1 0 421682725 11350016 2380 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2771 2380 603 41 0 2730 0 vsize: 11084 [startup+890.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2402 0 0 0 88999 10 0 0 25 0 1 0 421682725 11350016 2380 4294967295 134512640 134672761 3221224544 3221223584 134612630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2771 2380 603 41 0 2730 0 vsize: 11084 [startup+900.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2406 0 0 0 89999 10 0 0 25 0 1 0 421682725 11350016 2384 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2771 2384 603 41 0 2730 0 vsize: 11084 [startup+910.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2406 0 0 0 90999 10 0 0 25 0 1 0 421682725 11350016 2384 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2771 2384 603 41 0 2730 0 vsize: 11084 [startup+920.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2406 0 0 0 91999 10 0 0 25 0 1 0 421682725 11350016 2384 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2771 2384 603 41 0 2730 0 vsize: 11084 [startup+930.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2406 0 0 0 92999 10 0 0 25 0 1 0 421682725 11350016 2384 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2771 2384 603 41 0 2730 0 vsize: 11084 [startup+940.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2411 0 0 0 94000 10 0 0 25 0 1 0 421682725 11350016 2389 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2771 2389 603 41 0 2730 0 vsize: 11084 [startup+950.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2426 0 0 0 95000 10 0 0 25 0 1 0 421682725 11464704 2404 4294967295 134512640 134672761 3221224544 3221223584 134612634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2799 2404 603 41 0 2758 0 vsize: 11196 [startup+960.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2441 0 0 0 96000 10 0 0 25 0 1 0 421682725 11509760 2419 4294967295 134512640 134672761 3221224544 3221223584 134603536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2810 2419 603 41 0 2769 0 vsize: 11240 [startup+970.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2441 0 0 0 97000 10 0 0 25 0 1 0 421682725 11509760 2419 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2810 2419 603 41 0 2769 0 vsize: 11240 [startup+980.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2446 0 0 0 98000 10 0 0 25 0 1 0 421682725 11509760 2424 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2810 2424 603 41 0 2769 0 vsize: 11240 [startup+990.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2453 0 0 0 99000 10 0 0 25 0 1 0 421682725 11624448 2431 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2838 2431 603 41 0 2797 0 vsize: 11352 [startup+1000 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2453 0 0 0 100001 10 0 0 25 0 1 0 421682725 11624448 2431 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2838 2431 603 41 0 2797 0 vsize: 11352 [startup+1010 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2453 0 0 0 101001 10 0 0 25 0 1 0 421682725 11624448 2431 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2838 2431 603 41 0 2797 0 vsize: 11352 [startup+1020 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2459 0 0 0 102001 10 0 0 25 0 1 0 421682725 11624448 2437 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2838 2437 603 41 0 2797 0 vsize: 11352 [startup+1030 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2464 0 0 0 103001 10 0 0 25 0 1 0 421682725 11624448 2442 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2838 2442 603 41 0 2797 0 vsize: 11352 [startup+1040 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2472 0 0 0 104001 10 0 0 25 0 1 0 421682725 11624448 2450 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2838 2450 603 41 0 2797 0 vsize: 11352 [startup+1050 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2486 0 0 0 105002 10 0 0 25 0 1 0 421682725 11730944 2464 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2864 2464 603 41 0 2823 0 vsize: 11456 [startup+1060 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2486 0 0 0 106002 10 0 0 25 0 1 0 421682725 11730944 2464 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2864 2464 603 41 0 2823 0 vsize: 11456 [startup+1070 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2503 0 0 0 107002 10 0 0 25 0 1 0 421682725 11730944 2481 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2864 2481 603 41 0 2823 0 vsize: 11456 [startup+1080 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2510 0 0 0 108002 10 0 0 25 0 1 0 421682725 11845632 2488 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2892 2488 603 41 0 2851 0 vsize: 11568 [startup+1090 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2629 0 0 0 109002 10 0 0 25 0 1 0 421682725 12337152 2607 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3012 2607 603 41 0 2971 0 vsize: 12048 [startup+1100 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2639 0 0 0 110002 10 0 0 25 0 1 0 421682725 12304384 2617 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3004 2617 603 41 0 2963 0 vsize: 12016 [startup+1110 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2662 0 0 0 111002 11 0 0 25 0 1 0 421682725 12443648 2640 4294967295 134512640 134672761 3221224544 3221223584 134612927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3038 2640 603 41 0 2997 0 vsize: 12152 [startup+1120 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2691 0 0 0 112002 11 0 0 25 0 1 0 421682725 12562432 2669 4294967295 134512640 134672761 3221224544 3221223584 134612608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3067 2669 603 41 0 3026 0 vsize: 12268 [startup+1130 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2722 0 0 0 113003 11 0 0 25 0 1 0 421682725 12677120 2700 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3095 2700 603 41 0 3054 0 vsize: 12380 [startup+1140 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2771 0 0 0 114003 11 0 0 25 0 1 0 421682725 12910592 2749 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3152 2749 603 41 0 3111 0 vsize: 12608 [startup+1150 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2795 0 0 0 115003 11 0 0 25 0 1 0 421682725 13012992 2773 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3177 2773 603 41 0 3136 0 vsize: 12708 [startup+1160 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2804 0 0 0 116003 11 0 0 25 0 1 0 421682725 13012992 2782 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3177 2782 603 41 0 3136 0 vsize: 12708 [startup+1170 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2824 0 0 0 117003 11 0 0 25 0 1 0 421682725 13123584 2802 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3204 2802 603 41 0 3163 0 vsize: 12816 [startup+1180 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2825 0 0 0 118003 11 0 0 25 0 1 0 421682725 13123584 2803 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3204 2803 603 41 0 3163 0 vsize: 12816 [startup+1190 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2834 0 0 0 119003 11 0 0 25 0 1 0 421682725 13123584 2812 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3204 2812 603 41 0 3163 0 vsize: 12816 [startup+1200 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3691 Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2834 0 0 0 120004 11 0 0 25 0 1 0 421682725 13123584 2812 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3204 2812 603 41 0 3163 0 vsize: 12816 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.01 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 3691 Raw data (stat): 3691 (minisat+) Z 3690 30701 30700 0 -1 12 2834 0 0 0 120004 12 0 0 25 0 1 0 421682725 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.01 CPU time (s): 1200.16 CPU user time (s): 1200.04 CPU system time (s): 0.120981 CPU usage (%): 100.013 Max. virtual memory (Kb): 12816 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####