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 wulflinc2 THE 2005-04-14 03:20:55 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4517 boxname=wulflinc2 idbench=5 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3f8902c4e8af50006f671e2bddb3e9aa /oldhome/oroussel/tmp/wulflinc2/normalized-chnl15_16_pb.cnf.cr.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-chnl15_16_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc2/normalized-chnl15_16_pb.cnf.cr.opb IDLAUNCH: 4517 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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.191 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: 893864 kB Buffers: 35500 kB Cached: 84652 kB SwapCached: 4 kB Active: 58008 kB Inactive: 64984 kB HighTotal: 131008 kB HighFree: 42588 kB LowTotal: 903652 kB LowFree: 851276 kB SwapTotal: 2097136 kB SwapFree: 2097132 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6916 kB Slab: 12200 kB Committed_AS: 71676 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 03:40:58 (client local time) WITH STATUS 0 IN 1200.17 SECONDS stats: 4517 7 1200.17 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 ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 3812 10920 | 1270 0 0 nan | 0.000 % | c | 104 | 3812 10920 | 1397 104 5751 55.3 | 2.222 % | c | 254 | 3767 10785 | 1536 225 13712 60.9 | 2.889 % | c | 479 | 3752 10740 | 1690 441 34253 77.7 | 3.111 % | c | 816 | 3742 10710 | 1859 774 59164 76.4 | 3.259 % | c | 1322 | 3727 10665 | 2045 1274 101292 79.5 | 3.482 % | c | 2082 | 3717 10635 | 2249 2028 179745 88.6 | 3.630 % | c | 3221 | 3692 10560 | 2474 1829 170632 93.3 | 4.000 % | c | 4931 | 3682 10530 | 2722 2190 237517 108.5 | 4.148 % | c | 7493 | 3657 10455 | 2994 1776 202464 114.0 | 4.519 % | c | 11337 | 3652 10440 | 3294 2184 248774 113.9 | 4.593 % | c | 17106 | 3622 10350 | 3623 2452 272522 111.1 | 5.037 % | c | 25755 | 3572 10200 | 3985 3052 345591 113.2 | 5.778 % | c | 38730 | 3467 9885 | 4384 2932 272102 92.8 | 7.333 % | c | 58191 | 3323 9455 | 4822 3250 335612 103.3 | 9.482 % | c | 87384 | 3078 8720 | 5305 3861 333434 86.4 | 13.111 % | c | 131173 | 2662 7480 | 5835 4082 414316 101.5 | 19.333 % | c | 196857 | 2465 6895 | 6419 5973 616395 103.2 | 22.296 % | c | 295385 | 2257 6275 | 7061 6199 614660 99.2 | 25.407 % | c | 443174 | 1951 5365 | 7767 7248 676251 93.3 | 30.000 % | c | 664857 | 1931 5305 | 8543 6162 519332 84.3 | 30.296 % | c | 997383 | 1754 4800 | 9398 7206 513867 71.3 | 33.111 % | #### 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.92 2/54 26245 Raw data (stat): 26245 (runsolver) R 26244 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423087806 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0006 s] Raw data (loadavg): 0.93 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 973 0 0 0 996 2 0 0 25 0 1 0 423087806 5496832 951 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1342 951 603 41 0 1301 0 vsize: 5368 [startup+20.0029 s] Raw data (loadavg): 0.94 0.98 0.92 5/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1056 0 0 0 1996 3 0 0 25 0 1 0 423087806 5902336 1034 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1441 1034 603 41 0 1400 0 vsize: 5764 [startup+30.0036 s] Raw data (loadavg): 0.95 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1159 0 0 0 2996 3 0 0 25 0 1 0 423087806 6303744 1137 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1539 1137 603 41 0 1498 0 vsize: 6156 [startup+40.0037 s] Raw data (loadavg): 0.96 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1229 0 0 0 3995 4 0 0 25 0 1 0 423087806 6574080 1207 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1605 1207 603 41 0 1564 0 vsize: 6420 [startup+50.004 s] Raw data (loadavg): 0.96 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1292 0 0 0 4994 4 0 0 25 0 1 0 423087806 6844416 1270 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1671 1270 603 41 0 1630 0 vsize: 6684 [startup+60.0037 s] Raw data (loadavg): 0.97 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1376 0 0 0 5994 4 0 0 25 0 1 0 423087806 7114752 1354 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1737 1354 603 41 0 1696 0 vsize: 6948 [startup+70.0034 s] Raw data (loadavg): 0.97 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1398 0 0 0 6994 4 0 0 25 0 1 0 423087806 7254016 1376 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1771 1376 603 41 0 1730 0 vsize: 7084 [startup+80.0041 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1428 0 0 0 7993 5 0 0 25 0 1 0 423087806 7393280 1406 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1805 1406 603 41 0 1764 0 vsize: 7220 [startup+90.0037 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1467 0 0 0 8993 5 0 0 25 0 1 0 423087806 7532544 1445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1839 1445 603 41 0 1798 0 vsize: 7356 [startup+100.004 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1513 0 0 0 9992 6 0 0 25 0 1 0 423087806 7827456 1491 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1911 1491 603 41 0 1870 0 vsize: 7644 [startup+110.005 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1582 0 0 0 10993 6 0 0 25 0 1 0 423087806 8093696 1560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1976 1560 603 41 0 1935 0 vsize: 7904 [startup+120.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1598 0 0 0 11992 6 0 0 25 0 1 0 423087806 8241152 1576 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2012 1576 603 41 0 1971 0 vsize: 8048 [startup+130.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1649 0 0 0 12993 6 0 0 25 0 1 0 423087806 8376320 1627 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2045 1627 603 41 0 2004 0 vsize: 8180 [startup+140.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1721 0 0 0 13993 6 0 0 25 0 1 0 423087806 8646656 1699 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2111 1699 603 41 0 2070 0 vsize: 8444 [startup+150.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1732 0 0 0 14993 6 0 0 25 0 1 0 423087806 8785920 1710 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2145 1710 603 41 0 2104 0 vsize: 8580 [startup+160.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1769 0 0 0 15993 6 0 0 25 0 1 0 423087806 8921088 1747 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2178 1747 603 41 0 2137 0 vsize: 8712 [startup+170.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1792 0 0 0 16993 6 0 0 25 0 1 0 423087806 9056256 1770 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2211 1770 603 41 0 2170 0 vsize: 8844 [startup+180.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1813 0 0 0 17993 6 0 0 25 0 1 0 423087806 9056256 1791 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2211 1791 603 41 0 2170 0 vsize: 8844 [startup+190.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1865 0 0 0 18993 6 0 0 25 0 1 0 423087806 9326592 1843 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2277 1843 603 41 0 2236 0 vsize: 9108 [startup+200.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1878 0 0 0 19993 6 0 0 25 0 1 0 423087806 9461760 1856 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2310 1856 603 41 0 2269 0 vsize: 9240 [startup+210.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1907 0 0 0 20993 6 0 0 25 0 1 0 423087806 9625600 1885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2350 1885 603 41 0 2309 0 vsize: 9400 [startup+220.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1931 0 0 0 21994 6 0 0 25 0 1 0 423087806 9625600 1909 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2350 1909 603 41 0 2309 0 vsize: 9400 [startup+230.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 1936 0 0 0 22994 6 0 0 25 0 1 0 423087806 9773056 1914 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2386 1914 603 41 0 2345 0 vsize: 9544 [startup+240.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2004 0 0 0 23994 6 0 0 25 0 1 0 423087806 10051584 1982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2454 1982 603 41 0 2413 0 vsize: 9816 [startup+250.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2021 0 0 0 24994 6 0 0 25 0 1 0 423087806 10051584 1999 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2454 1999 603 41 0 2413 0 vsize: 9816 [startup+260.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2047 0 0 0 25994 7 0 0 25 0 1 0 423087806 10199040 2025 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2490 2025 603 41 0 2449 0 vsize: 9960 [startup+270.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2096 0 0 0 26994 7 0 0 25 0 1 0 423087806 10346496 2074 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2526 2074 603 41 0 2485 0 vsize: 10104 [startup+280.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2106 0 0 0 27994 7 0 0 25 0 1 0 423087806 10493952 2084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2562 2084 603 41 0 2521 0 vsize: 10248 [startup+290.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2114 0 0 0 28994 7 0 0 25 0 1 0 423087806 10493952 2092 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2562 2092 603 41 0 2521 0 vsize: 10248 [startup+300.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2117 0 0 0 29994 7 0 0 25 0 1 0 423087806 10493952 2095 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2562 2095 603 41 0 2521 0 vsize: 10248 [startup+310.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2118 0 0 0 30995 7 0 0 25 0 1 0 423087806 10493952 2096 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2562 2096 603 41 0 2521 0 vsize: 10248 [startup+320.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2128 0 0 0 31995 7 0 0 25 0 1 0 423087806 10493952 2106 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2562 2106 603 41 0 2521 0 vsize: 10248 [startup+330.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2136 0 0 0 32995 7 0 0 25 0 1 0 423087806 10493952 2114 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2562 2114 603 41 0 2521 0 vsize: 10248 [startup+340.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2142 0 0 0 33995 7 0 0 25 0 1 0 423087806 10657792 2120 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2602 2120 603 41 0 2561 0 vsize: 10408 [startup+350.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2195 0 0 0 34994 7 0 0 25 0 1 0 423087806 10792960 2173 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2635 2173 603 41 0 2594 0 vsize: 10540 [startup+360.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2250 0 0 0 35993 7 0 0 25 0 1 0 423087806 11063296 2228 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2701 2228 603 41 0 2660 0 vsize: 10804 [startup+370.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2251 0 0 0 36994 7 0 0 25 0 1 0 423087806 11063296 2229 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2701 2229 603 41 0 2660 0 vsize: 10804 [startup+380.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2271 0 0 0 37994 7 0 0 25 0 1 0 423087806 11206656 2249 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2736 2249 603 41 0 2695 0 vsize: 10944 [startup+390.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2272 0 0 0 38994 7 0 0 25 0 1 0 423087806 11206656 2250 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2736 2250 603 41 0 2695 0 vsize: 10944 [startup+400.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2338 0 0 0 39994 7 0 0 25 0 1 0 423087806 11341824 2316 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2769 2316 603 41 0 2728 0 vsize: 11076 [startup+410.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2339 0 0 0 40994 7 0 0 25 0 1 0 423087806 11341824 2317 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2769 2317 603 41 0 2728 0 vsize: 11076 [startup+420.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2346 0 0 0 41994 8 0 0 25 0 1 0 423087806 11501568 2324 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2808 2324 603 41 0 2767 0 vsize: 11232 [startup+430.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2351 0 0 0 42994 8 0 0 25 0 1 0 423087806 11501568 2329 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2808 2329 603 41 0 2767 0 vsize: 11232 [startup+440.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2361 0 0 0 43995 8 0 0 25 0 1 0 423087806 11501568 2339 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2808 2339 603 41 0 2767 0 vsize: 11232 [startup+450.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2367 0 0 0 44995 8 0 0 25 0 1 0 423087806 11501568 2345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2808 2345 603 41 0 2767 0 vsize: 11232 [startup+460.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2367 0 0 0 45995 8 0 0 25 0 1 0 423087806 11501568 2345 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2808 2345 603 41 0 2767 0 vsize: 11232 [startup+470.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2367 0 0 0 46995 8 0 0 25 0 1 0 423087806 11501568 2345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2808 2345 603 41 0 2767 0 vsize: 11232 [startup+480.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2372 0 0 0 47995 8 0 0 25 0 1 0 423087806 11665408 2350 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2848 2350 603 41 0 2807 0 vsize: 11392 [startup+490.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2373 0 0 0 48995 8 0 0 25 0 1 0 423087806 11665408 2351 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2848 2351 603 41 0 2807 0 vsize: 11392 [startup+500.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2374 0 0 0 49995 8 0 0 25 0 1 0 423087806 11665408 2352 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2848 2352 603 41 0 2807 0 vsize: 11392 [startup+510.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2379 0 0 0 50996 8 0 0 25 0 1 0 423087806 11665408 2357 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2848 2357 603 41 0 2807 0 vsize: 11392 [startup+520.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2424 0 0 0 51995 8 0 0 25 0 1 0 423087806 11800576 2402 4294967295 134512640 134672761 3221224544 3221223776 134541847 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2881 2402 603 41 0 2840 0 vsize: 11524 [startup+530.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2427 0 0 0 52995 8 0 0 25 0 1 0 423087806 11800576 2405 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2881 2405 603 41 0 2840 0 vsize: 11524 [startup+540.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2432 0 0 0 53995 8 0 0 25 0 1 0 423087806 11964416 2410 4294967295 134512640 134672761 3221224544 3221223648 134559802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2921 2410 603 41 0 2880 0 vsize: 11684 [startup+550.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2445 0 0 0 54996 8 0 0 25 0 1 0 423087806 11964416 2423 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2921 2423 603 41 0 2880 0 vsize: 11684 [startup+560.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2445 0 0 0 55996 8 0 0 25 0 1 0 423087806 11964416 2423 4294967295 134512640 134672761 3221224544 3221223728 134559613 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2921 2423 603 41 0 2880 0 vsize: 11684 [startup+570.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2464 0 0 0 56996 8 0 0 25 0 1 0 423087806 12099584 2442 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2954 2442 603 41 0 2913 0 vsize: 11816 [startup+580.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2558 0 0 0 57996 8 0 0 25 0 1 0 423087806 12541952 2536 4294967295 134512640 134672761 3221224544 3221223680 134560694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3062 2536 603 41 0 3021 0 vsize: 12248 [startup+590.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2631 0 0 0 58995 9 0 0 25 0 1 0 423087806 12836864 2609 4294967295 134512640 134672761 3221224544 3221223648 134560347 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3134 2609 603 41 0 3093 0 vsize: 12536 [startup+600.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2653 0 0 0 59996 9 0 0 25 0 1 0 423087806 12980224 2631 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3169 2631 603 41 0 3128 0 vsize: 12676 [startup+610.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2691 0 0 0 60996 9 0 0 25 0 1 0 423087806 13127680 2669 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3205 2669 603 41 0 3164 0 vsize: 12820 [startup+620.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2719 0 0 0 61996 9 0 0 25 0 1 0 423087806 13262848 2697 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3238 2697 603 41 0 3197 0 vsize: 12952 [startup+630.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2751 0 0 0 62996 9 0 0 25 0 1 0 423087806 13426688 2729 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3278 2729 603 41 0 3237 0 vsize: 13112 [startup+640.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2763 0 0 0 63996 9 0 0 25 0 1 0 423087806 13590528 2741 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3318 2741 603 41 0 3277 0 vsize: 13272 [startup+650.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2764 0 0 0 64997 9 0 0 25 0 1 0 423087806 13590528 2742 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3318 2742 603 41 0 3277 0 vsize: 13272 [startup+660.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2788 0 0 0 65997 9 0 0 25 0 1 0 423087806 13590528 2766 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3318 2766 603 41 0 3277 0 vsize: 13272 [startup+670.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2810 0 0 0 66997 9 0 0 25 0 1 0 423087806 13754368 2788 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3358 2788 603 41 0 3317 0 vsize: 13432 [startup+680.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2815 0 0 0 67997 9 0 0 25 0 1 0 423087806 13754368 2793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3358 2793 603 41 0 3317 0 vsize: 13432 [startup+690.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2818 0 0 0 68997 9 0 0 25 0 1 0 423087806 13754368 2796 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3358 2796 603 41 0 3317 0 vsize: 13432 [startup+700.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2840 0 0 0 69997 9 0 0 25 0 1 0 423087806 13918208 2818 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3398 2818 603 41 0 3357 0 vsize: 13592 [startup+710.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 2840 0 0 0 70997 9 0 0 25 0 1 0 423087806 13918208 2818 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3398 2818 603 41 0 3357 0 vsize: 13592 [startup+720.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3175 0 0 0 71996 10 0 0 25 0 1 0 423087806 15405056 3153 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3761 3153 603 41 0 3720 0 vsize: 15044 [startup+730.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3217 0 0 0 72996 10 0 0 25 0 1 0 423087806 15540224 3195 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3794 3195 603 41 0 3753 0 vsize: 15176 [startup+740.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3282 0 0 0 73996 10 0 0 25 0 1 0 423087806 15843328 3260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3868 3260 603 41 0 3827 0 vsize: 15472 [startup+750.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3310 0 0 0 74996 10 0 0 25 0 1 0 423087806 15986688 3288 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3288 603 41 0 3862 0 vsize: 15612 [startup+760.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3317 0 0 0 75997 10 0 0 25 0 1 0 423087806 15986688 3295 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3295 603 41 0 3862 0 vsize: 15612 [startup+770.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3357 0 0 0 76997 11 0 0 25 0 1 0 423087806 16257024 3335 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3969 3335 603 41 0 3928 0 vsize: 15876 [startup+780.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3383 0 0 0 77997 11 0 0 25 0 1 0 423087806 16257024 3361 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3969 3361 603 41 0 3928 0 vsize: 15876 [startup+790.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3383 0 0 0 78997 11 0 0 25 0 1 0 423087806 16257024 3361 4294967295 134512640 134672761 3221224544 3221223648 134554647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3969 3361 603 41 0 3928 0 vsize: 15876 [startup+800.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3432 0 0 0 79997 11 0 0 25 0 1 0 423087806 16547840 3410 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4040 3410 603 41 0 3999 0 vsize: 16160 [startup+810.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3444 0 0 0 80997 11 0 0 25 0 1 0 423087806 16547840 3422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4040 3422 603 41 0 3999 0 vsize: 16160 [startup+820.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3445 0 0 0 81997 11 0 0 25 0 1 0 423087806 16547840 3423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4040 3423 603 41 0 3999 0 vsize: 16160 [startup+830.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3463 0 0 0 82998 11 0 0 25 0 1 0 423087806 16711680 3441 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4080 3441 603 41 0 4039 0 vsize: 16320 [startup+840.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3474 0 0 0 83998 11 0 0 25 0 1 0 423087806 16711680 3452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4080 3452 603 41 0 4039 0 vsize: 16320 [startup+850.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3493 0 0 0 84998 11 0 0 25 0 1 0 423087806 16875520 3471 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4120 3471 603 41 0 4079 0 vsize: 16480 [startup+860.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3507 0 0 0 85998 11 0 0 25 0 1 0 423087806 16875520 3485 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4120 3485 603 41 0 4079 0 vsize: 16480 [startup+870.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3523 0 0 0 86998 11 0 0 25 0 1 0 423087806 17010688 3501 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4153 3501 603 41 0 4112 0 vsize: 16612 [startup+880.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3526 0 0 0 87998 11 0 0 25 0 1 0 423087806 17010688 3504 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4153 3504 603 41 0 4112 0 vsize: 16612 [startup+890.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3532 0 0 0 88999 11 0 0 25 0 1 0 423087806 17010688 3510 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4153 3510 603 41 0 4112 0 vsize: 16612 [startup+900.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3541 0 0 0 89999 11 0 0 25 0 1 0 423087806 17010688 3519 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4153 3519 603 41 0 4112 0 vsize: 16612 [startup+910.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3541 0 0 0 90999 11 0 0 25 0 1 0 423087806 17010688 3519 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4153 3519 603 41 0 4112 0 vsize: 16612 [startup+920.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3549 0 0 0 91999 11 0 0 25 0 1 0 423087806 17010688 3527 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4153 3527 603 41 0 4112 0 vsize: 16612 [startup+930.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3570 0 0 0 92999 11 0 0 25 0 1 0 423087806 17158144 3548 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4189 3548 603 41 0 4148 0 vsize: 16756 [startup+940.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3571 0 0 0 94000 11 0 0 25 0 1 0 423087806 17158144 3549 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4189 3549 603 41 0 4148 0 vsize: 16756 [startup+950.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3571 0 0 0 95000 11 0 0 25 0 1 0 423087806 17158144 3549 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4189 3549 603 41 0 4148 0 vsize: 16756 [startup+960.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3573 0 0 0 96000 11 0 0 25 0 1 0 423087806 17158144 3551 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4189 3551 603 41 0 4148 0 vsize: 16756 [startup+970.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3590 0 0 0 97000 11 0 0 25 0 1 0 423087806 17321984 3568 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4229 3568 603 41 0 4188 0 vsize: 16916 [startup+980.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3602 0 0 0 98000 11 0 0 25 0 1 0 423087806 17321984 3580 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4229 3580 603 41 0 4188 0 vsize: 16916 [startup+990.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3618 0 0 0 99001 11 0 0 25 0 1 0 423087806 17469440 3596 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3596 603 41 0 4224 0 vsize: 17060 [startup+1000.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3624 0 0 0 100001 11 0 0 25 0 1 0 423087806 17469440 3602 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3602 603 41 0 4224 0 vsize: 17060 [startup+1010.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3648 0 0 0 101001 11 0 0 25 0 1 0 423087806 17633280 3626 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4305 3626 603 41 0 4264 0 vsize: 17220 [startup+1020.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3651 0 0 0 102001 11 0 0 25 0 1 0 423087806 17633280 3629 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4305 3629 603 41 0 4264 0 vsize: 17220 [startup+1030.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3657 0 0 0 103001 11 0 0 25 0 1 0 423087806 17633280 3635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4305 3635 603 41 0 4264 0 vsize: 17220 [startup+1040.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3668 0 0 0 104001 11 0 0 25 0 1 0 423087806 17633280 3646 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4305 3646 603 41 0 4264 0 vsize: 17220 [startup+1050.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3668 0 0 0 105002 11 0 0 25 0 1 0 423087806 17633280 3646 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4305 3646 603 41 0 4264 0 vsize: 17220 [startup+1060.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3680 0 0 0 106002 11 0 0 25 0 1 0 423087806 17797120 3658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4345 3658 603 41 0 4304 0 vsize: 17380 [startup+1070.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3680 0 0 0 107002 11 0 0 25 0 1 0 423087806 17797120 3658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4345 3658 603 41 0 4304 0 vsize: 17380 [startup+1080.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3690 0 0 0 108002 11 0 0 25 0 1 0 423087806 17797120 3668 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4345 3668 603 41 0 4304 0 vsize: 17380 [startup+1090.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3692 0 0 0 109002 11 0 0 25 0 1 0 423087806 17797120 3670 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4345 3670 603 41 0 4304 0 vsize: 17380 [startup+1100.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3692 0 0 0 110003 11 0 0 25 0 1 0 423087806 17797120 3670 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4345 3670 603 41 0 4304 0 vsize: 17380 [startup+1110.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3700 0 0 0 111002 11 0 0 25 0 1 0 423087806 17797120 3678 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4345 3678 603 41 0 4304 0 vsize: 17380 [startup+1120.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3783 0 0 0 112002 11 0 0 25 0 1 0 423087806 18194432 3761 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4442 3761 603 41 0 4401 0 vsize: 17768 [startup+1130.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3788 0 0 0 113003 11 0 0 25 0 1 0 423087806 18194432 3766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4442 3766 603 41 0 4401 0 vsize: 17768 [startup+1140.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3789 0 0 0 114003 11 0 0 25 0 1 0 423087806 18194432 3767 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4442 3767 603 41 0 4401 0 vsize: 17768 [startup+1150.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3801 0 0 0 115003 11 0 0 25 0 1 0 423087806 18345984 3779 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4479 3779 603 41 0 4438 0 vsize: 17916 [startup+1160.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3832 0 0 0 116003 11 0 0 25 0 1 0 423087806 18493440 3810 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4515 3810 603 41 0 4474 0 vsize: 18060 [startup+1170.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3832 0 0 0 117003 11 0 0 25 0 1 0 423087806 18493440 3810 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4515 3810 603 41 0 4474 0 vsize: 18060 [startup+1180.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3832 0 0 0 118003 11 0 0 25 0 1 0 423087806 18493440 3810 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4515 3810 603 41 0 4474 0 vsize: 18060 [startup+1190.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3842 0 0 0 119003 12 0 0 25 0 1 0 423087806 18493440 3820 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4515 3820 603 41 0 4474 0 vsize: 18060 [startup+1200.01 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 26245 Raw data (stat): 26245 (minisat+) R 26244 20937 20936 0 -1 0 3859 0 0 0 120004 12 0 0 25 0 1 0 423087806 18657280 3837 4294967295 134512640 134672761 3221224544 3221223648 134559958 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4555 3837 603 41 0 4514 0 vsize: 18220 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.02 s] Raw data (loadavg): 0.99 0.98 0.92 1/54 26245 Raw data (stat): 26245 (minisat+) Z 26244 20937 20936 0 -1 12 3861 0 0 0 120004 13 0 0 25 0 1 0 423087806 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.02 CPU time (s): 1200.17 CPU user time (s): 1200.04 CPU system time (s): 0.13098 CPU usage (%): 100.012 Max. virtual memory (Kb): 18220 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####