Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl40_45_pb.cnf.cr.opb |
MD5SUM | df5f31774bab40070962f7d0b16d093c |
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 | 46 |
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.107983 |
Number of variables | 3600 |
Total number of constraints | 170 |
Number of constraints which are clauses | 90 |
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 | 45 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc11 THE 2005-04-14 03:31:11 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4530 boxname=wulflinc11 idbench=18 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: df5f31774bab40070962f7d0b16d093c /oldhome/oroussel/tmp/wulflinc11/normalized-chnl40_45_pb.cnf.cr.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc11/normalized-chnl40_45_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc11/normalized-chnl40_45_pb.cnf.cr.opb IDLAUNCH: 4530 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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: 906920 kB Buffers: 36192 kB Cached: 67200 kB SwapCached: 4932 kB Active: 57312 kB Inactive: 53836 kB HighTotal: 131008 kB HighFree: 59976 kB LowTotal: 903652 kB LowFree: 846944 kB SwapTotal: 2097136 kB SwapFree: 2092204 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6924 kB Slab: 10900 kB Committed_AS: 63488 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 03:51:13 (client local time) WITH STATUS 0 IN 1200.22 SECONDS stats: 4530 7 1200.22 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 170 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .......................................................................................... c ---[ 79]---> BDD-cost: 87 c ---[ 78]---> BDD-cost: 87 c ---[ 77]---> BDD-cost: 87 c ---[ 76]---> BDD-cost: 87 c ---[ 75]---> BDD-cost: 87 c ---[ 74]---> BDD-cost: 87 c ---[ 73]---> BDD-cost: 87 c ---[ 72]---> BDD-cost: 87 c ---[ 71]---> BDD-cost: 87 c ---[ 70]---> BDD-cost: 87 c ---[ 69]---> BDD-cost: 87 c ---[ 68]---> BDD-cost: 87 c ---[ 67]---> BDD-cost: 87 c ---[ 66]---> BDD-cost: 87 c ---[ 65]---> BDD-cost: 87 c ---[ 64]---> BDD-cost: 87 c ---[ 63]---> BDD-cost: 87 c ---[ 62]---> BDD-cost: 87 c ---[ 61]---> BDD-cost: 87 c ---[ 60]---> BDD-cost: 87 c ---[ 59]---> BDD-cost: 87 c ---[ 58]---> BDD-cost: 87 c ---[ 57]---> BDD-cost: 87 c ---[ 56]---> BDD-cost: 87 c ---[ 55]---> BDD-cost: 87 c ---[ 54]---> BDD-cost: 87 c ---[ 53]---> BDD-cost: 87 c ---[ 52]---> BDD-cost: 87 c ---[ 51]---> BDD-cost: 87 c ---[ 50]---> BDD-cost: 87 c ---[ 49]---> BDD-cost: 87 c ---[ 48]---> BDD-cost: 87 c ---[ 47]---> BDD-cost: 87 c ---[ 46]---> BDD-cost: 87 c ---[ 45]---> BDD-cost: 87 c ---[ 44]---> BDD-cost: 87 c ---[ 43]---> BDD-cost: 87 c ---[ 42]---> BDD-cost: 87 c ---[ 41]---> BDD-cost: 87 c ---[ 40]---> BDD-cost: 87 c ---[ 39]---> BDD-cost: 87 c ---[ 38]---> BDD-cost: 87 c ---[ 37]---> BDD-cost: 87 c ---[ 36]---> BDD-cost: 87 c ---[ 35]---> BDD-cost: 87 c ---[ 34]---> BDD-cost: 87 c ---[ 33]---> BDD-cost: 87 c ---[ 32]---> BDD-cost: 87 c ---[ 31]---> BDD-cost: 87 c ---[ 30]---> BDD-cost: 87 c ---[ 29]---> BDD-cost: 87 c ---[ 28]---> BDD-cost: 87 c ---[ 27]---> BDD-cost: 87 c ---[ 26]---> BDD-cost: 87 c ---[ 25]---> BDD-cost: 87 c ---[ 24]---> BDD-cost: 87 c ---[ 23]---> BDD-cost: 87 c ---[ 22]---> BDD-cost: 87 c ---[ 21]---> BDD-cost: 87 c ---[ 20]---> BDD-cost: 87 c ---[ 19]---> BDD-cost: 87 c ---[ 18]---> BDD-cost: 87 c ---[ 17]---> BDD-cost: 87 c ---[ 16]---> BDD-cost: 87 c ---[ 15]---> BDD-cost: 87 c ---[ 14]---> BDD-cost: 87 c ---[ 13]---> BDD-cost: 87 c ---[ 12]---> BDD-cost: 87 c ---[ 11]---> BDD-cost: 87 c ---[ 10]---> BDD-cost: 87 c ---[ 9]---> BDD-cost: 87 c ---[ 8]---> BDD-cost: 87 c ---[ 7]---> BDD-cost: 87 c ---[ 6]---> BDD-cost: 87 c ---[ 5]---> BDD-cost: 87 c ---[ 4]---> BDD-cost: 87 c ---[ 3]---> BDD-cost: 87 c ---[ 2]---> BDD-cost: 87 c ---[ 1]---> BDD-cost: 87 c ---[ 0]---> BDD-cost: 87 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 31050 89440 | 10350 0 0 nan | 0.000 % | c | 100 | 30745 88525 | 11385 7 15 2.1 | 1.345 % | c | 250 | 30365 87385 | 12523 18 41 2.3 | 2.055 % | c | 475 | 29750 85540 | 13775 36 86 2.4 | 3.229 % | c | 813 | 29305 84205 | 15153 217 25261 116.4 | 4.063 % | c | 1320 | 28730 82480 | 16668 535 83456 156.0 | 5.152 % | c | 2079 | 28620 82150 | 18335 1250 268069 214.5 | 5.360 % | c | 3221 | 28060 80470 | 20169 2162 430715 199.2 | 6.420 % | c | 4929 | 27495 78775 | 22186 3654 781855 214.0 | 7.491 % | c | 7493 | 26565 75985 | 24404 5892 1319099 223.9 | 9.252 % | c | 11338 | 25020 71350 | 26845 9203 2200913 239.2 | 12.178 % | c | 17104 | 23325 66265 | 29529 14409 3611532 250.6 | 15.388 % | c | 25753 | 21466 60690 | 32482 22459 6293342 280.2 | 18.911 % | c | 38727 | 20227 56975 | 35731 35014 10328228 295.0 | 21.259 % | c | 58188 | 18788 52660 | 39304 25546 8175374 320.0 | 23.987 % | c | 87383 | 17264 48090 | 43234 24209 8566180 353.8 | 26.875 % | c | 131172 | 16565 45995 | 47557 33500 12860011 383.9 | 28.201 % | c | 196856 | 16071 44515 | 52313 17385 6319087 363.5 | 29.138 % | #### 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.85 0.97 0.93 2/54 6932 Raw data (stat): 6932 (runsolver) R 6931 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423145402 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0003 s] Raw data (loadavg): 0.87 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 1609 0 0 0 993 5 0 0 25 0 1 0 423145402 8335360 1584 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2035 1584 603 41 0 1994 0 vsize: 8140 [startup+20.0005 s] Raw data (loadavg): 0.89 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 2131 0 0 0 1992 6 0 0 25 0 1 0 423145402 10498048 2106 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2563 2106 603 41 0 2522 0 vsize: 10252 [startup+30.0009 s] Raw data (loadavg): 0.91 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 2804 0 0 0 2990 8 0 0 25 0 1 0 423145402 13332480 2779 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3255 2779 603 41 0 3214 0 vsize: 13020 [startup+40.0007 s] Raw data (loadavg): 0.92 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 3248 0 0 0 3988 10 0 0 25 0 1 0 423145402 15085568 3223 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3683 3223 603 41 0 3642 0 vsize: 14732 [startup+50.002 s] Raw data (loadavg): 0.93 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 3618 0 0 0 4987 11 0 0 25 0 1 0 423145402 16703488 3593 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4078 3593 603 41 0 4037 0 vsize: 16312 [startup+60.0023 s] Raw data (loadavg): 0.94 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 3817 0 0 0 5986 12 0 0 25 0 1 0 423145402 17514496 3792 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4276 3792 603 41 0 4235 0 vsize: 17104 [startup+70.002 s] Raw data (loadavg): 0.95 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 4063 0 0 0 6985 13 0 0 25 0 1 0 423145402 18456576 4038 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4506 4038 603 41 0 4465 0 vsize: 18024 [startup+80.0033 s] Raw data (loadavg): 0.96 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 4430 0 0 0 7985 14 0 0 25 0 1 0 423145402 19943424 4405 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4869 4405 603 41 0 4828 0 vsize: 19476 [startup+90.0026 s] Raw data (loadavg): 0.96 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 5019 0 0 0 8983 16 0 0 25 0 1 0 423145402 22364160 4994 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5460 4994 603 41 0 5419 0 vsize: 21840 [startup+100.003 s] Raw data (loadavg): 0.97 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 5613 0 0 0 9981 18 0 0 25 0 1 0 423145402 24780800 5588 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6050 5588 603 41 0 6009 0 vsize: 24200 [startup+110.005 s] Raw data (loadavg): 0.97 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 5881 0 0 0 10981 18 0 0 25 0 1 0 423145402 26005504 5856 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6349 5856 603 41 0 6308 0 vsize: 25396 [startup+120.004 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 6320 0 0 0 11979 20 0 0 25 0 1 0 423145402 27762688 6295 4294967295 134512640 134672761 3221224544 3221223648 134559991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6778 6295 603 41 0 6737 0 vsize: 27112 [startup+130.004 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 6696 0 0 0 12978 21 0 0 25 0 1 0 423145402 29245440 6671 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7140 6671 603 41 0 7099 0 vsize: 28560 [startup+140.004 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 7108 0 0 0 13977 22 0 0 25 0 1 0 423145402 31002624 7083 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7569 7083 603 41 0 7528 0 vsize: 30276 [startup+150.004 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 7229 0 0 0 14977 22 0 0 25 0 1 0 423145402 31404032 7204 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7667 7204 603 41 0 7626 0 vsize: 30668 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 7600 0 0 0 15976 23 0 0 25 0 1 0 423145402 33026048 7575 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8063 7575 603 41 0 8022 0 vsize: 32252 [startup+170.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 8218 0 0 0 16975 25 0 0 25 0 1 0 423145402 35450880 8193 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8655 8193 603 41 0 8614 0 vsize: 34620 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 8887 0 0 0 17973 26 0 0 25 0 1 0 423145402 38277120 8862 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9345 8862 603 41 0 9304 0 vsize: 37380 [startup+190.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 8889 0 0 0 18972 27 0 0 25 0 1 0 423145402 38277120 8864 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9345 8864 603 41 0 9304 0 vsize: 37380 [startup+200.006 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 9023 0 0 0 19972 27 0 0 25 0 1 0 423145402 38817792 8998 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9477 8998 603 41 0 9436 0 vsize: 37908 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 9633 0 0 0 20971 28 0 0 25 0 1 0 423145402 41254912 9608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10072 9608 603 41 0 10031 0 vsize: 40288 [startup+220.006 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 9940 0 0 0 21970 29 0 0 25 0 1 0 423145402 42471424 9915 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10369 9915 603 41 0 10328 0 vsize: 41476 [startup+230.006 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 10741 0 0 0 22967 32 0 0 25 0 1 0 423145402 45838336 10716 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11191 10716 603 41 0 11150 0 vsize: 44764 [startup+240.005 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 10985 0 0 0 23966 34 0 0 25 0 1 0 423145402 46780416 10960 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11421 10960 603 41 0 11380 0 vsize: 45684 [startup+250.006 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 11443 0 0 0 24963 36 0 0 25 0 1 0 423145402 48672768 11418 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11883 11418 603 41 0 11842 0 vsize: 47532 [startup+260.006 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 11552 0 0 0 25963 37 0 0 25 0 1 0 423145402 49078272 11527 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11982 11527 603 41 0 11941 0 vsize: 47928 [startup+270.006 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 12166 0 0 0 26961 38 0 0 25 0 1 0 423145402 51765248 12141 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12638 12141 603 41 0 12597 0 vsize: 50552 [startup+280.007 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 12683 0 0 0 27960 40 0 0 25 0 1 0 423145402 53919744 12658 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13164 12658 603 41 0 13123 0 vsize: 52656 [startup+290.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 12790 0 0 0 28960 40 0 0 25 0 1 0 423145402 54325248 12765 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13263 12765 603 41 0 13222 0 vsize: 53052 [startup+300.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 12897 0 0 0 29959 41 0 0 25 0 1 0 423145402 54734848 12872 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13363 12872 603 41 0 13322 0 vsize: 53452 [startup+310.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 13160 0 0 0 30958 42 0 0 25 0 1 0 423145402 55812096 13135 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13626 13135 603 41 0 13585 0 vsize: 54504 [startup+320.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 13394 0 0 0 31957 43 0 0 25 0 1 0 423145402 56758272 13369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13857 13369 603 41 0 13816 0 vsize: 55428 [startup+330.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 13702 0 0 0 32956 44 0 0 25 0 1 0 423145402 57970688 13677 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14153 13677 603 41 0 14112 0 vsize: 56612 [startup+340.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14014 0 0 0 33955 45 0 0 25 0 1 0 423145402 59330560 13989 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14485 13989 603 41 0 14444 0 vsize: 57940 [startup+350.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 34954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+360.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 35954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+370.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 36954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+380.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 37954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+390.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 38954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+400.011 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 39955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+410.011 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 40955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+420.011 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 41955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+430.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 42955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+440.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 43955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+450.011 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 44955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+460.011 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 45955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15240 14760 603 41 0 15199 0 vsize: 60960 [startup+470.011 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14826 0 0 0 46955 47 0 0 25 0 1 0 423145402 62558208 14801 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15273 14801 603 41 0 15232 0 vsize: 61092 [startup+480.011 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 15768 0 0 0 47953 50 0 0 25 0 1 0 423145402 66469888 15743 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16228 15743 603 41 0 16187 0 vsize: 64912 [startup+490.011 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16005 0 0 0 48953 50 0 0 25 0 1 0 423145402 67420160 15980 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16460 15980 603 41 0 16419 0 vsize: 65840 [startup+500.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16005 0 0 0 49953 50 0 0 25 0 1 0 423145402 67420160 15980 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16460 15980 603 41 0 16419 0 vsize: 65840 [startup+510.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16077 0 0 0 50953 50 0 0 25 0 1 0 423145402 67690496 16052 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16526 16052 603 41 0 16485 0 vsize: 66104 [startup+520.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16492 0 0 0 51952 51 0 0 25 0 1 0 423145402 69443584 16467 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16954 16467 603 41 0 16913 0 vsize: 67816 [startup+530.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16517 0 0 0 52953 51 0 0 25 0 1 0 423145402 69582848 16492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16988 16492 603 41 0 16947 0 vsize: 67952 [startup+540.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16823 0 0 0 53952 52 0 0 25 0 1 0 423145402 70795264 16798 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17284 16798 603 41 0 17243 0 vsize: 69136 [startup+550.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 54951 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+560.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 55952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+570.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 56952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+580.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 57952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+590.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 58952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+600.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 59952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+610.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 60952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+620.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 61952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+630.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 62952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+640.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 63953 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+650.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 64953 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17482 17009 603 41 0 17441 0 vsize: 69928 [startup+660.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 18011 0 0 0 65951 55 0 0 25 0 1 0 423145402 75653120 17986 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18470 17986 603 41 0 18429 0 vsize: 73880 [startup+670.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 18310 0 0 0 66950 56 0 0 25 0 1 0 423145402 76886016 18285 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18771 18285 603 41 0 18730 0 vsize: 75084 [startup+680.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 18898 0 0 0 67949 57 0 0 25 0 1 0 423145402 79319040 18873 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19365 18873 603 41 0 19324 0 vsize: 77460 [startup+690.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 19711 0 0 0 68948 58 0 0 25 0 1 0 423145402 82690048 19686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20188 19686 603 41 0 20147 0 vsize: 80752 [startup+700.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 20760 0 0 0 69946 60 0 0 25 0 1 0 423145402 87015424 20735 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21244 20736 603 41 0 21203 0 vsize: 84976 [startup+710.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 70945 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+720.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 71946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+730.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 72946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+740.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 73946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+750.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 74946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+760.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 75946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+770.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 76947 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+780.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 77946 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+790.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 78946 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+800.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 79946 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+810.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 80947 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+820.019 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 81947 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22002 21520 603 41 0 21961 0 vsize: 88008 [startup+830.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 22103 0 0 0 82946 63 0 0 25 0 1 0 423145402 92536832 22078 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22592 22078 603 41 0 22551 0 vsize: 90368 [startup+840.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 22751 0 0 0 83945 64 0 0 25 0 1 0 423145402 95092736 22726 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23216 22726 603 41 0 23175 0 vsize: 92864 [startup+850.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 23170 0 0 0 84945 65 0 0 25 0 1 0 423145402 96858112 23145 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23647 23145 603 41 0 23606 0 vsize: 94588 [startup+860.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 24275 0 0 0 85942 67 0 0 25 0 1 0 423145402 101421056 24250 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24761 24250 603 41 0 24720 0 vsize: 99044 [startup+870.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 24869 0 0 0 86941 69 0 0 25 0 1 0 423145402 103854080 24844 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25355 24844 603 41 0 25314 0 vsize: 101420 [startup+880.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 25715 0 0 0 87939 71 0 0 25 0 1 0 423145402 107225088 25690 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26178 25690 603 41 0 26137 0 vsize: 104712 [startup+890.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26557 0 0 0 88938 72 0 0 25 0 1 0 423145402 110751744 26532 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26532 603 41 0 26998 0 vsize: 108156 [startup+900.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26557 0 0 0 89938 72 0 0 25 0 1 0 423145402 110751744 26532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26532 603 41 0 26998 0 vsize: 108156 [startup+910.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26557 0 0 0 90938 72 0 0 25 0 1 0 423145402 110751744 26532 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26532 603 41 0 26998 0 vsize: 108156 [startup+920.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 91938 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+930.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 92938 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+940.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 93939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+950.024 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 94939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+960.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 95939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+970.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 96939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+980.024 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 97939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+990.024 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 98940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+1000.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 99940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+1010.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 100940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+1020.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 101940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+1030.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 102940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+1040.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 103940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 104941 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 105941 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27039 26533 603 41 0 26998 0 vsize: 108156 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 106941 72 0 0 25 0 1 0 423145402 110534656 26498 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26498 603 41 0 26945 0 vsize: 107944 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 107941 72 0 0 25 0 1 0 423145402 110534656 26498 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26498 603 41 0 26945 0 vsize: 107944 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 108941 73 0 0 25 0 1 0 423145402 110534656 26498 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26498 603 41 0 26945 0 vsize: 107944 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 109941 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 110941 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 111942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 112942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 113942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 114942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 115942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 116943 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 117943 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 118943 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 6932 Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 119943 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26986 26499 603 41 0 26945 0 vsize: 107944 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.93 1/54 6932 Raw data (stat): 6932 (minisat+) Z 6931 32461 32460 0 -1 12 26561 0 0 0 119943 77 0 0 25 0 1 0 423145402 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.22 CPU user time (s): 1199.44 CPU system time (s): 0.779881 CPU usage (%): 100.011 Max. virtual memory (Kb): 108156 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####