Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl40_41_pb.cnf.cr.opb |
MD5SUM | 3c9e81ddaaf37dd621fe2bc839a3f27f |
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 | 42 |
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.098984 |
Number of variables | 3280 |
Total number of constraints | 162 |
Number of constraints which are clauses | 82 |
Number of constraints which are cardinality constraints (but not clauses) | 80 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 40 |
Maximum length of a constraint | 41 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc19 THE 2005-04-14 03:31:10 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4529 boxname=wulflinc19 idbench=17 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3c9e81ddaaf37dd621fe2bc839a3f27f /oldhome/oroussel/tmp/wulflinc19/normalized-chnl40_41_pb.cnf.cr.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc19/normalized-chnl40_41_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc19/normalized-chnl40_41_pb.cnf.cr.opb IDLAUNCH: 4529 /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: 876000 kB Buffers: 35452 kB Cached: 89272 kB SwapCached: 56 kB Active: 49860 kB Inactive: 77884 kB HighTotal: 131008 kB HighFree: 37604 kB LowTotal: 903652 kB LowFree: 838396 kB SwapTotal: 2097892 kB SwapFree: 2097836 kB Dirty: 28 kB Writeback: 0 kB Mapped: 7028 kB Slab: 25300 kB Committed_AS: 63708 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 03:51:12 (client local time) WITH STATUS 0 IN 1200.23 SECONDS stats: 4529 7 1200.23 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 162 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................. c ---[ 79]---> BDD-cost: 79 c ---[ 78]---> BDD-cost: 79 c ---[ 77]---> BDD-cost: 79 c ---[ 76]---> BDD-cost: 79 c ---[ 75]---> BDD-cost: 79 c ---[ 74]---> BDD-cost: 79 c ---[ 73]---> BDD-cost: 79 c ---[ 72]---> BDD-cost: 79 c ---[ 71]---> BDD-cost: 79 c ---[ 70]---> BDD-cost: 79 c ---[ 69]---> BDD-cost: 79 c ---[ 68]---> BDD-cost: 79 c ---[ 67]---> BDD-cost: 79 c ---[ 66]---> BDD-cost: 79 c ---[ 65]---> BDD-cost: 79 c ---[ 64]---> BDD-cost: 79 c ---[ 63]---> BDD-cost: 79 c ---[ 62]---> BDD-cost: 79 c ---[ 61]---> BDD-cost: 79 c ---[ 60]---> BDD-cost: 79 c ---[ 59]---> BDD-cost: 79 c ---[ 58]---> BDD-cost: 79 c ---[ 57]---> BDD-cost: 79 c ---[ 56]---> BDD-cost: 79 c ---[ 55]---> BDD-cost: 79 c ---[ 54]---> BDD-cost: 79 c ---[ 53]---> BDD-cost: 79 c ---[ 52]---> BDD-cost: 79 c ---[ 51]---> BDD-cost: 79 c ---[ 50]---> BDD-cost: 79 c ---[ 49]---> BDD-cost: 79 c ---[ 48]---> BDD-cost: 79 c ---[ 47]---> BDD-cost: 79 c ---[ 46]---> BDD-cost: 79 c ---[ 45]---> BDD-cost: 79 c ---[ 44]---> BDD-cost: 79 c ---[ 43]---> BDD-cost: 79 c ---[ 42]---> BDD-cost: 79 c ---[ 41]---> BDD-cost: 79 c ---[ 40]---> BDD-cost: 79 c ---[ 39]---> BDD-cost: 79 c ---[ 38]---> BDD-cost: 79 c ---[ 37]---> BDD-cost: 79 c ---[ 36]---> BDD-cost: 79 c ---[ 35]---> BDD-cost: 79 c ---[ 34]---> BDD-cost: 79 c ---[ 33]---> BDD-cost: 79 c ---[ 32]---> BDD-cost: 79 c ---[ 31]---> BDD-cost: 79 c ---[ 30]---> BDD-cost: 79 c ---[ 29]---> BDD-cost: 79 c ---[ 28]---> BDD-cost: 79 c ---[ 27]---> BDD-cost: 79 c ---[ 26]---> BDD-cost: 79 c ---[ 25]---> BDD-cost: 79 c ---[ 24]---> BDD-cost: 79 c ---[ 23]---> BDD-cost: 79 c ---[ 22]---> BDD-cost: 79 c ---[ 21]---> BDD-cost: 79 c ---[ 20]---> BDD-cost: 79 c ---[ 19]---> BDD-cost: 79 c ---[ 18]---> BDD-cost: 79 c ---[ 17]---> BDD-cost: 79 c ---[ 16]---> BDD-cost: 79 c ---[ 15]---> BDD-cost: 79 c ---[ 14]---> BDD-cost: 79 c ---[ 13]---> BDD-cost: 79 c ---[ 12]---> BDD-cost: 79 c ---[ 11]---> BDD-cost: 79 c ---[ 10]---> BDD-cost: 79 c ---[ 9]---> BDD-cost: 79 c ---[ 8]---> BDD-cost: 79 c ---[ 7]---> BDD-cost: 79 c ---[ 6]---> BDD-cost: 79 c ---[ 5]---> BDD-cost: 79 c ---[ 4]---> BDD-cost: 79 c ---[ 3]---> BDD-cost: 79 c ---[ 2]---> BDD-cost: 79 c ---[ 1]---> BDD-cost: 79 c ---[ 0]---> BDD-cost: 79 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 28162 81120 | 9387 0 0 nan | 0.000 % | c | 100 | 27997 80625 | 10325 27 2140 79.3 | 1.177 % | c | 250 | 27657 79605 | 11358 34 2527 74.3 | 1.896 % | c | 476 | 27218 78290 | 12494 49 2561 52.3 | 2.812 % | c | 813 | 26318 75590 | 13743 80 2795 34.9 | 4.688 % | c | 1321 | 26168 75140 | 15117 519 83828 161.5 | 4.990 % | c | 2083 | 25748 73880 | 16629 1139 202046 177.4 | 5.865 % | c | 3222 | 25228 72320 | 18292 2104 390297 185.5 | 6.948 % | c | 4932 | 24193 69215 | 20121 3426 708435 206.8 | 9.104 % | c | 7498 | 22984 65590 | 22134 5592 1334596 238.7 | 11.625 % | c | 11343 | 21704 61750 | 24347 8970 2331930 260.0 | 14.292 % | c | 17109 | 19166 54140 | 26782 13866 3975662 286.7 | 19.583 % | c | 25758 | 18416 51890 | 29460 22249 6701305 301.2 | 21.146 % | c | 38735 | 17668 49650 | 32406 14788 4504952 304.6 | 22.708 % | c | 58199 | 16889 47315 | 35647 34019 10751402 316.0 | 24.333 % | c | 87391 | 15981 44595 | 39211 36341 14534040 399.9 | 26.229 % | c | 131181 | 15097 41945 | 43133 16553 5983149 361.5 | 28.073 % | c | 196869 | 14347 39695 | 47446 47245 19939784 422.1 | 29.635 % | #### 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.91 0.97 0.92 2/55 29123 Raw data (stat): 29123 (runsolver) R 29122 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481364026 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0005 s] Raw data (loadavg): 0.93 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 1576 0 0 0 996 2 0 0 25 0 1 0 481364026 8290304 1551 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2024 1551 603 41 0 1983 0 vsize: 8096 [startup+20.0005 s] Raw data (loadavg): 0.94 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 1991 0 0 0 1994 4 0 0 25 0 1 0 481364026 10043392 1966 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2452 1966 603 41 0 2411 0 vsize: 9808 [startup+30.0001 s] Raw data (loadavg): 0.95 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 2625 0 0 0 2993 5 0 0 25 0 1 0 481364026 12599296 2600 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3076 2600 603 41 0 3035 0 vsize: 12304 [startup+39.9999 s] Raw data (loadavg): 0.95 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 3024 0 0 0 3992 6 0 0 25 0 1 0 481364026 14221312 2999 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3472 2999 603 41 0 3431 0 vsize: 13888 [startup+49.9999 s] Raw data (loadavg): 0.96 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 3712 0 0 0 4990 8 0 0 25 0 1 0 481364026 17063936 3687 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4166 3687 603 41 0 4125 0 vsize: 16664 [startup+60.0005 s] Raw data (loadavg): 0.97 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 3930 0 0 0 5990 8 0 0 25 0 1 0 481364026 18006016 3905 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4396 3905 603 41 0 4355 0 vsize: 17584 [startup+70.0003 s] Raw data (loadavg): 0.97 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 4092 0 0 0 6990 9 0 0 25 0 1 0 481364026 18546688 4067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4528 4067 603 41 0 4487 0 vsize: 18112 [startup+80.0004 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 4537 0 0 0 7989 9 0 0 25 0 1 0 481364026 20434944 4512 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4989 4512 603 41 0 4948 0 vsize: 19956 [startup+90.0009 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 4759 0 0 0 8989 10 0 0 25 0 1 0 481364026 21377024 4734 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5219 4734 603 41 0 5178 0 vsize: 20876 [startup+100.001 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 5045 0 0 0 9988 11 0 0 25 0 1 0 481364026 22454272 5020 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5482 5020 603 41 0 5441 0 vsize: 21928 [startup+110.002 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 5509 0 0 0 10987 12 0 0 25 0 1 0 481364026 24342528 5484 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5943 5484 603 41 0 5902 0 vsize: 23772 [startup+120.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 6133 0 0 0 11985 14 0 0 25 0 1 0 481364026 26906624 6108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6569 6108 603 41 0 6528 0 vsize: 26276 [startup+130.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 6851 0 0 0 12984 16 0 0 25 0 1 0 481364026 29925376 6826 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7306 6826 603 41 0 7265 0 vsize: 29224 [startup+140.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 7191 0 0 0 13983 17 0 0 25 0 1 0 481364026 31268864 7166 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7634 7166 603 41 0 7593 0 vsize: 30536 [startup+150.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 7860 0 0 0 14982 18 0 0 25 0 1 0 481364026 34095104 7835 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8324 7835 603 41 0 8283 0 vsize: 33296 [startup+160.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 8565 0 0 0 15979 21 0 0 25 0 1 0 481364026 36929536 8540 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9016 8540 603 41 0 8975 0 vsize: 36064 [startup+170.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 8961 0 0 0 16979 21 0 0 25 0 1 0 481364026 38551552 8936 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9412 8936 603 41 0 9371 0 vsize: 37648 [startup+180.002 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 9407 0 0 0 17978 22 0 0 25 0 1 0 481364026 40439808 9382 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9873 9382 603 41 0 9832 0 vsize: 39492 [startup+190.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 10492 0 0 0 18976 24 0 0 25 0 1 0 481364026 44761088 10467 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10928 10467 603 41 0 10887 0 vsize: 43712 [startup+200.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 10610 0 0 0 19976 24 0 0 25 0 1 0 481364026 45297664 10585 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11059 10585 603 41 0 11018 0 vsize: 44236 [startup+210.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11305 0 0 0 20975 26 0 0 25 0 1 0 481364026 48132096 11280 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11751 11280 603 41 0 11710 0 vsize: 47004 [startup+220.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11583 0 0 0 21974 27 0 0 25 0 1 0 481364026 49344512 11558 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12047 11558 603 41 0 12006 0 vsize: 48188 [startup+230.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 22974 27 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12276 11814 603 41 0 12235 0 vsize: 49104 [startup+240.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 23974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12276 11814 603 41 0 12235 0 vsize: 49104 [startup+250.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 24974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12276 11814 603 41 0 12235 0 vsize: 49104 [startup+260.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 25974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12276 11814 603 41 0 12235 0 vsize: 49104 [startup+270.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 26973 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12276 11814 603 41 0 12235 0 vsize: 49104 [startup+280.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 27974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12276 11814 603 41 0 12235 0 vsize: 49104 [startup+290.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29123 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 28974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12276 11814 603 41 0 12235 0 vsize: 49104 [startup+300.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 12097 0 0 0 29973 29 0 0 25 0 1 0 481364026 51359744 12072 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12539 12072 603 41 0 12498 0 vsize: 50156 [startup+310.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 12935 0 0 0 30971 31 0 0 25 0 1 0 481364026 54984704 12910 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13424 12910 603 41 0 13383 0 vsize: 53696 [startup+320.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 13377 0 0 0 31970 32 0 0 25 0 1 0 481364026 56733696 13352 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13851 13352 603 41 0 13810 0 vsize: 55404 [startup+330.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 13563 0 0 0 32970 33 0 0 25 0 1 0 481364026 57544704 13538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14049 13538 603 41 0 14008 0 vsize: 56196 [startup+340.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14414 0 0 0 33968 35 0 0 25 0 1 0 481364026 61059072 14389 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14907 14389 603 41 0 14866 0 vsize: 59628 [startup+350.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 34967 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15271 14784 603 41 0 15230 0 vsize: 61084 [startup+360.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 35967 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15271 14784 603 41 0 15230 0 vsize: 61084 [startup+370.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 36967 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15271 14784 603 41 0 15230 0 vsize: 61084 [startup+380.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 37968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15271 14784 603 41 0 15230 0 vsize: 61084 [startup+390.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 38968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15271 14784 603 41 0 15230 0 vsize: 61084 [startup+400.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 39968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223728 134559121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15271 14784 603 41 0 15230 0 vsize: 61084 [startup+410.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 40968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15271 14784 603 41 0 15230 0 vsize: 61084 [startup+420.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 41968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15271 14784 603 41 0 15230 0 vsize: 61084 [startup+430.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 15072 0 0 0 42968 36 0 0 25 0 1 0 481364026 63631360 15047 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15535 15047 603 41 0 15494 0 vsize: 62140 [startup+440.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 15338 0 0 0 43968 37 0 0 25 0 1 0 481364026 64716800 15313 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15800 15313 603 41 0 15759 0 vsize: 63200 [startup+450.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 15575 0 0 0 44967 37 0 0 25 0 1 0 481364026 65802240 15550 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16065 15550 603 41 0 16024 0 vsize: 64260 [startup+460.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 16500 0 0 0 45965 40 0 0 25 0 1 0 481364026 69582848 16475 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16988 16475 603 41 0 16947 0 vsize: 67952 [startup+470.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 17570 0 0 0 46962 43 0 0 25 0 1 0 481364026 73900032 17545 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18042 17545 603 41 0 18001 0 vsize: 72168 [startup+480.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 17846 0 0 0 47960 44 0 0 25 0 1 0 481364026 75116544 17821 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18339 17821 603 41 0 18298 0 vsize: 73356 [startup+490.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 18267 0 0 0 48960 45 0 0 25 0 1 0 481364026 76722176 18242 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18731 18242 603 41 0 18690 0 vsize: 74924 [startup+500.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 18822 0 0 0 49959 46 0 0 25 0 1 0 481364026 79020032 18797 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19292 18797 603 41 0 19251 0 vsize: 77168 [startup+510.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 50957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+520.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 51957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+530.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 52957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+540.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 53957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+550.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 54957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+560.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 55958 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+570.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 56958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+580.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 57958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+590.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29125 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 58958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+600.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 59958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+610.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 60958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+620.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 61958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19578 603 41 0 20039 0 vsize: 80320 [startup+630.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19604 0 0 0 62958 49 0 0 25 0 1 0 481364026 82247680 19579 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20080 19579 603 41 0 20039 0 vsize: 80320 [startup+640.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 63957 50 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20213 603 41 0 20664 0 vsize: 82820 [startup+650.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 64957 50 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20213 603 41 0 20664 0 vsize: 82820 [startup+660.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 65957 51 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20213 603 41 0 20664 0 vsize: 82820 [startup+670.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 66957 51 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20213 603 41 0 20664 0 vsize: 82820 [startup+680.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 67957 51 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20213 603 41 0 20664 0 vsize: 82820 [startup+690.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 68957 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20214 603 41 0 20664 0 vsize: 82820 [startup+700.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 69957 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20214 603 41 0 20664 0 vsize: 82820 [startup+710.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 70958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20214 603 41 0 20664 0 vsize: 82820 [startup+720.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 71958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20214 603 41 0 20664 0 vsize: 82820 [startup+730.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 72958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20214 603 41 0 20664 0 vsize: 82820 [startup+740.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 73958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20214 603 41 0 20664 0 vsize: 82820 [startup+750.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 74958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20705 20214 603 41 0 20664 0 vsize: 82820 [startup+760.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20311 0 0 0 75958 51 0 0 25 0 1 0 481364026 85078016 20286 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20771 20286 603 41 0 20730 0 vsize: 83084 [startup+770.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 21085 0 0 0 76957 52 0 0 25 0 1 0 481364026 88322048 21060 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21563 21060 603 41 0 21522 0 vsize: 86252 [startup+780.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 21326 0 0 0 77957 53 0 0 25 0 1 0 481364026 89268224 21301 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21794 21301 603 41 0 21753 0 vsize: 87176 [startup+790.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 21819 0 0 0 78957 53 0 0 25 0 1 0 481364026 91295744 21794 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22289 21794 603 41 0 22248 0 vsize: 89156 [startup+800.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 22156 0 0 0 79956 54 0 0 25 0 1 0 481364026 92647424 22131 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22619 22131 603 41 0 22578 0 vsize: 90476 [startup+810.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 22971 0 0 0 80955 56 0 0 25 0 1 0 481364026 96022528 22946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23443 22946 603 41 0 23402 0 vsize: 93772 [startup+820.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 81955 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+830.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 82955 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+840.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 83955 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+850.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 84955 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223648 134560523 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+860.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 85956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+870.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 86956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+880.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 87956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+890.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29127 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 88956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+900.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 89956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+910.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 90956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+920.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 91956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+930.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 92956 57 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23510 23013 603 41 0 23469 0 vsize: 94040 [startup+940.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23174 0 0 0 93956 57 0 0 25 0 1 0 481364026 96837632 23149 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23642 23149 603 41 0 23601 0 vsize: 94568 [startup+950.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23846 0 0 0 94955 58 0 0 25 0 1 0 481364026 99680256 23821 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24336 23821 603 41 0 24295 0 vsize: 97344 [startup+960.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 24920 0 0 0 95951 61 0 0 25 0 1 0 481364026 103989248 24895 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25388 24895 603 41 0 25347 0 vsize: 101552 [startup+970.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 25929 0 0 0 96949 64 0 0 25 0 1 0 481364026 108167168 25904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26408 25904 603 41 0 26367 0 vsize: 105632 [startup+980.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 97949 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+990.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 98949 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1000.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 99949 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1010.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 100949 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 101950 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 102950 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 103950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 104950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223728 134559618 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 105950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 106950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 107950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 108951 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 109951 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 110951 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223704 134560076 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 111951 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26606 26110 603 41 0 26565 0 vsize: 106424 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 112951 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26566 26074 603 41 0 26525 0 vsize: 106264 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 113951 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26566 26074 603 41 0 26525 0 vsize: 106264 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 114951 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26566 26074 603 41 0 26525 0 vsize: 106264 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 115952 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223728 134559618 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26566 26074 603 41 0 26525 0 vsize: 106264 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 116952 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26566 26074 603 41 0 26525 0 vsize: 106264 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26136 0 0 0 117952 65 0 0 25 0 1 0 481364026 108814336 26075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26566 26075 603 41 0 26525 0 vsize: 106264 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29129 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26136 0 0 0 118952 65 0 0 25 0 1 0 481364026 108814336 26075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26566 26075 603 41 0 26525 0 vsize: 106264 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 29131 Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26136 0 0 0 119952 65 0 0 25 0 1 0 481364026 108814336 26075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26566 26075 603 41 0 26525 0 vsize: 106264 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.92 1/55 29131 Raw data (stat): 29123 (minisat+) Z 29122 22929 22928 0 -1 12 26138 0 0 0 119952 70 0 0 25 0 1 0 481364026 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.08 CPU time (s): 1200.23 CPU user time (s): 1199.53 CPU system time (s): 0.707892 CPU usage (%): 100.013 Max. virtual memory (Kb): 106424 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####