Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga40_38_sat_pb.cnf.cr.opb |
MD5SUM | 69d239b72e8d1a72f9c55329043493e1 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
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 | 41 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 15.9626 |
Number of variables | 2280 |
Total number of constraints | 1636 |
Number of constraints which are clauses | 1558 |
Number of constraints which are cardinality constraints (but not clauses) | 78 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 40 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-04-13 20:25:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=464 boxname=wulflinc4 idbench=52 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 69d239b72e8d1a72f9c55329043493e1 /oldhome/oroussel/tmp/wulflinc4/normalized-fpga40_38_sat_pb.cnf.cr.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc4/normalized-fpga40_38_sat_pb.cnf.cr.opb IDLAUNCH: 464 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 927788 kB Buffers: 34292 kB Cached: 52952 kB SwapCached: 0 kB Active: 50516 kB Inactive: 39604 kB HighTotal: 131008 kB HighFree: 74284 kB LowTotal: 903652 kB LowFree: 853504 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6920 kB Slab: 11196 kB Committed_AS: 71676 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 20:45:22 (client local time) WITH STATUS 0 IN 1200.2 SECONDS stats: 464 7 1200.2 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 1636 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[ 77]---> BDD-cost: 73 c ---[ 76]---> BDD-cost: 73 c ---[ 75]---> BDD-cost: 73 c ---[ 74]---> BDD-cost: 73 c ---[ 73]---> BDD-cost: 73 c ---[ 72]---> BDD-cost: 73 c ---[ 71]---> BDD-cost: 73 c ---[ 70]---> BDD-cost: 73 c ---[ 69]---> BDD-cost: 73 c ---[ 68]---> BDD-cost: 73 c ---[ 67]---> BDD-cost: 73 c ---[ 66]---> BDD-cost: 73 c ---[ 65]---> BDD-cost: 73 c ---[ 64]---> BDD-cost: 73 c ---[ 63]---> BDD-cost: 73 c ---[ 62]---> BDD-cost: 73 c ---[ 61]---> BDD-cost: 73 c ---[ 60]---> BDD-cost: 73 c ---[ 59]---> BDD-cost: 73 c ---[ 58]---> BDD-cost: 73 c ---[ 57]---> BDD-cost: 73 c ---[ 56]---> BDD-cost: 73 c ---[ 55]---> BDD-cost: 73 c ---[ 54]---> BDD-cost: 73 c ---[ 53]---> BDD-cost: 73 c ---[ 52]---> BDD-cost: 73 c ---[ 51]---> BDD-cost: 73 c ---[ 50]---> BDD-cost: 73 c ---[ 49]---> BDD-cost: 73 c ---[ 48]---> BDD-cost: 73 c ---[ 47]---> BDD-cost: 73 c ---[ 46]---> BDD-cost: 73 c ---[ 45]---> BDD-cost: 73 c ---[ 44]---> BDD-cost: 73 c ---[ 43]---> BDD-cost: 73 c ---[ 42]---> BDD-cost: 73 c ---[ 41]---> BDD-cost: 73 c ---[ 40]---> BDD-cost: 73 c ---[ 39]---> BDD-cost: 73 c ---[ 38]---> BDD-cost: 73 c ---[ 37]---> BDD-cost: 37 c ---[ 36]---> BDD-cost: 37 c ---[ 35]---> BDD-cost: 37 c ---[ 34]---> BDD-cost: 37 c ---[ 33]---> BDD-cost: 37 c ---[ 32]---> BDD-cost: 37 c ---[ 31]---> BDD-cost: 37 c ---[ 30]---> BDD-cost: 37 c ---[ 29]---> BDD-cost: 37 c ---[ 28]---> BDD-cost: 37 c ---[ 27]---> BDD-cost: 37 c ---[ 26]---> BDD-cost: 37 c ---[ 25]---> BDD-cost: 37 c ---[ 24]---> BDD-cost: 37 c ---[ 23]---> BDD-cost: 37 c ---[ 22]---> BDD-cost: 37 c ---[ 21]---> BDD-cost: 37 c ---[ 20]---> BDD-cost: 37 c ---[ 19]---> BDD-cost: 37 c ---[ 18]---> BDD-cost: 37 c ---[ 17]---> BDD-cost: 37 c ---[ 16]---> BDD-cost: 37 c ---[ 15]---> BDD-cost: 37 c ---[ 14]---> BDD-cost: 37 c ---[ 13]---> BDD-cost: 37 c ---[ 12]---> BDD-cost: 37 c ---[ 11]---> BDD-cost: 37 c ---[ 10]---> BDD-cost: 37 c ---[ 9]---> BDD-cost: 37 c ---[ 8]---> BDD-cost: 37 c ---[ 7]---> BDD-cost: 37 c ---[ 6]---> BDD-cost: 37 c ---[ 5]---> BDD-cost: 37 c ---[ 4]---> BDD-cost: 37 c ---[ 3]---> BDD-cost: 37 c ---[ 2]---> BDD-cost: 37 c ---[ 1]---> BDD-cost: 37 c ---[ 0]---> BDD-cost: 37 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 12256 59766 | 4085 0 0 nan | 0.000 % | c | 103 | 12256 59766 | 4493 103 23189 225.1 | 1.181 % | c | 253 | 12256 59766 | 4942 253 33793 133.6 | 1.181 % | c | 480 | 12256 59766 | 5437 480 75308 156.9 | 1.181 % | c | 817 | 12256 59766 | 5980 817 169756 207.8 | 1.181 % | c | 1323 | 12256 59766 | 6578 1323 266622 201.5 | 1.181 % | c | 2082 | 12256 59766 | 7236 2082 346944 166.6 | 1.181 % | c | 3221 | 12256 59766 | 7960 3221 672994 208.9 | 1.181 % | c | 4933 | 12256 59766 | 8756 4933 891745 180.8 | 1.181 % | c | 7495 | 12256 59766 | 9632 7495 1795103 239.5 | 1.181 % | c | 11340 | 12256 59766 | 10595 11340 2331890 205.6 | 1.181 % | c | 17107 | 12256 59766 | 11654 11437 3336088 291.7 | 1.181 % | c | 25760 | 12256 59766 | 12820 12101 3971454 328.2 | 1.181 % | c | 38736 | 12256 59766 | 14102 16761 4472808 266.9 | 1.181 % | c | 58201 | 12256 59766 | 15512 18480 7868227 425.8 | 1.181 % | c | 87394 | 12256 59766 | 17064 17668 2277590 128.9 | 1.181 % | c | 131184 | 12256 59766 | 18770 21073 9678978 459.3 | 1.181 % | c | 196873 | 12256 59766 | 20647 20482 7435518 363.0 | 1.181 % | c | 295403 | 12256 59766 | 22712 24813 4118111 166.0 | 1.181 % | #### 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.57 0.87 0.87 2/54 8173 Raw data (stat): 8173 (runsolver) R 8172 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420588316 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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+10.0003 s] Raw data (loadavg): 0.64 0.87 0.87 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 3015 0 0 0 991 7 0 0 25 0 1 0 420588316 13971456 2993 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3411 2993 603 41 0 3370 0 vsize: 13644 [startup+20.0015 s] Raw data (loadavg): 0.69 0.87 0.87 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 3465 0 0 0 1988 9 0 0 25 0 1 0 420588316 15728640 3443 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3840 3443 603 41 0 3799 0 vsize: 15360 [startup+30.0029 s] Raw data (loadavg): 0.74 0.88 0.87 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 4910 0 0 0 2985 13 0 0 25 0 1 0 420588316 21667840 4888 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5290 4888 603 41 0 5249 0 vsize: 21160 [startup+40.0026 s] Raw data (loadavg): 0.78 0.88 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 5951 0 0 0 3982 15 0 0 25 0 1 0 420588316 26001408 5929 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6348 5929 603 41 0 6307 0 vsize: 25392 [startup+50.0031 s] Raw data (loadavg): 0.81 0.89 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 5954 0 0 0 4982 15 0 0 25 0 1 0 420588316 26001408 5932 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6348 5932 603 41 0 6307 0 vsize: 25392 [startup+60.0035 s] Raw data (loadavg): 0.84 0.89 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 5955 0 0 0 5982 15 0 0 25 0 1 0 420588316 26001408 5933 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6348 5933 603 41 0 6307 0 vsize: 25392 [startup+70.0043 s] Raw data (loadavg): 0.87 0.89 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 6726 0 0 0 6978 18 0 0 25 0 1 0 420588316 29265920 6704 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7145 6704 603 41 0 7104 0 vsize: 28580 [startup+80.0046 s] Raw data (loadavg): 0.89 0.89 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 6726 0 0 0 7978 18 0 0 25 0 1 0 420588316 29265920 6704 4294967295 134512640 134672761 3221224624 3221223728 134560492 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7145 6704 603 41 0 7104 0 vsize: 28580 [startup+90.0048 s] Raw data (loadavg): 0.90 0.90 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 6726 0 0 0 8978 18 0 0 25 0 1 0 420588316 29265920 6704 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7145 6704 603 41 0 7104 0 vsize: 28580 [startup+100.006 s] Raw data (loadavg): 0.92 0.90 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 6726 0 0 0 9978 18 0 0 25 0 1 0 420588316 29265920 6704 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7145 6704 603 41 0 7104 0 vsize: 28580 [startup+110.006 s] Raw data (loadavg): 0.93 0.90 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 7358 0 0 0 10976 20 0 0 25 0 1 0 420588316 31834112 7336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7772 7336 603 41 0 7731 0 vsize: 31088 [startup+120.007 s] Raw data (loadavg): 0.94 0.91 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 7358 0 0 0 11977 20 0 0 25 0 1 0 420588316 31834112 7336 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7772 7336 603 41 0 7731 0 vsize: 31088 [startup+130.008 s] Raw data (loadavg): 0.95 0.91 0.88 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 7358 0 0 0 12977 20 0 0 25 0 1 0 420588316 31834112 7336 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7772 7336 603 41 0 7731 0 vsize: 31088 [startup+140.008 s] Raw data (loadavg): 0.96 0.91 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 7358 0 0 0 13977 20 0 0 25 0 1 0 420588316 31834112 7336 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7772 7336 603 41 0 7731 0 vsize: 31088 [startup+150.009 s] Raw data (loadavg): 0.96 0.91 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 7581 0 0 0 14976 21 0 0 25 0 1 0 420588316 32669696 7559 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7976 7559 603 41 0 7935 0 vsize: 31904 [startup+160.009 s] Raw data (loadavg): 0.97 0.92 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 8163 0 0 0 15975 23 0 0 25 0 1 0 420588316 35094528 8141 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8568 8141 603 41 0 8527 0 vsize: 34272 [startup+170.009 s] Raw data (loadavg): 0.97 0.92 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 8756 0 0 0 16973 25 0 0 25 0 1 0 420588316 37527552 8734 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9162 8734 603 41 0 9121 0 vsize: 36648 [startup+180.01 s] Raw data (loadavg): 0.98 0.92 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9367 0 0 0 17972 27 0 0 25 0 1 0 420588316 40099840 9345 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9790 9345 603 41 0 9749 0 vsize: 39160 [startup+190.01 s] Raw data (loadavg): 0.98 0.92 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9774 0 0 0 18970 28 0 0 25 0 1 0 420588316 41738240 9752 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10190 9752 603 41 0 10149 0 vsize: 40760 [startup+200.01 s] Raw data (loadavg): 0.98 0.92 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 19969 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+210.01 s] Raw data (loadavg): 0.98 0.93 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 20969 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+220.011 s] Raw data (loadavg): 0.99 0.93 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 21970 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+230.01 s] Raw data (loadavg): 0.99 0.93 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 22970 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+240.011 s] Raw data (loadavg): 0.99 0.93 0.89 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 23970 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+250.012 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 24970 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+260.012 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 25970 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+270.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 26971 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+280.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 27971 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+290.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9776 0 0 0 28971 29 0 0 25 0 1 0 420588316 41738240 9754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9754 603 41 0 10149 0 vsize: 40760 [startup+300.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9777 0 0 0 29971 29 0 0 25 0 1 0 420588316 41738240 9755 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9755 603 41 0 10149 0 vsize: 40760 [startup+310.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9777 0 0 0 30971 29 0 0 25 0 1 0 420588316 41738240 9755 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9755 603 41 0 10149 0 vsize: 40760 [startup+320.013 s] Raw data (loadavg): 0.99 0.94 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9777 0 0 0 31971 29 0 0 25 0 1 0 420588316 41738240 9755 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10190 9755 603 41 0 10149 0 vsize: 40760 [startup+330.014 s] Raw data (loadavg): 0.99 0.95 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 9843 0 0 0 32971 29 0 0 25 0 1 0 420588316 42139648 9821 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10288 9821 603 41 0 10247 0 vsize: 41152 [startup+340.014 s] Raw data (loadavg): 0.99 0.95 0.90 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 10207 0 0 0 33970 30 0 0 25 0 1 0 420588316 43659264 10185 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10659 10185 603 41 0 10618 0 vsize: 42636 [startup+350.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 10659 0 0 0 34969 31 0 0 25 0 1 0 420588316 45400064 10637 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11084 10637 603 41 0 11043 0 vsize: 44336 [startup+360.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 11139 0 0 0 35968 33 0 0 25 0 1 0 420588316 47525888 11117 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11603 11117 603 41 0 11562 0 vsize: 46412 [startup+370.016 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 11719 0 0 0 36966 35 0 0 25 0 1 0 420588316 49811456 11697 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12161 11697 603 41 0 12120 0 vsize: 48644 [startup+380.016 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12131 0 0 0 37965 36 0 0 25 0 1 0 420588316 51580928 12109 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12593 12109 603 41 0 12552 0 vsize: 50372 [startup+390.016 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12394 0 0 0 38964 37 0 0 25 0 1 0 420588316 52662272 12372 4294967295 134512640 134672761 3221224624 3221223728 134559998 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12857 12372 603 41 0 12816 0 vsize: 51428 [startup+400.017 s] Raw data (loadavg): 1.07 0.97 0.91 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12394 0 0 0 39965 37 0 0 25 0 1 0 420588316 52662272 12372 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12857 12372 603 41 0 12816 0 vsize: 51428 [startup+410.017 s] Raw data (loadavg): 1.14 0.99 0.92 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12394 0 0 0 40965 37 0 0 25 0 1 0 420588316 52662272 12372 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12857 12372 603 41 0 12816 0 vsize: 51428 [startup+420.018 s] Raw data (loadavg): 1.11 0.99 0.92 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12394 0 0 0 41965 37 0 0 25 0 1 0 420588316 52662272 12372 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12857 12372 603 41 0 12816 0 vsize: 51428 [startup+430.019 s] Raw data (loadavg): 1.10 0.99 0.92 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12664 0 0 0 42965 38 0 0 25 0 1 0 420588316 53743616 12642 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13121 12642 603 41 0 13080 0 vsize: 52484 [startup+440.018 s] Raw data (loadavg): 1.08 0.99 0.92 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12766 0 0 0 43965 38 0 0 25 0 1 0 420588316 54149120 12744 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13220 12744 603 41 0 13179 0 vsize: 52880 [startup+450.019 s] Raw data (loadavg): 1.07 0.99 0.92 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12766 0 0 0 44965 38 0 0 25 0 1 0 420588316 54149120 12744 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13220 12744 603 41 0 13179 0 vsize: 52880 [startup+460.019 s] Raw data (loadavg): 1.06 0.99 0.92 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12766 0 0 0 45965 38 0 0 25 0 1 0 420588316 54149120 12744 4294967295 134512640 134672761 3221224624 3221223728 134559943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13220 12744 603 41 0 13179 0 vsize: 52880 [startup+470.02 s] Raw data (loadavg): 1.05 0.99 0.92 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12766 0 0 0 46965 38 0 0 25 0 1 0 420588316 54149120 12744 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13220 12744 603 41 0 13179 0 vsize: 52880 [startup+480.021 s] Raw data (loadavg): 1.04 0.99 0.92 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12775 0 0 0 47965 38 0 0 25 0 1 0 420588316 54284288 12753 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13253 12753 603 41 0 13212 0 vsize: 53012 [startup+490.02 s] Raw data (loadavg): 1.11 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12775 0 0 0 48965 38 0 0 25 0 1 0 420588316 54284288 12753 4294967295 134512640 134672761 3221224624 3221223808 134559609 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13253 12753 603 41 0 13212 0 vsize: 53012 [startup+500.021 s] Raw data (loadavg): 1.17 1.02 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12775 0 0 0 49965 38 0 0 25 0 1 0 420588316 54284288 12753 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13253 12753 603 41 0 13212 0 vsize: 53012 [startup+510.021 s] Raw data (loadavg): 1.14 1.02 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12775 0 0 0 50965 38 0 0 25 0 1 0 420588316 54284288 12753 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13253 12753 603 41 0 13212 0 vsize: 53012 [startup+520.022 s] Raw data (loadavg): 1.12 1.02 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 51965 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+530.022 s] Raw data (loadavg): 1.10 1.02 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 52965 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+540.022 s] Raw data (loadavg): 1.08 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 53966 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+550.023 s] Raw data (loadavg): 1.07 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 54966 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+560.023 s] Raw data (loadavg): 1.06 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 55966 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+570.024 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 56966 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+580.025 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 57966 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+590.024 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 58967 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+600.025 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 59967 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223728 134560355 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+610.025 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 60967 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+620.026 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 61967 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+630.026 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 62967 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+640.027 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 63968 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+650.027 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 64968 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+660.028 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 65968 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+670.028 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 66968 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+680.029 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 67969 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+690.029 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 68969 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+700.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 69969 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+710.029 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 70969 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+720.031 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 71969 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+730.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 72970 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+740.031 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 73970 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223808 134558903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+750.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 74970 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+760.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 75970 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+770.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 76970 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+780.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 77971 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+790.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 78971 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+800.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12776 0 0 0 79971 38 0 0 25 0 1 0 420588316 54276096 12754 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12754 603 41 0 13210 0 vsize: 53004 [startup+810.034 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12778 0 0 0 80970 38 0 0 25 0 1 0 420588316 54276096 12756 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13251 12756 603 41 0 13210 0 vsize: 53004 [startup+820.035 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12778 0 0 0 81970 38 0 0 25 0 1 0 420588316 54276096 12756 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12756 603 41 0 13210 0 vsize: 53004 [startup+830.036 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12778 0 0 0 82970 38 0 0 25 0 1 0 420588316 54276096 12756 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12756 603 41 0 13210 0 vsize: 53004 [startup+840.036 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 83970 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+850.036 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 84970 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+860.036 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 85970 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+870.038 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 86970 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+880.038 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 87971 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+890.038 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 88971 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+900.038 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 89971 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+910.039 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 90971 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+920.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 91972 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+930.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 92972 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223728 134560477 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+940.041 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 93972 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+950.041 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 94972 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+960.041 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 95972 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+970.041 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 96972 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+980.042 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 97973 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223728 134560010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+990.042 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 98973 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1000.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 99973 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1010.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 100973 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1020.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 101973 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1030.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 102974 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1040.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 103974 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1050.05 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 104974 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223808 134559489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1060.05 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 105974 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1070.05 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 106974 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1080.05 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 107975 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1090.05 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 108975 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1100.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 109975 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1110.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 12779 0 0 0 110976 38 0 0 25 0 1 0 420588316 54276096 12757 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13251 12757 603 41 0 13210 0 vsize: 53004 [startup+1120.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 13405 0 0 0 111974 41 0 0 25 0 1 0 420588316 56877056 13383 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13886 13383 603 41 0 13845 0 vsize: 55544 [startup+1130.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 13733 0 0 0 112973 42 0 0 25 0 1 0 420588316 58228736 13711 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14216 13711 603 41 0 14175 0 vsize: 56864 [startup+1140.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 13733 0 0 0 113973 42 0 0 25 0 1 0 420588316 58228736 13711 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14216 13711 603 41 0 14175 0 vsize: 56864 [startup+1150.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 13733 0 0 0 114973 42 0 0 25 0 1 0 420588316 58228736 13711 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14216 13711 603 41 0 14175 0 vsize: 56864 [startup+1160.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 13733 0 0 0 115973 42 0 0 25 0 1 0 420588316 58228736 13711 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14216 13711 603 41 0 14175 0 vsize: 56864 [startup+1170.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 13765 0 0 0 116974 42 0 0 25 0 1 0 420588316 58363904 13743 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14249 13743 603 41 0 14208 0 vsize: 56996 [startup+1180.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 14423 0 0 0 117972 43 0 0 25 0 1 0 420588316 61116416 14401 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14921 14401 603 41 0 14880 0 vsize: 59684 [startup+1190.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 15178 0 0 0 118970 45 0 0 25 0 1 0 420588316 64253952 15156 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15687 15156 603 41 0 15646 0 vsize: 62748 [startup+1200.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 8173 Raw data (stat): 8173 (minisat+) R 8172 5897 5896 0 -1 0 15623 0 0 0 119969 46 0 0 25 0 1 0 420588316 66035712 15601 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16122 15601 603 41 0 16081 0 vsize: 64488 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.09 s] Raw data (loadavg): 1.00 1.00 0.93 1/54 8173 Raw data (stat): 8173 (minisat+) Z 8172 5897 5896 0 -1 12 15625 0 0 0 119969 49 0 0 25 0 1 0 420588316 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.09 CPU time (s): 1200.2 CPU user time (s): 1199.7 CPU system time (s): 0.499924 CPU usage (%): 100.009 Max. virtual memory (Kb): 64488 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####