Name | normalized-opb/submitted/manquinho/logic-synthesis/normalized-5xp1.b.opb |
MD5SUM | 24a8f38e94b07e6ca192a34c96c24c6e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 12 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 465 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 465 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 465 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.03084 |
Number of variables | 464 |
Total number of constraints | 859 |
Number of constraints which are clauses | 845 |
Number of constraints which are cardinality constraints (but not clauses) | 14 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 149 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc26 THE 2005-04-14 01:47:50 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4195 boxname=wulflinc26 idbench=59 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 24a8f38e94b07e6ca192a34c96c24c6e /oldhome/oroussel/tmp/wulflinc26/normalized-5xp1.b.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc26/normalized-5xp1.b.opb /oldhome/oroussel/tmp/wulflinc26/normalized-5xp1.b.opb IDLAUNCH: 4195 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 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 : 3 cpu MHz : 451.061 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 834660 kB Buffers: 35252 kB Cached: 124520 kB SwapCached: 2476 kB Active: 55652 kB Inactive: 109508 kB HighTotal: 131008 kB HighFree: 3388 kB LowTotal: 903652 kB LowFree: 831272 kB SwapTotal: 2097892 kB SwapFree: 2095416 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6948 kB Slab: 29380 kB Committed_AS: 63616 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 02:07:52 (client local time) WITH STATUS 10 IN 1200.12 SECONDS stats: 4195 7 1200.12 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 843 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 843 29887 | 281 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 20[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:17506 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 19368 73043 | 6456 0 0 nan | 0.000 % | c | 102 | 19368 73043 | 7101 102 7508 73.6 | 0.016 % | c | 253 | 19356 73019 | 7811 251 21282 84.8 | 0.056 % | c ============================================================================== c [1mFound solution: 17[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 293 | 17268 68155 | 5756 287 23635 82.4 | 0.056 % | c | 393 | 17268 68155 | 6331 387 30443 78.7 | 11.325 % | c | 543 | 17268 68155 | 6964 537 39041 72.7 | 11.325 % | c | 770 | 17268 68155 | 7661 764 50110 65.6 | 11.325 % | c ============================================================================== c [1mFound solution: 15[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 864 | 17261 68142 | 5753 845 54108 64.0 | 11.325 % | c | 964 | 17261 68142 | 6328 945 61405 65.0 | 11.470 % | c | 1115 | 17261 68142 | 6961 1096 75538 68.9 | 11.470 % | c | 1341 | 17261 68142 | 7657 1322 87753 66.4 | 11.470 % | c | 1678 | 17261 68142 | 8422 1659 110793 66.8 | 11.470 % | c | 2184 | 17261 68142 | 9265 2165 155258 71.7 | 11.470 % | c | 2943 | 17261 68142 | 10191 2924 219586 75.1 | 11.470 % | c ============================================================================== c [1mFound solution: 14[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3979 | 17273 68172 | 5757 3960 368681 93.1 | 11.470 % | c | 4081 | 17273 68172 | 6332 4062 376314 92.6 | 11.470 % | c | 4232 | 17273 68172 | 6965 4213 386712 91.8 | 11.470 % | c | 4457 | 17273 68172 | 7662 4438 409455 92.3 | 11.470 % | c | 4795 | 17273 68172 | 8428 4776 432918 90.6 | 11.470 % | c | 5301 | 17273 68172 | 9271 5282 466487 88.3 | 11.470 % | c | 6061 | 17273 68172 | 10198 6042 522550 86.5 | 11.470 % | c | 7204 | 17273 68172 | 11218 7185 589528 82.0 | 11.470 % | c | 8917 | 17273 68172 | 12340 8898 698521 78.5 | 11.470 % | c | 11480 | 17273 68172 | 13574 11461 858013 74.9 | 11.470 % | c | 15325 | 17273 68172 | 14932 15306 1141586 74.6 | 11.470 % | c | 21092 | 17273 68172 | 16425 12759 938327 73.5 | 11.470 % | c | 29741 | 17273 68172 | 18067 12053 875185 72.6 | 11.470 % | c | 42716 | 17273 68172 | 19874 14184 867021 61.1 | 11.470 % | c | 62178 | 17273 68172 | 21862 11498 890576 77.5 | 11.470 % | c | 91371 | 17273 68172 | 24048 15677 1206811 77.0 | 11.470 % | c | 135161 | 17273 68172 | 26453 20827 1226051 58.9 | 11.470 % | c | 200848 | 17273 68172 | 29098 27816 1466699 52.7 | 11.470 % | c | 299376 | 17273 68172 | 32008 25897 1765102 68.2 | 11.470 % | #### 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.91 2/54 29018 Raw data (stat): 29018 (runsolver) R 29017 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480753407 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0008 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 1899 0 0 0 993 5 0 0 25 0 1 0 480753407 9879552 1876 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2412 1876 603 41 0 2371 0 vsize: 9648 [startup+20.0012 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2228 0 0 0 1992 6 0 0 25 0 1 0 480753407 11223040 2205 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2740 2205 603 41 0 2699 0 vsize: 10960 [startup+30.0022 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2596 0 0 0 2991 7 0 0 25 0 1 0 480753407 12689408 2573 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3098 2573 603 41 0 3057 0 vsize: 12392 [startup+40.0022 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2752 0 0 0 3990 7 0 0 25 0 1 0 480753407 13463552 2729 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3287 2729 603 41 0 3246 0 vsize: 13148 [startup+50.0024 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2752 0 0 0 4990 7 0 0 25 0 1 0 480753407 13463552 2729 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3287 2729 603 41 0 3246 0 vsize: 13148 [startup+60.0025 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2778 0 0 0 5989 8 0 0 25 0 1 0 480753407 13463552 2755 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3287 2755 603 41 0 3246 0 vsize: 13148 [startup+70.0032 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2955 0 0 0 6988 9 0 0 25 0 1 0 480753407 14282752 2932 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3487 2932 603 41 0 3446 0 vsize: 13948 [startup+80.0035 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 2955 0 0 0 7988 9 0 0 25 0 1 0 480753407 14282752 2932 4294967295 134512640 134672761 3221224560 3221223664 134559866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3487 2932 603 41 0 3446 0 vsize: 13948 [startup+90.0036 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3080 0 0 0 8988 10 0 0 25 0 1 0 480753407 14807040 3057 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3615 3057 603 41 0 3574 0 vsize: 14460 [startup+100.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3178 0 0 0 9986 11 0 0 25 0 1 0 480753407 15204352 3155 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3712 3155 603 41 0 3671 0 vsize: 14848 [startup+110.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3184 0 0 0 10986 11 0 0 25 0 1 0 480753407 15204352 3161 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3712 3161 603 41 0 3671 0 vsize: 14848 [startup+120.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3249 0 0 0 11985 12 0 0 25 0 1 0 480753407 15478784 3226 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3779 3226 603 41 0 3738 0 vsize: 15116 [startup+130.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3436 0 0 0 12984 13 0 0 25 0 1 0 480753407 16281600 3413 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3975 3413 603 41 0 3934 0 vsize: 15900 [startup+140.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3454 0 0 0 13984 13 0 0 25 0 1 0 480753407 16281600 3431 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3975 3431 603 41 0 3934 0 vsize: 15900 [startup+150.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3523 0 0 0 14984 13 0 0 25 0 1 0 480753407 16699392 3500 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4077 3500 603 41 0 4036 0 vsize: 16308 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3759 0 0 0 15983 14 0 0 25 0 1 0 480753407 17682432 3736 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4317 3736 603 41 0 4276 0 vsize: 17268 [startup+170.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3767 0 0 0 16983 15 0 0 25 0 1 0 480753407 17682432 3744 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4317 3744 603 41 0 4276 0 vsize: 17268 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3790 0 0 0 17983 15 0 0 25 0 1 0 480753407 17829888 3767 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4353 3767 603 41 0 4312 0 vsize: 17412 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3830 0 0 0 18982 15 0 0 25 0 1 0 480753407 17977344 3807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4389 3807 603 41 0 4348 0 vsize: 17556 [startup+200.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3862 0 0 0 19982 16 0 0 25 0 1 0 480753407 18288640 3839 4294967295 134512640 134672761 3221224560 3221223560 1075350054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3839 603 41 0 4424 0 vsize: 17860 [startup+210.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3864 0 0 0 20981 16 0 0 25 0 1 0 480753407 18288640 3841 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3841 603 41 0 4424 0 vsize: 17860 [startup+220.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3876 0 0 0 21981 16 0 0 25 0 1 0 480753407 18288640 3853 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3853 603 41 0 4424 0 vsize: 17860 [startup+230.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3880 0 0 0 22981 17 0 0 25 0 1 0 480753407 18288640 3857 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3857 603 41 0 4424 0 vsize: 17860 [startup+240.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 3888 0 0 0 23980 17 0 0 25 0 1 0 480753407 18288640 3865 4294967295 134512640 134672761 3221224560 3221223728 134561272 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3865 603 41 0 4424 0 vsize: 17860 [startup+250.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4035 0 0 0 24980 18 0 0 25 0 1 0 480753407 18997248 4012 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4638 4012 603 41 0 4597 0 vsize: 18552 [startup+260.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4081 0 0 0 25979 18 0 0 25 0 1 0 480753407 19136512 4058 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4672 4058 603 41 0 4631 0 vsize: 18688 [startup+270.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4093 0 0 0 26979 19 0 0 25 0 1 0 480753407 19300352 4070 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4712 4070 603 41 0 4671 0 vsize: 18848 [startup+280.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4103 0 0 0 27979 19 0 0 25 0 1 0 480753407 19300352 4080 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4712 4080 603 41 0 4671 0 vsize: 18848 [startup+290.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4122 0 0 0 28978 19 0 0 25 0 1 0 480753407 19464192 4099 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4752 4099 603 41 0 4711 0 vsize: 19008 [startup+300.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4127 0 0 0 29977 20 0 0 25 0 1 0 480753407 19464192 4104 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4752 4104 603 41 0 4711 0 vsize: 19008 [startup+310.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4127 0 0 0 30977 20 0 0 25 0 1 0 480753407 19464192 4104 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4752 4104 603 41 0 4711 0 vsize: 19008 [startup+320.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4140 0 0 0 31976 21 0 0 25 0 1 0 480753407 19464192 4117 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4752 4117 603 41 0 4711 0 vsize: 19008 [startup+330.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4163 0 0 0 32976 21 0 0 25 0 1 0 480753407 19607552 4140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4787 4140 603 41 0 4746 0 vsize: 19148 [startup+340.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4189 0 0 0 33976 22 0 0 25 0 1 0 480753407 19755008 4166 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4166 603 41 0 4782 0 vsize: 19292 [startup+350.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4197 0 0 0 34975 22 0 0 25 0 1 0 480753407 19755008 4174 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4174 603 41 0 4782 0 vsize: 19292 [startup+360.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4198 0 0 0 35975 22 0 0 25 0 1 0 480753407 19755008 4175 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4175 603 41 0 4782 0 vsize: 19292 [startup+370.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4206 0 0 0 36974 23 0 0 25 0 1 0 480753407 19755008 4183 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4183 603 41 0 4782 0 vsize: 19292 [startup+380.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4207 0 0 0 37974 23 0 0 25 0 1 0 480753407 19755008 4184 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4184 603 41 0 4782 0 vsize: 19292 [startup+390.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4210 0 0 0 38974 23 0 0 25 0 1 0 480753407 19755008 4187 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4823 4187 603 41 0 4782 0 vsize: 19292 [startup+400.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4210 0 0 0 39973 24 0 0 25 0 1 0 480753407 19755008 4187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4187 603 41 0 4782 0 vsize: 19292 [startup+410.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4218 0 0 0 40973 24 0 0 25 0 1 0 480753407 19755008 4195 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4823 4195 603 41 0 4782 0 vsize: 19292 [startup+420.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4221 0 0 0 41973 24 0 0 25 0 1 0 480753407 19918848 4198 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4863 4198 603 41 0 4822 0 vsize: 19452 [startup+430.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4221 0 0 0 42974 24 0 0 25 0 1 0 480753407 19918848 4198 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4863 4198 603 41 0 4822 0 vsize: 19452 [startup+440.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4235 0 0 0 43974 24 0 0 25 0 1 0 480753407 19918848 4212 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4863 4212 603 41 0 4822 0 vsize: 19452 [startup+450.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4236 0 0 0 44974 24 0 0 25 0 1 0 480753407 19918848 4213 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4863 4213 603 41 0 4822 0 vsize: 19452 [startup+460.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4255 0 0 0 45974 24 0 0 25 0 1 0 480753407 20082688 4232 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4903 4232 603 41 0 4862 0 vsize: 19612 [startup+470.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4256 0 0 0 46974 24 0 0 25 0 1 0 480753407 20082688 4233 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4903 4233 603 41 0 4862 0 vsize: 19612 [startup+480.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4256 0 0 0 47974 24 0 0 25 0 1 0 480753407 20082688 4233 4294967295 134512640 134672761 3221224560 3221223664 134555076 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4903 4233 603 41 0 4862 0 vsize: 19612 [startup+490.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4261 0 0 0 48975 24 0 0 25 0 1 0 480753407 20082688 4238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4903 4238 603 41 0 4862 0 vsize: 19612 [startup+500.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4261 0 0 0 49975 24 0 0 25 0 1 0 480753407 20082688 4238 4294967295 134512640 134672761 3221224560 3221223664 134555214 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4903 4238 603 41 0 4862 0 vsize: 19612 [startup+510.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4284 0 0 0 50975 24 0 0 25 0 1 0 480753407 20246528 4261 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4943 4261 603 41 0 4902 0 vsize: 19772 [startup+520.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4298 0 0 0 51975 24 0 0 25 0 1 0 480753407 20246528 4275 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4943 4275 603 41 0 4902 0 vsize: 19772 [startup+530.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4311 0 0 0 52975 24 0 0 25 0 1 0 480753407 20246528 4288 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4943 4288 603 41 0 4902 0 vsize: 19772 [startup+540.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4341 0 0 0 53975 24 0 0 25 0 1 0 480753407 20410368 4318 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4983 4318 603 41 0 4942 0 vsize: 19932 [startup+550.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4341 0 0 0 54975 24 0 0 25 0 1 0 480753407 20410368 4318 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4983 4318 603 41 0 4942 0 vsize: 19932 [startup+560.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4341 0 0 0 55975 24 0 0 25 0 1 0 480753407 20410368 4318 4294967295 134512640 134672761 3221224560 3221223696 134560560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4983 4318 603 41 0 4942 0 vsize: 19932 [startup+570.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4350 0 0 0 56976 24 0 0 25 0 1 0 480753407 20606976 4327 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5031 4327 603 41 0 4990 0 vsize: 20124 [startup+580.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4352 0 0 0 57976 24 0 0 25 0 1 0 480753407 20606976 4329 4294967295 134512640 134672761 3221224560 3221223724 134561028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5031 4329 603 41 0 4990 0 vsize: 20124 [startup+590.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4376 0 0 0 58976 24 0 0 25 0 1 0 480753407 20606976 4353 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5031 4353 603 41 0 4990 0 vsize: 20124 [startup+600.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 59976 24 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5079 4369 603 41 0 5038 0 vsize: 20316 [startup+610.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 60976 25 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5079 4369 603 41 0 5038 0 vsize: 20316 [startup+620.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 61976 25 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5079 4369 603 41 0 5038 0 vsize: 20316 [startup+630.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 62976 25 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5079 4369 603 41 0 5038 0 vsize: 20316 [startup+640.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4392 0 0 0 63976 25 0 0 25 0 1 0 480753407 20803584 4369 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5079 4369 603 41 0 5038 0 vsize: 20316 [startup+650.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4407 0 0 0 64976 25 0 0 25 0 1 0 480753407 20803584 4384 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5079 4384 603 41 0 5038 0 vsize: 20316 [startup+660.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4408 0 0 0 65976 25 0 0 25 0 1 0 480753407 20803584 4385 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5079 4385 603 41 0 5038 0 vsize: 20316 [startup+670.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4419 0 0 0 66977 25 0 0 25 0 1 0 480753407 20967424 4396 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5119 4396 603 41 0 5078 0 vsize: 20476 [startup+680.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4428 0 0 0 67977 25 0 0 25 0 1 0 480753407 20967424 4405 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5119 4405 603 41 0 5078 0 vsize: 20476 [startup+690.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4429 0 0 0 68977 25 0 0 25 0 1 0 480753407 20967424 4406 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5119 4406 603 41 0 5078 0 vsize: 20476 [startup+700.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 69977 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5119 4413 603 41 0 5078 0 vsize: 20476 [startup+710.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 70977 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5119 4413 603 41 0 5078 0 vsize: 20476 [startup+720.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 71977 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223744 134558768 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5119 4413 603 41 0 5078 0 vsize: 20476 [startup+730.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29018 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 72978 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5119 4413 603 41 0 5078 0 vsize: 20476 [startup+740.023 s] Raw data (loadavg): 1.22 1.02 0.93 2/57 29067 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4436 0 0 0 73978 25 0 0 25 0 1 0 480753407 20967424 4413 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5119 4413 603 41 0 5078 0 vsize: 20476 [startup+750.022 s] Raw data (loadavg): 1.19 1.02 0.93 2/54 29071 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4588 0 0 0 74978 26 0 0 25 0 1 0 480753407 21635072 4565 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5282 4565 603 41 0 5241 0 vsize: 21128 [startup+760.022 s] Raw data (loadavg): 1.16 1.02 0.93 2/54 29071 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4755 0 0 0 75978 26 0 0 25 0 1 0 480753407 22298624 4732 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5444 4732 603 41 0 5403 0 vsize: 21776 [startup+770.022 s] Raw data (loadavg): 1.13 1.02 0.93 2/54 29071 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4762 0 0 0 76978 26 0 0 25 0 1 0 480753407 22437888 4739 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5478 4739 603 41 0 5437 0 vsize: 21912 [startup+780.021 s] Raw data (loadavg): 1.11 1.02 0.93 2/54 29071 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4765 0 0 0 77978 26 0 0 25 0 1 0 480753407 22437888 4742 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5478 4742 603 41 0 5437 0 vsize: 21912 [startup+790.021 s] Raw data (loadavg): 1.09 1.02 0.93 2/54 29071 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4771 0 0 0 78978 26 0 0 25 0 1 0 480753407 22437888 4748 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5478 4748 603 41 0 5437 0 vsize: 21912 [startup+800.021 s] Raw data (loadavg): 1.08 1.01 0.93 2/54 29071 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4796 0 0 0 79978 26 0 0 25 0 1 0 480753407 22618112 4773 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4773 603 41 0 5481 0 vsize: 22088 [startup+810.022 s] Raw data (loadavg): 1.07 1.01 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4813 0 0 0 80978 26 0 0 25 0 1 0 480753407 22618112 4790 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4790 603 41 0 5481 0 vsize: 22088 [startup+820.021 s] Raw data (loadavg): 1.06 1.01 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4824 0 0 0 81978 26 0 0 25 0 1 0 480753407 22618112 4801 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4801 603 41 0 5481 0 vsize: 22088 [startup+830.021 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4826 0 0 0 82978 26 0 0 25 0 1 0 480753407 22618112 4803 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4803 603 41 0 5481 0 vsize: 22088 [startup+840.021 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4827 0 0 0 83978 26 0 0 25 0 1 0 480753407 22618112 4804 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4804 603 41 0 5481 0 vsize: 22088 [startup+850.02 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4829 0 0 0 84979 26 0 0 25 0 1 0 480753407 22618112 4806 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4806 603 41 0 5481 0 vsize: 22088 [startup+860.021 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4829 0 0 0 85979 26 0 0 25 0 1 0 480753407 22618112 4806 4294967295 134512640 134672761 3221224560 3221223664 134554665 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4806 603 41 0 5481 0 vsize: 22088 [startup+870.021 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4829 0 0 0 86979 26 0 0 25 0 1 0 480753407 22618112 4806 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4806 603 41 0 5481 0 vsize: 22088 [startup+880.021 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4830 0 0 0 87979 26 0 0 25 0 1 0 480753407 22618112 4807 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4807 603 41 0 5481 0 vsize: 22088 [startup+890.021 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4830 0 0 0 88979 26 0 0 25 0 1 0 480753407 22618112 4807 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5522 4807 603 41 0 5481 0 vsize: 22088 [startup+900.021 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4862 0 0 0 89979 26 0 0 25 0 1 0 480753407 22781952 4839 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5562 4839 603 41 0 5521 0 vsize: 22248 [startup+910.021 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 4885 0 0 0 90978 27 0 0 25 0 1 0 480753407 22913024 4862 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5594 4862 603 41 0 5553 0 vsize: 22376 [startup+920.021 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5049 0 0 0 91978 27 0 0 25 0 1 0 480753407 23588864 5026 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5759 5026 603 41 0 5718 0 vsize: 23036 [startup+930.021 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5181 0 0 0 92978 28 0 0 25 0 1 0 480753407 24248320 5158 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5920 5158 603 41 0 5879 0 vsize: 23680 [startup+940.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5204 0 0 0 93978 28 0 0 25 0 1 0 480753407 24391680 5181 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5955 5181 603 41 0 5914 0 vsize: 23820 [startup+950.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5207 0 0 0 94978 28 0 0 25 0 1 0 480753407 24391680 5184 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5955 5184 603 41 0 5914 0 vsize: 23820 [startup+960.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5207 0 0 0 95978 28 0 0 25 0 1 0 480753407 24391680 5184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5955 5184 603 41 0 5914 0 vsize: 23820 [startup+970.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5212 0 0 0 96978 28 0 0 25 0 1 0 480753407 24391680 5189 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5955 5189 603 41 0 5914 0 vsize: 23820 [startup+980.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5350 0 0 0 97978 28 0 0 25 0 1 0 480753407 25063424 5327 4294967295 134512640 134672761 3221224560 3221223744 134559182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6119 5327 603 41 0 6078 0 vsize: 24476 [startup+990.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5608 0 0 0 98977 29 0 0 25 0 1 0 480753407 26001408 5585 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6348 5585 603 41 0 6307 0 vsize: 25392 [startup+1000.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5636 0 0 0 99977 30 0 0 25 0 1 0 480753407 26132480 5613 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6380 5613 603 41 0 6339 0 vsize: 25520 [startup+1010.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5636 0 0 0 100977 30 0 0 25 0 1 0 480753407 26132480 5613 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6380 5613 603 41 0 6339 0 vsize: 25520 [startup+1020.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5636 0 0 0 101977 30 0 0 25 0 1 0 480753407 26132480 5613 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6380 5613 603 41 0 6339 0 vsize: 25520 [startup+1030.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5637 0 0 0 102978 30 0 0 25 0 1 0 480753407 26132480 5614 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6380 5614 603 41 0 6339 0 vsize: 25520 [startup+1040.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5676 0 0 0 103978 30 0 0 25 0 1 0 480753407 26304512 5653 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6422 5653 603 41 0 6381 0 vsize: 25688 [startup+1050.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 5850 0 0 0 104977 30 0 0 25 0 1 0 480753407 27107328 5827 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6618 5827 603 41 0 6577 0 vsize: 26472 [startup+1060.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6050 0 0 0 105977 31 0 0 25 0 1 0 480753407 27934720 6027 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6820 6027 603 41 0 6779 0 vsize: 27280 [startup+1070.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29073 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6050 0 0 0 106977 31 0 0 25 0 1 0 480753407 27934720 6027 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6820 6027 603 41 0 6779 0 vsize: 27280 [startup+1080.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6050 0 0 0 107977 31 0 0 25 0 1 0 480753407 27934720 6027 4294967295 134512640 134672761 3221224560 3221223760 134557915 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6820 6027 603 41 0 6779 0 vsize: 27280 [startup+1090.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6055 0 0 0 108977 31 0 0 25 0 1 0 480753407 27934720 6032 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6820 6032 603 41 0 6779 0 vsize: 27280 [startup+1100.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6055 0 0 0 109977 31 0 0 25 0 1 0 480753407 27934720 6032 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6820 6032 603 41 0 6779 0 vsize: 27280 [startup+1110.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6060 0 0 0 110977 31 0 0 25 0 1 0 480753407 27934720 6037 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6820 6037 603 41 0 6779 0 vsize: 27280 [startup+1120.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6074 0 0 0 111977 31 0 0 25 0 1 0 480753407 28123136 6051 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6866 6051 603 41 0 6825 0 vsize: 27464 [startup+1130.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6074 0 0 0 112978 31 0 0 25 0 1 0 480753407 28123136 6051 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6866 6051 603 41 0 6825 0 vsize: 27464 [startup+1140.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6075 0 0 0 113978 31 0 0 25 0 1 0 480753407 28123136 6052 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6866 6052 603 41 0 6825 0 vsize: 27464 [startup+1150.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6085 0 0 0 114978 31 0 0 25 0 1 0 480753407 28123136 6062 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6866 6062 603 41 0 6825 0 vsize: 27464 [startup+1160.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6095 0 0 0 115978 31 0 0 25 0 1 0 480753407 28123136 6072 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6866 6072 603 41 0 6825 0 vsize: 27464 [startup+1170.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6098 0 0 0 116978 32 0 0 25 0 1 0 480753407 28123136 6075 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6866 6075 603 41 0 6825 0 vsize: 27464 [startup+1180.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6099 0 0 0 117978 32 0 0 25 0 1 0 480753407 28123136 6076 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6866 6076 603 41 0 6825 0 vsize: 27464 [startup+1190.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6099 0 0 0 118978 32 0 0 25 0 1 0 480753407 28123136 6076 4294967295 134512640 134672761 3221224560 3221223664 134559916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6866 6076 603 41 0 6825 0 vsize: 27464 [startup+1200.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 29075 Raw data (stat): 29018 (minisat+) R 29017 22612 22611 0 -1 0 6099 0 0 0 119978 32 0 0 25 0 1 0 480753407 28123136 6076 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6866 6076 603 41 0 6825 0 vsize: 27464 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.04 s] Raw data (loadavg): 1.00 1.00 0.93 1/54 29075 Raw data (stat): 29018 (minisat+) Z 29017 22612 22611 0 -1 12 6102 0 0 0 119978 33 0 0 25 0 1 0 480753407 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: 10 Real time (s): 1200.04 CPU time (s): 1200.12 CPU user time (s): 1199.79 CPU system time (s): 0.334949 CPU usage (%): 100.007 Max. virtual memory (Kb): 27464 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####