Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl50_51_pb.cnf.cr.opb |
MD5SUM | 00bdc6bb9bafd4b1100d8bfa4f886626 |
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 | 52 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.156976 |
Number of variables | 5100 |
Total number of constraints | 202 |
Number of constraints which are clauses | 102 |
Number of constraints which are cardinality constraints (but not clauses) | 100 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 50 |
Maximum length of a constraint | 51 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc23 THE 2005-04-13 20:23:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=176 boxname=wulflinc23 idbench=20 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 00bdc6bb9bafd4b1100d8bfa4f886626 /oldhome/oroussel/tmp/wulflinc23/normalized-chnl50_51_pb.cnf.cr.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc23/normalized-chnl50_51_pb.cnf.cr.opb IDLAUNCH: 176 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 3 cpu MHz : 451.037 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: 912032 kB Buffers: 33920 kB Cached: 46128 kB SwapCached: 192 kB Active: 45476 kB Inactive: 37644 kB HighTotal: 131008 kB HighFree: 81004 kB LowTotal: 903652 kB LowFree: 831028 kB SwapTotal: 2097136 kB SwapFree: 2096944 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6908 kB Slab: 34056 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 20:43:23 (client local time) WITH STATUS 0 IN 1200.25 SECONDS stats: 176 7 1200.25 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 202 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ...................................................................................................... c ---[ 99]---> BDD-cost: 99 c ---[ 98]---> BDD-cost: 99 c ---[ 97]---> BDD-cost: 99 c ---[ 96]---> BDD-cost: 99 c ---[ 95]---> BDD-cost: 99 c ---[ 94]---> BDD-cost: 99 c ---[ 93]---> BDD-cost: 99 c ---[ 92]---> BDD-cost: 99 c ---[ 91]---> BDD-cost: 99 c ---[ 90]---> BDD-cost: 99 c ---[ 89]---> BDD-cost: 99 c ---[ 88]---> BDD-cost: 99 c ---[ 87]---> BDD-cost: 99 c ---[ 86]---> BDD-cost: 99 c ---[ 85]---> BDD-cost: 99 c ---[ 84]---> BDD-cost: 99 c ---[ 83]---> BDD-cost: 99 c ---[ 82]---> BDD-cost: 99 c ---[ 81]---> BDD-cost: 99 c ---[ 80]---> BDD-cost: 99 c ---[ 79]---> BDD-cost: 99 c ---[ 78]---> BDD-cost: 99 c ---[ 77]---> BDD-cost: 99 c ---[ 76]---> BDD-cost: 99 c ---[ 75]---> BDD-cost: 99 c ---[ 74]---> BDD-cost: 99 c ---[ 73]---> BDD-cost: 99 c ---[ 72]---> BDD-cost: 99 c ---[ 71]---> BDD-cost: 99 c ---[ 70]---> BDD-cost: 99 c ---[ 69]---> BDD-cost: 99 c ---[ 68]---> BDD-cost: 99 c ---[ 67]---> BDD-cost: 99 c ---[ 66]---> BDD-cost: 99 c ---[ 65]---> BDD-cost: 99 c ---[ 64]---> BDD-cost: 99 c ---[ 63]---> BDD-cost: 99 c ---[ 62]---> BDD-cost: 99 c ---[ 61]---> BDD-cost: 99 c ---[ 60]---> BDD-cost: 99 c ---[ 59]---> BDD-cost: 99 c ---[ 58]---> BDD-cost: 99 c ---[ 57]---> BDD-cost: 99 c ---[ 56]---> BDD-cost: 99 c ---[ 55]---> BDD-cost: 99 c ---[ 54]---> BDD-cost: 99 c ---[ 53]---> BDD-cost: 99 c ---[ 52]---> BDD-cost: 99 c ---[ 51]---> BDD-cost: 99 c ---[ 50]---> BDD-cost: 99 c ---[ 49]---> BDD-cost: 99 c ---[ 48]---> BDD-cost: 99 c ---[ 47]---> BDD-cost: 99 c ---[ 46]---> BDD-cost: 99 c ---[ 45]---> BDD-cost: 99 c ---[ 44]---> BDD-cost: 99 c ---[ 43]---> BDD-cost: 99 c ---[ 42]---> BDD-cost: 99 c ---[ 41]---> BDD-cost: 99 c ---[ 40]---> BDD-cost: 99 c ---[ 39]---> BDD-cost: 99 c ---[ 38]---> BDD-cost: 99 c ---[ 37]---> BDD-cost: 99 c ---[ 36]---> BDD-cost: 99 c ---[ 35]---> BDD-cost: 99 c ---[ 34]---> BDD-cost: 99 c ---[ 33]---> BDD-cost: 99 c ---[ 32]---> BDD-cost: 99 c ---[ 31]---> BDD-cost: 99 c ---[ 30]---> BDD-cost: 99 c ---[ 29]---> BDD-cost: 99 c ---[ 28]---> BDD-cost: 99 c ---[ 27]---> BDD-cost: 99 c ---[ 26]---> BDD-cost: 99 c ---[ 25]---> BDD-cost: 99 c ---[ 24]---> BDD-cost: 99 c ---[ 23]---> BDD-cost: 99 c ---[ 22]---> BDD-cost: 99 c ---[ 21]---> BDD-cost: 99 c ---[ 20]---> BDD-cost: 99 c ---[ 19]---> BDD-cost: 99 c ---[ 18]---> BDD-cost: 99 c ---[ 17]---> BDD-cost: 99 c ---[ 16]---> BDD-cost: 99 c ---[ 15]---> BDD-cost: 99 c ---[ 14]---> BDD-cost: 99 c ---[ 13]---> BDD-cost: 99 c ---[ 12]---> BDD-cost: 99 c ---[ 11]---> BDD-cost: 99 c ---[ 10]---> BDD-cost: 99 c ---[ 9]---> BDD-cost: 99 c ---[ 8]---> BDD-cost: 99 c ---[ 7]---> BDD-cost: 99 c ---[ 6]---> BDD-cost: 99 c ---[ 5]---> BDD-cost: 99 c ---[ 4]---> BDD-cost: 99 c ---[ 3]---> BDD-cost: 99 c ---[ 2]---> BDD-cost: 99 c ---[ 1]---> BDD-cost: 99 c ---[ 0]---> BDD-cost: 99 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 24702 69100 | 8234 0 0 nan | 0.000 % | c | 103 | 24702 69100 | 9057 103 21251 206.3 | 0.667 % | c | 257 | 24702 69100 | 9963 257 49705 193.4 | 0.667 % | c | 483 | 24702 69100 | 10959 483 104379 216.1 | 0.667 % | c | 820 | 24702 69100 | 12055 820 161617 197.1 | 0.667 % | c | 1328 | 24702 69100 | 13260 1328 304812 229.5 | 0.667 % | c | 2087 | 24702 69100 | 14587 2087 499248 239.2 | 0.667 % | c | 3226 | 24702 69100 | 16045 3226 939931 291.4 | 0.667 % | c | 4934 | 24702 69100 | 17650 4934 1692679 343.1 | 0.667 % | c | 7497 | 24702 69100 | 19415 7497 2867483 382.5 | 0.667 % | c | 11345 | 24702 69100 | 21356 11345 4334050 382.0 | 0.667 % | c | 17113 | 24702 69100 | 23492 17113 7407340 432.8 | 0.667 % | c | 25762 | 24702 69100 | 25841 25762 11735963 455.6 | 0.667 % | c | 38736 | 24702 69100 | 28426 19007 8582103 451.5 | 0.667 % | c | 58197 | 24702 69100 | 31268 16084 9622847 598.3 | 0.667 % | c | 87391 | 24702 69100 | 34395 15805 8643661 546.9 | 0.667 % | c | 131182 | 24702 69100 | 37835 29400 20102392 683.8 | 0.667 % | #### 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.97 0.91 2/54 4870 Raw data (stat): 4870 (runsolver) R 4869 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478800321 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 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 3414 0 0 0 991 7 0 0 25 0 1 0 478800321 15720448 3389 4294967295 134512640 134672761 3221224624 3221223640 1075353072 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3838 3389 603 41 0 3797 0 vsize: 15352 [startup+20.0009 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 5196 0 0 0 1986 11 0 0 25 0 1 0 478800321 23015424 5171 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5619 5171 603 41 0 5578 0 vsize: 22476 [startup+30.0015 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 6852 0 0 0 2983 16 0 0 25 0 1 0 478800321 29761536 6827 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7266 6827 603 41 0 7225 0 vsize: 29064 [startup+40.0009 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 8551 0 0 0 3979 20 0 0 25 0 1 0 478800321 36782080 8526 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8980 8526 603 41 0 8939 0 vsize: 35920 [startup+50.0016 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 10024 0 0 0 4975 23 0 0 25 0 1 0 478800321 42758144 9999 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10439 9999 603 41 0 10398 0 vsize: 41756 [startup+60.0015 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 11250 0 0 0 5973 26 0 0 25 0 1 0 478800321 47886336 11225 4294967295 134512640 134672761 3221224624 3221223808 134559385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11691 11225 603 41 0 11650 0 vsize: 46764 [startup+70.0021 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 12458 0 0 0 6970 29 0 0 25 0 1 0 478800321 52748288 12433 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12878 12433 603 41 0 12837 0 vsize: 51512 [startup+80.0025 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 13380 0 0 0 7968 32 0 0 25 0 1 0 478800321 56528896 13355 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13801 13355 603 41 0 13760 0 vsize: 55204 [startup+90.0024 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 14669 0 0 0 8963 36 0 0 25 0 1 0 478800321 61784064 14644 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15084 14644 603 41 0 15043 0 vsize: 60336 [startup+100.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 15746 0 0 0 9959 40 0 0 25 0 1 0 478800321 66244608 15721 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16173 15721 603 41 0 16132 0 vsize: 64692 [startup+110.002 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 10958 41 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+120.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 11958 41 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+130.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 12958 41 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+140.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 13957 42 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+150.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 14958 42 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+160.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 15958 42 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+170.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 16958 42 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+180.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 17958 42 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+190.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 18958 42 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+200.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16218 0 0 0 19958 42 0 0 25 0 1 0 478800321 68263936 16193 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16666 16193 603 41 0 16625 0 vsize: 66664 [startup+210.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16302 0 0 0 20958 43 0 0 25 0 1 0 478800321 68534272 16277 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16732 16277 603 41 0 16691 0 vsize: 66928 [startup+220.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 16997 0 0 0 21956 45 0 0 25 0 1 0 478800321 71372800 16972 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17425 16972 603 41 0 17384 0 vsize: 69700 [startup+230.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 17508 0 0 0 22955 46 0 0 25 0 1 0 478800321 73560064 17483 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17959 17483 603 41 0 17918 0 vsize: 71836 [startup+240.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 18003 0 0 0 23954 47 0 0 25 0 1 0 478800321 75587584 17978 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18454 17978 603 41 0 18413 0 vsize: 73816 [startup+250.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 18572 0 0 0 24952 49 0 0 25 0 1 0 478800321 78016512 18547 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19047 18547 603 41 0 19006 0 vsize: 76188 [startup+260.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 19308 0 0 0 25951 51 0 0 25 0 1 0 478800321 80990208 19283 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19773 19283 603 41 0 19732 0 vsize: 79092 [startup+270.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 19835 0 0 0 26949 53 0 0 25 0 1 0 478800321 83275776 19810 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20331 19810 603 41 0 20290 0 vsize: 81324 [startup+280.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20343 0 0 0 27948 54 0 0 25 0 1 0 478800321 85438464 20318 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20859 20318 603 41 0 20818 0 vsize: 83436 [startup+290.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20813 0 0 0 28946 56 0 0 25 0 1 0 478800321 87330816 20788 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21321 20788 603 41 0 21280 0 vsize: 85284 [startup+300.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20897 0 0 0 29946 56 0 0 25 0 1 0 478800321 87601152 20872 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21387 20872 603 41 0 21346 0 vsize: 85548 [startup+310.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20897 0 0 0 30947 56 0 0 25 0 1 0 478800321 87601152 20872 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21387 20872 603 41 0 21346 0 vsize: 85548 [startup+320.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20897 0 0 0 31947 56 0 0 25 0 1 0 478800321 87601152 20872 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21387 20872 603 41 0 21346 0 vsize: 85548 [startup+330.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20897 0 0 0 32947 56 0 0 25 0 1 0 478800321 87601152 20872 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21387 20872 603 41 0 21346 0 vsize: 85548 [startup+340.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20897 0 0 0 33947 56 0 0 25 0 1 0 478800321 87601152 20872 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21387 20872 603 41 0 21346 0 vsize: 85548 [startup+350.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20897 0 0 0 34947 56 0 0 25 0 1 0 478800321 87601152 20872 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21387 20872 603 41 0 21346 0 vsize: 85548 [startup+360.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20897 0 0 0 35947 56 0 0 25 0 1 0 478800321 87601152 20872 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21387 20872 603 41 0 21346 0 vsize: 85548 [startup+370.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 20897 0 0 0 36947 56 0 0 25 0 1 0 478800321 87601152 20872 4294967295 134512640 134672761 3221224624 3221223728 134560160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21387 20872 603 41 0 21346 0 vsize: 85548 [startup+380.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 21135 0 0 0 37946 57 0 0 25 0 1 0 478800321 88559616 21110 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21621 21110 603 41 0 21580 0 vsize: 86484 [startup+390.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 22233 0 0 0 38944 60 0 0 25 0 1 0 478800321 93155328 22208 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22743 22208 603 41 0 22702 0 vsize: 90972 [startup+400.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 23431 0 0 0 39942 63 0 0 25 0 1 0 478800321 98029568 23406 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23933 23406 603 41 0 23892 0 vsize: 95732 [startup+410.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 24469 0 0 0 40940 65 0 0 25 0 1 0 478800321 102383616 24444 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24996 24444 603 41 0 24955 0 vsize: 99984 [startup+420.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 25490 0 0 0 41938 67 0 0 25 0 1 0 478800321 106622976 25465 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26031 25465 603 41 0 25990 0 vsize: 104124 [startup+430.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 26382 0 0 0 42935 69 0 0 25 0 1 0 478800321 110194688 26357 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26903 26357 603 41 0 26862 0 vsize: 107612 [startup+440.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 27445 0 0 0 43932 73 0 0 25 0 1 0 478800321 114659328 27420 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27993 27420 603 41 0 27952 0 vsize: 111972 [startup+450.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28403 0 0 0 44931 74 0 0 25 0 1 0 478800321 118583296 28378 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28951 28378 603 41 0 28910 0 vsize: 115804 [startup+460.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28935 0 0 0 45930 76 0 0 25 0 1 0 478800321 120733696 28910 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28910 603 41 0 29435 0 vsize: 117904 [startup+470.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 46930 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+480.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 47929 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+490.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 48930 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+500.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 49930 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+510.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 50930 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+520.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 51930 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+530.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 52930 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+540.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 53931 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+550.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 54931 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+560.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 55931 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+570.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 56931 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+580.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 57931 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+590.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 58931 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+600.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 59931 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223728 134555114 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+610.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 60931 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+620.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 28937 0 0 0 61931 76 0 0 25 0 1 0 478800321 120733696 28912 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29476 28912 603 41 0 29435 0 vsize: 117904 [startup+630.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29256 0 0 0 62931 77 0 0 25 0 1 0 478800321 122081280 29231 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29805 29231 603 41 0 29764 0 vsize: 119220 [startup+640.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29599 0 0 0 63930 78 0 0 25 0 1 0 478800321 123432960 29574 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29574 603 41 0 30094 0 vsize: 120540 [startup+650.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 64930 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+660.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 65930 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+670.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 66930 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223728 134560136 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+680.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 67930 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+690.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 68931 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+700.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 69931 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223728 134560005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+710.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 70931 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223808 134559028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+720.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 71931 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223728 134559998 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+730.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 72931 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+740.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 73931 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+750.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 74931 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+760.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 29600 0 0 0 75931 78 0 0 25 0 1 0 478800321 123432960 29575 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30135 29575 603 41 0 30094 0 vsize: 120540 [startup+770.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 30257 0 0 0 76929 80 0 0 25 0 1 0 478800321 126132224 30232 4294967295 134512640 134672761 3221224624 3221223808 134559553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30794 30232 603 41 0 30753 0 vsize: 123176 [startup+780.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 31219 0 0 0 77927 83 0 0 25 0 1 0 478800321 130048000 31194 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31750 31194 603 41 0 31709 0 vsize: 127000 [startup+790.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 32093 0 0 0 78925 85 0 0 25 0 1 0 478800321 133697536 32068 4294967295 134512640 134672761 3221224624 3221223808 134558925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32641 32068 603 41 0 32600 0 vsize: 130564 [startup+800.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 32905 0 0 0 79924 86 0 0 25 0 1 0 478800321 136978432 32880 4294967295 134512640 134672761 3221224624 3221223728 134559814 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33442 32880 603 41 0 33401 0 vsize: 133768 [startup+810.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 33662 0 0 0 80922 88 0 0 25 0 1 0 478800321 140218368 33637 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34233 33637 603 41 0 34192 0 vsize: 136932 [startup+820.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 34403 0 0 0 81920 90 0 0 25 0 1 0 478800321 143245312 34378 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34972 34378 603 41 0 34931 0 vsize: 139888 [startup+830.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35089 0 0 0 82918 92 0 0 25 0 1 0 478800321 146104320 35064 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35064 603 41 0 35629 0 vsize: 142680 [startup+840.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35090 0 0 0 83918 92 0 0 25 0 1 0 478800321 146104320 35065 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35065 603 41 0 35629 0 vsize: 142680 [startup+850.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35090 0 0 0 84919 92 0 0 25 0 1 0 478800321 146104320 35065 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35065 603 41 0 35629 0 vsize: 142680 [startup+860.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35091 0 0 0 85919 92 0 0 25 0 1 0 478800321 146104320 35066 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35066 603 41 0 35629 0 vsize: 142680 [startup+870.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35091 0 0 0 86919 92 0 0 25 0 1 0 478800321 146104320 35066 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35066 603 41 0 35629 0 vsize: 142680 [startup+880.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35096 0 0 0 87919 92 0 0 25 0 1 0 478800321 146104320 35071 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35071 603 41 0 35629 0 vsize: 142680 [startup+890.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35100 0 0 0 88919 92 0 0 25 0 1 0 478800321 146104320 35075 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35075 603 41 0 35629 0 vsize: 142680 [startup+900.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35101 0 0 0 89919 92 0 0 25 0 1 0 478800321 146104320 35076 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35076 603 41 0 35629 0 vsize: 142680 [startup+910.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35101 0 0 0 90920 92 0 0 25 0 1 0 478800321 146104320 35076 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35076 603 41 0 35629 0 vsize: 142680 [startup+920.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35101 0 0 0 91920 92 0 0 25 0 1 0 478800321 146104320 35076 4294967295 134512640 134672761 3221224624 3221223728 134560148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35076 603 41 0 35629 0 vsize: 142680 [startup+930.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35105 0 0 0 92920 92 0 0 25 0 1 0 478800321 146104320 35080 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35080 603 41 0 35629 0 vsize: 142680 [startup+940.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35106 0 0 0 93920 92 0 0 25 0 1 0 478800321 146104320 35081 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35081 603 41 0 35629 0 vsize: 142680 [startup+950.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35109 0 0 0 94920 92 0 0 25 0 1 0 478800321 146104320 35084 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35084 603 41 0 35629 0 vsize: 142680 [startup+960.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35109 0 0 0 95920 92 0 0 25 0 1 0 478800321 146104320 35084 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35084 603 41 0 35629 0 vsize: 142680 [startup+970.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35113 0 0 0 96921 92 0 0 25 0 1 0 478800321 146104320 35088 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35088 603 41 0 35629 0 vsize: 142680 [startup+980.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35115 0 0 0 97921 92 0 0 25 0 1 0 478800321 146104320 35090 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35090 603 41 0 35629 0 vsize: 142680 [startup+990.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35119 0 0 0 98921 92 0 0 25 0 1 0 478800321 146104320 35094 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35094 603 41 0 35629 0 vsize: 142680 [startup+1000.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35120 0 0 0 99921 92 0 0 25 0 1 0 478800321 146104320 35095 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35095 603 41 0 35629 0 vsize: 142680 [startup+1010.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35121 0 0 0 100921 92 0 0 25 0 1 0 478800321 146104320 35096 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35096 603 41 0 35629 0 vsize: 142680 [startup+1020.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35125 0 0 0 101922 92 0 0 25 0 1 0 478800321 146104320 35100 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35100 603 41 0 35629 0 vsize: 142680 [startup+1030.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35125 0 0 0 102922 92 0 0 25 0 1 0 478800321 146104320 35100 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35100 603 41 0 35629 0 vsize: 142680 [startup+1040.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35125 0 0 0 103922 92 0 0 25 0 1 0 478800321 146104320 35100 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35100 603 41 0 35629 0 vsize: 142680 [startup+1050.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35125 0 0 0 104922 92 0 0 25 0 1 0 478800321 146104320 35100 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35100 603 41 0 35629 0 vsize: 142680 [startup+1060.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35126 0 0 0 105922 92 0 0 25 0 1 0 478800321 146104320 35101 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35101 603 41 0 35629 0 vsize: 142680 [startup+1070.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35126 0 0 0 106922 92 0 0 25 0 1 0 478800321 146104320 35101 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35101 603 41 0 35629 0 vsize: 142680 [startup+1080.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35126 0 0 0 107922 92 0 0 25 0 1 0 478800321 146104320 35101 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35101 603 41 0 35629 0 vsize: 142680 [startup+1090.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35126 0 0 0 108923 92 0 0 25 0 1 0 478800321 146104320 35101 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35101 603 41 0 35629 0 vsize: 142680 [startup+1100.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35126 0 0 0 109923 92 0 0 25 0 1 0 478800321 146104320 35101 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35101 603 41 0 35629 0 vsize: 142680 [startup+1110.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35126 0 0 0 110923 92 0 0 25 0 1 0 478800321 146104320 35101 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35101 603 41 0 35629 0 vsize: 142680 [startup+1120.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35133 0 0 0 111923 93 0 0 25 0 1 0 478800321 146104320 35108 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35108 603 41 0 35629 0 vsize: 142680 [startup+1130.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35133 0 0 0 112923 93 0 0 25 0 1 0 478800321 146104320 35108 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35108 603 41 0 35629 0 vsize: 142680 [startup+1140.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35134 0 0 0 113923 93 0 0 25 0 1 0 478800321 146104320 35109 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35109 603 41 0 35629 0 vsize: 142680 [startup+1150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35134 0 0 0 114924 93 0 0 25 0 1 0 478800321 146104320 35109 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35109 603 41 0 35629 0 vsize: 142680 [startup+1160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35135 0 0 0 115924 93 0 0 25 0 1 0 478800321 146104320 35110 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35110 603 41 0 35629 0 vsize: 142680 [startup+1170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35135 0 0 0 116924 93 0 0 25 0 1 0 478800321 146104320 35110 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35110 603 41 0 35629 0 vsize: 142680 [startup+1180.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35135 0 0 0 117924 93 0 0 25 0 1 0 478800321 146104320 35110 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35110 603 41 0 35629 0 vsize: 142680 [startup+1190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35135 0 0 0 118924 93 0 0 25 0 1 0 478800321 146104320 35110 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35110 603 41 0 35629 0 vsize: 142680 [startup+1200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 4870 Raw data (stat): 4870 (minisat+) R 4869 3260 3259 0 -1 0 35135 0 0 0 119924 93 0 0 25 0 1 0 478800321 146104320 35110 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35670 35110 603 41 0 35629 0 vsize: 142680 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 4870 Raw data (stat): 4870 (minisat+) Z 4869 3260 3259 0 -1 12 35137 0 0 0 119925 99 0 0 23 0 1 0 478800321 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.1 CPU time (s): 1200.25 CPU user time (s): 1199.25 CPU system time (s): 0.995848 CPU usage (%): 100.012 Max. virtual memory (Kb): 142680 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####