Name | normalized-opb/submitted/manquinho/logic-synthesis/normalized-f51m.b.opb |
MD5SUM | 4fc22abde8250807abd95442a25fac44 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 18 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 407 |
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 | 407 |
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 | 407 |
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.02684 |
Number of variables | 406 |
Total number of constraints | 538 |
Number of constraints which are clauses | 520 |
Number of constraints which are cardinality constraints (but not clauses) | 18 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 123 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc2 THE 2005-04-14 03:41:05 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4581 boxname=wulflinc2 idbench=69 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4fc22abde8250807abd95442a25fac44 /oldhome/oroussel/tmp/wulflinc2/normalized-f51m.b.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-f51m.b.opb /oldhome/oroussel/tmp/wulflinc2/normalized-f51m.b.opb IDLAUNCH: 4581 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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.191 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: 893696 kB Buffers: 35516 kB Cached: 84840 kB SwapCached: 4 kB Active: 58136 kB Inactive: 65088 kB HighTotal: 131008 kB HighFree: 42364 kB LowTotal: 903652 kB LowFree: 851332 kB SwapTotal: 2097136 kB SwapFree: 2097132 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6916 kB Slab: 12132 kB Committed_AS: 71676 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 04:01:07 (client local time) WITH STATUS 10 IN 1200.16 SECONDS stats: 4581 7 1200.16 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 498 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 | 498 13351 | 166 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 26[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:14920 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1 | 32445 88186 | 10815 1 18 18.0 | 0.000 % | c | 101 | 32445 88186 | 11896 101 634 6.3 | 0.055 % | c | 251 | 32430 88150 | 13086 250 3216 12.9 | 0.083 % | c | 476 | 32419 88126 | 14394 474 4850 10.2 | 0.110 % | c | 816 | 32419 88126 | 15834 814 16091 19.8 | 0.110 % | c ============================================================================== c [1mFound solution: 25[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 | 1205 | 32375 88025 | 10791 1202 21345 17.8 | 0.110 % | c | 1307 | 32375 88025 | 11870 1304 22745 17.4 | 0.266 % | c | 1458 | 32302 87862 | 13057 1369 23099 16.9 | 0.449 % | c | 1683 | 32302 87862 | 14362 1594 31156 19.5 | 0.449 % | c | 2020 | 32302 87862 | 15799 1931 44330 23.0 | 0.449 % | c ============================================================================== c [1mFound solution: 24[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 | 2184 | 32330 87933 | 10776 2095 47803 22.8 | 0.449 % | c | 2284 | 32330 87933 | 11853 2195 50493 23.0 | 0.467 % | c | 2434 | 32330 87933 | 13038 2345 52068 22.2 | 0.467 % | c | 2660 | 32207 87658 | 14342 2425 52611 21.7 | 0.778 % | c | 2997 | 32207 87658 | 15777 2762 75546 27.4 | 0.778 % | c ============================================================================== c [1mFound solution: 23[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 | 3307 | 27823 77625 | 9274 2752 72417 26.3 | 0.778 % | c | 3407 | 27784 77538 | 10201 2851 74418 26.1 | 12.913 % | c | 3561 | 27784 77538 | 11221 3005 79103 26.3 | 12.913 % | c ============================================================================== c [1mFound solution: 22[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 | 3695 | 27811 77606 | 9270 3139 85648 27.3 | 12.913 % | c | 3796 | 27811 77606 | 10197 3240 88815 27.4 | 12.911 % | c ============================================================================== c [1mFound solution: 21[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 | 3937 | 27780 77523 | 9260 3283 94010 28.6 | 12.911 % | c | 4038 | 27780 77523 | 10186 3384 101422 30.0 | 13.030 % | c | 4188 | 27780 77523 | 11204 3534 108295 30.6 | 13.028 % | c ============================================================================== c [1mFound solution: 20[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 | 4213 | 27803 77580 | 9267 3559 109846 30.9 | 13.028 % | c | 4315 | 27803 77580 | 10193 3661 114004 31.1 | 13.036 % | c | 4467 | 27803 77580 | 11213 3813 120687 31.7 | 13.036 % | c | 4692 | 27803 77580 | 12334 4038 131801 32.6 | 13.036 % | c | 5029 | 27803 77580 | 13567 4375 148244 33.9 | 13.036 % | c | 5535 | 27803 77580 | 14924 4881 167957 34.4 | 13.036 % | c | 6294 | 27803 77580 | 16417 5640 221295 39.2 | 13.036 % | c | 7433 | 27803 77580 | 18058 6779 298159 44.0 | 13.036 % | c | 9141 | 27803 77580 | 19864 8487 374760 44.2 | 13.036 % | c | 11703 | 27803 77580 | 21851 11049 481722 43.6 | 13.036 % | c ============================================================================== c [1mFound solution: 19[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 | 13211 | 27463 76774 | 9154 12212 523652 42.9 | 13.036 % | c | 13312 | 27463 76774 | 10069 6207 222101 35.8 | 14.047 % | c | 13462 | 27463 76774 | 11076 6357 229393 36.1 | 14.047 % | c | 13687 | 27463 76774 | 12183 6582 240050 36.5 | 14.047 % | c | 14024 | 27463 76774 | 13402 6919 253868 36.7 | 14.047 % | c | 14532 | 27463 76774 | 14742 7427 276080 37.2 | 14.047 % | c | 15292 | 27463 76774 | 16216 8187 307132 37.5 | 14.047 % | c | 16433 | 27463 76774 | 17838 9328 353593 37.9 | 14.047 % | c | 18143 | 27463 76774 | 19622 11038 409460 37.1 | 14.047 % | c | 20706 | 27463 76774 | 21584 13601 532070 39.1 | 14.047 % | c | 24553 | 27463 76774 | 23743 17448 684730 39.2 | 14.047 % | c | 30319 | 27463 76774 | 26117 23214 936867 40.4 | 14.047 % | c | 38968 | 27463 76774 | 28729 14420 580313 40.2 | 14.047 % | c ============================================================================== c [1mFound solution: 18[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 | 41503 | 27485 76828 | 9161 16955 682680 40.3 | 14.047 % | c | 41604 | 27485 76828 | 10077 8579 312700 36.4 | 14.046 % | c | 41755 | 27485 76828 | 11084 8730 317676 36.4 | 14.046 % | c | 41982 | 27485 76828 | 12193 8957 325192 36.3 | 14.046 % | c | 42328 | 27485 76828 | 13412 9303 338520 36.4 | 14.046 % | c | 42834 | 27485 76828 | 14753 9809 355907 36.3 | 14.046 % | c | 43593 | 27485 76828 | 16229 10568 380258 36.0 | 14.046 % | c | 44733 | 27485 76828 | 17852 11708 418476 35.7 | 14.046 % | c | 46444 | 27485 76828 | 19637 13419 471610 35.1 | 14.046 % | c | 49007 | 27485 76828 | 21601 15982 553496 34.6 | 14.046 % | c | 52852 | 27485 76828 | 23761 19827 658033 33.2 | 14.046 % | c | 58618 | 27485 76828 | 26137 25593 854059 33.4 | 14.046 % | c | 67268 | 27485 76828 | 28751 18563 557689 30.0 | 14.046 % | c | 80242 | 27485 76828 | 31626 31537 999852 31.7 | 14.046 % | c | 99703 | 27442 76729 | 34788 33262 1026630 30.9 | 14.174 % | c | 128898 | 27442 76729 | 38267 18508 645811 34.9 | 14.174 % | c | 172688 | 27442 76729 | 42094 34799 1260627 36.2 | 14.174 % | c | 238373 | 27371 76565 | 46304 41184 1139588 27.7 | 14.374 % | c | 336899 | 27312 76425 | 50934 37922 1051365 27.7 | 14.539 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.92 0.97 0.91 2/54 26335 Raw data (stat): 26335 (runsolver) R 26334 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423208750 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0007 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 1472 0 0 0 995 3 0 0 25 0 1 0 423208750 7999488 1446 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1953 1446 603 41 0 1912 0 vsize: 7812 [startup+20.0008 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 1796 0 0 0 1994 4 0 0 25 0 1 0 423208750 9338880 1770 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2280 1770 603 41 0 2239 0 vsize: 9120 [startup+30.0004 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 1979 0 0 0 2992 5 0 0 25 0 1 0 423208750 10096640 1953 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2465 1953 603 41 0 2424 0 vsize: 9860 [startup+40.0015 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 1979 0 0 0 3992 5 0 0 25 0 1 0 423208750 10096640 1953 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2465 1953 603 41 0 2424 0 vsize: 9860 [startup+50.0019 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2087 0 0 0 4992 5 0 0 25 0 1 0 423208750 10502144 2061 4294967295 134512640 134672761 3221224576 3221223712 134560608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2564 2061 603 41 0 2523 0 vsize: 10256 [startup+60.0015 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2250 0 0 0 5992 6 0 0 25 0 1 0 423208750 11198464 2224 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2734 2224 603 41 0 2693 0 vsize: 10936 [startup+70.0026 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2450 0 0 0 6992 6 0 0 25 0 1 0 423208750 12001280 2424 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2930 2424 603 41 0 2889 0 vsize: 11720 [startup+80.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2664 0 0 0 7991 8 0 0 25 0 1 0 423208750 12943360 2638 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3160 2638 603 41 0 3119 0 vsize: 12640 [startup+90.0037 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2854 0 0 0 8991 8 0 0 25 0 1 0 423208750 13758464 2828 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3359 2828 603 41 0 3318 0 vsize: 13436 [startup+100.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 2990 0 0 0 9990 9 0 0 25 0 1 0 423208750 14295040 2964 4294967295 134512640 134672761 3221224576 3221223744 134561269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3490 2964 603 41 0 3449 0 vsize: 13960 [startup+110.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3015 0 0 0 10989 9 0 0 25 0 1 0 423208750 14450688 2989 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3528 2989 603 41 0 3487 0 vsize: 14112 [startup+120.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3031 0 0 0 11989 9 0 0 25 0 1 0 423208750 14450688 3005 4294967295 134512640 134672761 3221224576 3221223760 134559590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3528 3005 603 41 0 3487 0 vsize: 14112 [startup+130.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3047 0 0 0 12989 9 0 0 25 0 1 0 423208750 14598144 3021 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3564 3021 603 41 0 3523 0 vsize: 14256 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3056 0 0 0 13989 9 0 0 25 0 1 0 423208750 14598144 3030 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3564 3030 603 41 0 3523 0 vsize: 14256 [startup+150.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3096 0 0 0 14990 9 0 0 25 0 1 0 423208750 14745600 3070 4294967295 134512640 134672761 3221224576 3221223760 134558923 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3600 3070 603 41 0 3559 0 vsize: 14400 [startup+160.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3100 0 0 0 15990 9 0 0 25 0 1 0 423208750 14745600 3074 4294967295 134512640 134672761 3221224576 3221223712 134560657 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3600 3074 603 41 0 3559 0 vsize: 14400 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3137 0 0 0 16990 10 0 0 25 0 1 0 423208750 14942208 3111 4294967295 134512640 134672761 3221224576 3221223680 134555211 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3648 3111 603 41 0 3607 0 vsize: 14592 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3154 0 0 0 17990 10 0 0 25 0 1 0 423208750 15138816 3128 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3696 3128 603 41 0 3655 0 vsize: 14784 [startup+190.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3154 0 0 0 18990 10 0 0 25 0 1 0 423208750 15138816 3128 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3696 3128 603 41 0 3655 0 vsize: 14784 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3155 0 0 0 19990 10 0 0 25 0 1 0 423208750 15138816 3129 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3696 3129 603 41 0 3655 0 vsize: 14784 [startup+210.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3162 0 0 0 20990 10 0 0 25 0 1 0 423208750 15138816 3136 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3696 3136 603 41 0 3655 0 vsize: 14784 [startup+220.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3164 0 0 0 21990 10 0 0 25 0 1 0 423208750 15138816 3138 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3696 3138 603 41 0 3655 0 vsize: 14784 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3191 0 0 0 22991 10 0 0 25 0 1 0 423208750 15335424 3165 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3744 3165 603 41 0 3703 0 vsize: 14976 [startup+240.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 23990 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223680 134554662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3808 3227 603 41 0 3767 0 vsize: 15232 [startup+250.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 24991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3808 3227 603 41 0 3767 0 vsize: 15232 [startup+260.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 25991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3808 3227 603 41 0 3767 0 vsize: 15232 [startup+270.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 26991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223760 134558332 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3808 3227 603 41 0 3767 0 vsize: 15232 [startup+280.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 27991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3808 3227 603 41 0 3767 0 vsize: 15232 [startup+290.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3253 0 0 0 28991 10 0 0 25 0 1 0 423208750 15597568 3227 4294967295 134512640 134672761 3221224576 3221223744 134561278 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3808 3227 603 41 0 3767 0 vsize: 15232 [startup+300.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3256 0 0 0 29991 10 0 0 25 0 1 0 423208750 15597568 3230 4294967295 134512640 134672761 3221224576 3221223700 134566059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3808 3230 603 41 0 3767 0 vsize: 15232 [startup+310.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3258 0 0 0 30992 10 0 0 25 0 1 0 423208750 15597568 3232 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3808 3232 603 41 0 3767 0 vsize: 15232 [startup+320.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3274 0 0 0 31990 11 0 0 25 0 1 0 423208750 15794176 3248 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3856 3248 603 41 0 3815 0 vsize: 15424 [startup+330.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3274 0 0 0 32990 11 0 0 25 0 1 0 423208750 15794176 3248 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3856 3248 603 41 0 3815 0 vsize: 15424 [startup+340.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3285 0 0 0 33990 11 0 0 25 0 1 0 423208750 15794176 3259 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3856 3259 603 41 0 3815 0 vsize: 15424 [startup+350.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3286 0 0 0 34990 11 0 0 25 0 1 0 423208750 15794176 3260 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3856 3260 603 41 0 3815 0 vsize: 15424 [startup+360.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3287 0 0 0 35990 11 0 0 25 0 1 0 423208750 15794176 3261 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3856 3261 603 41 0 3815 0 vsize: 15424 [startup+370.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3318 0 0 0 36990 11 0 0 25 0 1 0 423208750 15929344 3292 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3889 3292 603 41 0 3848 0 vsize: 15556 [startup+380.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3321 0 0 0 37991 11 0 0 25 0 1 0 423208750 15929344 3295 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3889 3295 603 41 0 3848 0 vsize: 15556 [startup+390.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3321 0 0 0 38991 11 0 0 25 0 1 0 423208750 15929344 3295 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3889 3295 603 41 0 3848 0 vsize: 15556 [startup+400.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3332 0 0 0 39991 11 0 0 25 0 1 0 423208750 16064512 3306 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3922 3306 603 41 0 3881 0 vsize: 15688 [startup+410.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3332 0 0 0 40991 11 0 0 25 0 1 0 423208750 16064512 3306 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3922 3306 603 41 0 3881 0 vsize: 15688 [startup+420.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3334 0 0 0 41991 11 0 0 25 0 1 0 423208750 16064512 3308 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3922 3308 603 41 0 3881 0 vsize: 15688 [startup+430.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3432 0 0 0 42991 11 0 0 25 0 1 0 423208750 16347136 3406 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3991 3406 603 41 0 3950 0 vsize: 15964 [startup+440.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3550 0 0 0 43991 11 0 0 25 0 1 0 423208750 16879616 3524 4294967295 134512640 134672761 3221224576 3221223776 134557796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4121 3524 603 41 0 4080 0 vsize: 16484 [startup+450.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3703 0 0 0 44990 12 0 0 25 0 1 0 423208750 17547264 3677 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4284 3677 603 41 0 4243 0 vsize: 17136 [startup+460.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3822 0 0 0 45990 13 0 0 25 0 1 0 423208750 17944576 3796 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4381 3796 603 41 0 4340 0 vsize: 17524 [startup+470.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3829 0 0 0 46991 13 0 0 25 0 1 0 423208750 18079744 3803 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4414 3803 603 41 0 4373 0 vsize: 17656 [startup+480.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3841 0 0 0 47991 13 0 0 25 0 1 0 423208750 18079744 3815 4294967295 134512640 134672761 3221224576 3221223760 134558937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4414 3815 603 41 0 4373 0 vsize: 17656 [startup+490.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3842 0 0 0 48991 13 0 0 25 0 1 0 423208750 18079744 3816 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4414 3816 603 41 0 4373 0 vsize: 17656 [startup+500.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3845 0 0 0 49991 13 0 0 25 0 1 0 423208750 18079744 3819 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4414 3819 603 41 0 4373 0 vsize: 17656 [startup+510.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3846 0 0 0 50991 13 0 0 25 0 1 0 423208750 18079744 3820 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4414 3820 603 41 0 4373 0 vsize: 17656 [startup+520.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3866 0 0 0 51990 13 0 0 25 0 1 0 423208750 18227200 3840 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4450 3840 603 41 0 4409 0 vsize: 17800 [startup+530.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3878 0 0 0 52990 13 0 0 25 0 1 0 423208750 18227200 3852 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4450 3852 603 41 0 4409 0 vsize: 17800 [startup+540.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3887 0 0 0 53990 13 0 0 25 0 1 0 423208750 18227200 3861 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4450 3861 603 41 0 4409 0 vsize: 17800 [startup+550.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3901 0 0 0 54991 13 0 0 25 0 1 0 423208750 18227200 3875 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4450 3875 603 41 0 4409 0 vsize: 17800 [startup+560.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3901 0 0 0 55991 13 0 0 25 0 1 0 423208750 18227200 3875 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4450 3875 603 41 0 4409 0 vsize: 17800 [startup+570.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3906 0 0 0 56991 13 0 0 25 0 1 0 423208750 18391040 3880 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3880 603 41 0 4449 0 vsize: 17960 [startup+580.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3911 0 0 0 57991 13 0 0 25 0 1 0 423208750 18391040 3885 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3885 603 41 0 4449 0 vsize: 17960 [startup+590.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3917 0 0 0 58992 13 0 0 25 0 1 0 423208750 18391040 3891 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3891 603 41 0 4449 0 vsize: 17960 [startup+600.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3918 0 0 0 59992 13 0 0 25 0 1 0 423208750 18391040 3892 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3892 603 41 0 4449 0 vsize: 17960 [startup+610.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3920 0 0 0 60992 13 0 0 25 0 1 0 423208750 18391040 3894 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3894 603 41 0 4449 0 vsize: 17960 [startup+620.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3921 0 0 0 61992 13 0 0 25 0 1 0 423208750 18391040 3895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3895 603 41 0 4449 0 vsize: 17960 [startup+630.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3921 0 0 0 62992 13 0 0 25 0 1 0 423208750 18391040 3895 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3895 603 41 0 4449 0 vsize: 17960 [startup+640.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3921 0 0 0 63992 13 0 0 25 0 1 0 423208750 18391040 3895 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3895 603 41 0 4449 0 vsize: 17960 [startup+650.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 64993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3901 603 41 0 4449 0 vsize: 17960 [startup+660.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 65993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3901 603 41 0 4449 0 vsize: 17960 [startup+670.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 66993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3901 603 41 0 4449 0 vsize: 17960 [startup+680.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 67993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3901 603 41 0 4449 0 vsize: 17960 [startup+690.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 68993 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3901 603 41 0 4449 0 vsize: 17960 [startup+700.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 69994 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3901 603 41 0 4449 0 vsize: 17960 [startup+710.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 70994 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3901 603 41 0 4449 0 vsize: 17960 [startup+720.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3927 0 0 0 71994 13 0 0 25 0 1 0 423208750 18391040 3901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4490 3901 603 41 0 4449 0 vsize: 17960 [startup+730.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3945 0 0 0 72994 14 0 0 25 0 1 0 423208750 18554880 3919 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4530 3919 603 41 0 4489 0 vsize: 18120 [startup+740.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3949 0 0 0 73993 14 0 0 25 0 1 0 423208750 18554880 3923 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3923 603 41 0 4489 0 vsize: 18120 [startup+750.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3952 0 0 0 74994 14 0 0 25 0 1 0 423208750 18554880 3926 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3926 603 41 0 4489 0 vsize: 18120 [startup+760.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 75994 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3928 603 41 0 4489 0 vsize: 18120 [startup+770.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 76994 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3928 603 41 0 4489 0 vsize: 18120 [startup+780.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 77994 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3928 603 41 0 4489 0 vsize: 18120 [startup+790.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 78994 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3928 603 41 0 4489 0 vsize: 18120 [startup+800.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3954 0 0 0 79995 14 0 0 25 0 1 0 423208750 18554880 3928 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3928 603 41 0 4489 0 vsize: 18120 [startup+810.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3955 0 0 0 80995 14 0 0 25 0 1 0 423208750 18554880 3929 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3929 603 41 0 4489 0 vsize: 18120 [startup+820.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3955 0 0 0 81995 14 0 0 25 0 1 0 423208750 18554880 3929 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3929 603 41 0 4489 0 vsize: 18120 [startup+830.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3961 0 0 0 82995 14 0 0 25 0 1 0 423208750 18554880 3935 4294967295 134512640 134672761 3221224576 3221223776 134557892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3935 603 41 0 4489 0 vsize: 18120 [startup+840.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3969 0 0 0 83995 14 0 0 25 0 1 0 423208750 18554880 3943 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3943 603 41 0 4489 0 vsize: 18120 [startup+850.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3969 0 0 0 84995 14 0 0 25 0 1 0 423208750 18554880 3943 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4530 3943 603 41 0 4489 0 vsize: 18120 [startup+860.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 3982 0 0 0 85996 14 0 0 25 0 1 0 423208750 18751488 3956 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4578 3956 603 41 0 4537 0 vsize: 18312 [startup+870.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4048 0 0 0 86996 14 0 0 25 0 1 0 423208750 19030016 4022 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4646 4022 603 41 0 4605 0 vsize: 18584 [startup+880.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 87996 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4646 4026 603 41 0 4605 0 vsize: 18584 [startup+890.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 88996 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134561261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4646 4026 603 41 0 4605 0 vsize: 18584 [startup+900.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 89996 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4646 4026 603 41 0 4605 0 vsize: 18584 [startup+910.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 90996 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4646 4026 603 41 0 4605 0 vsize: 18584 [startup+920.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4052 0 0 0 91997 14 0 0 25 0 1 0 423208750 19030016 4026 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4646 4026 603 41 0 4605 0 vsize: 18584 [startup+930.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4058 0 0 0 92997 14 0 0 25 0 1 0 423208750 19030016 4032 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4646 4032 603 41 0 4605 0 vsize: 18584 [startup+940.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4058 0 0 0 93997 14 0 0 25 0 1 0 423208750 19030016 4032 4294967295 134512640 134672761 3221224576 3221223712 134560619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4646 4032 603 41 0 4605 0 vsize: 18584 [startup+950.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4058 0 0 0 94997 14 0 0 25 0 1 0 423208750 19030016 4032 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4646 4032 603 41 0 4605 0 vsize: 18584 [startup+960.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4071 0 0 0 95997 14 0 0 25 0 1 0 423208750 19177472 4045 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4045 603 41 0 4641 0 vsize: 18728 [startup+970.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 96997 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4050 603 41 0 4641 0 vsize: 18728 [startup+980.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 97997 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4050 603 41 0 4641 0 vsize: 18728 [startup+990.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 98998 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4050 603 41 0 4641 0 vsize: 18728 [startup+1000.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 99998 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223760 134559572 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4050 603 41 0 4641 0 vsize: 18728 [startup+1010.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 100998 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4050 603 41 0 4641 0 vsize: 18728 [startup+1020.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4076 0 0 0 101998 14 0 0 25 0 1 0 423208750 19177472 4050 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4050 603 41 0 4641 0 vsize: 18728 [startup+1030.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4088 0 0 0 102998 14 0 0 25 0 1 0 423208750 19177472 4062 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4682 4062 603 41 0 4641 0 vsize: 18728 [startup+1040.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4088 0 0 0 103997 14 0 0 25 0 1 0 423208750 19177472 4062 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4062 603 41 0 4641 0 vsize: 18728 [startup+1050.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4091 0 0 0 104997 14 0 0 25 0 1 0 423208750 19177472 4065 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4065 603 41 0 4641 0 vsize: 18728 [startup+1060.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4091 0 0 0 105997 14 0 0 25 0 1 0 423208750 19177472 4065 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4065 603 41 0 4641 0 vsize: 18728 [startup+1070.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4101 0 0 0 106997 15 0 0 25 0 1 0 423208750 19324928 4075 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4718 4075 603 41 0 4677 0 vsize: 18872 [startup+1080.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4104 0 0 0 107997 15 0 0 25 0 1 0 423208750 19324928 4078 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4718 4078 603 41 0 4677 0 vsize: 18872 [startup+1090.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4107 0 0 0 108998 15 0 0 25 0 1 0 423208750 19324928 4081 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4718 4081 603 41 0 4677 0 vsize: 18872 [startup+1100.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4108 0 0 0 109998 15 0 0 25 0 1 0 423208750 19324928 4082 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4718 4082 603 41 0 4677 0 vsize: 18872 [startup+1110.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4108 0 0 0 110998 15 0 0 25 0 1 0 423208750 19324928 4082 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4718 4082 603 41 0 4677 0 vsize: 18872 [startup+1120.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4108 0 0 0 111998 15 0 0 25 0 1 0 423208750 19324928 4082 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4718 4082 603 41 0 4677 0 vsize: 18872 [startup+1130.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 26335 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4108 0 0 0 112999 15 0 0 25 0 1 0 423208750 19324928 4082 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4718 4082 603 41 0 4677 0 vsize: 18872 [startup+1140.02 s] Raw data (loadavg): 1.07 0.99 0.92 2/57 26338 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4116 0 0 0 113999 15 0 0 25 0 1 0 423208750 19324928 4090 4294967295 134512640 134672761 3221224576 3221223712 134560585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4718 4090 603 41 0 4677 0 vsize: 18872 [startup+1150.02 s] Raw data (loadavg): 1.14 1.00 0.93 2/54 26388 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4117 0 0 0 114999 15 0 0 25 0 1 0 423208750 19324928 4091 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4718 4091 603 41 0 4677 0 vsize: 18872 [startup+1160.02 s] Raw data (loadavg): 1.11 1.00 0.93 2/54 26388 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4136 0 0 0 115999 15 0 0 25 0 1 0 423208750 19505152 4110 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4762 4110 603 41 0 4721 0 vsize: 19048 [startup+1170.02 s] Raw data (loadavg): 1.10 1.00 0.93 2/54 26388 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4137 0 0 0 116999 15 0 0 25 0 1 0 423208750 19505152 4111 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4762 4111 603 41 0 4721 0 vsize: 19048 [startup+1180.02 s] Raw data (loadavg): 1.08 1.00 0.93 2/54 26388 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4137 0 0 0 117999 15 0 0 25 0 1 0 423208750 19505152 4111 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4762 4111 603 41 0 4721 0 vsize: 19048 [startup+1190.02 s] Raw data (loadavg): 1.07 1.00 0.93 2/54 26388 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4158 0 0 0 118999 15 0 0 25 0 1 0 423208750 19505152 4132 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4762 4132 603 41 0 4721 0 vsize: 19048 [startup+1200.02 s] Raw data (loadavg): 1.06 1.00 0.93 2/54 26388 Raw data (stat): 26335 (minisat+) R 26334 20937 20936 0 -1 0 4160 0 0 0 119999 15 0 0 25 0 1 0 423208750 19505152 4134 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4762 4134 603 41 0 4721 0 vsize: 19048 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.03 s] Raw data (loadavg): 1.06 1.00 0.93 1/54 26388 Raw data (stat): 26335 (minisat+) Z 26334 20937 20936 0 -1 12 4163 0 0 0 119999 16 0 0 25 0 1 0 423208750 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.03 CPU time (s): 1200.16 CPU user time (s): 1200 CPU system time (s): 0.162975 CPU usage (%): 100.011 Max. virtual memory (Kb): 19048 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####