Name | normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-9symml.opb |
MD5SUM | 48809ba02390b1184dab90aed89aff8e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4517 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 651 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 28138 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 28138 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02684 |
Number of variables | 651 |
Total number of constraints | 1658 |
Number of constraints which are clauses | 1656 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 2 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 42 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc7 THE 2005-04-13 22:24:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3630 boxname=wulflinc7 idbench=246 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 48809ba02390b1184dab90aed89aff8e /oldhome/oroussel/tmp/wulflinc7/normalized-9symml.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc7/normalized-9symml.opb /oldhome/oroussel/tmp/wulflinc7/normalized-9symml.opb IDLAUNCH: 3630 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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: 905776 kB Buffers: 36712 kB Cached: 72972 kB SwapCached: 0 kB Active: 72156 kB Inactive: 40388 kB HighTotal: 131008 kB HighFree: 54180 kB LowTotal: 903652 kB LowFree: 851596 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6924 kB Slab: 10776 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 22:45:00 (client local time) WITH STATUS 10 IN 1200.21 SECONDS stats: 3630 7 1200.21 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 1579 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 | 1552 6592 | 517 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 6227[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 3328 maxlim: 21911 bits: 15/15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 24771 89507 | 8257 0 0 nan | 0.000 % | c | 101 | 24744 89434 | 9082 100 422 4.2 | 0.552 % | c | 251 | 24717 89354 | 9990 247 1016 4.1 | 0.603 % | c | 476 | 24717 89354 | 10990 472 2201 4.7 | 0.603 % | c | 813 | 24717 89354 | 12089 809 4075 5.0 | 0.603 % | c | 1319 | 24717 89354 | 13297 1315 7339 5.6 | 0.603 % | c | 2078 | 24717 89354 | 14627 2074 12073 5.8 | 0.603 % | c | 3219 | 24717 89354 | 16090 3215 38941 12.1 | 0.603 % | c | 4927 | 24717 89354 | 17699 4923 183501 37.3 | 0.603 % | c | 7489 | 24717 89354 | 19469 7485 350885 46.9 | 0.603 % | c | 11334 | 24717 89354 | 21416 11330 576503 50.9 | 0.603 % | c | 17101 | 24717 89354 | 23558 17097 984668 57.6 | 0.603 % | c | 25751 | 24717 89354 | 25914 13444 914981 68.1 | 0.603 % | c | 38726 | 24717 89354 | 28505 26419 2670115 101.1 | 0.603 % | c | 58187 | 24717 89354 | 31355 14936 1308054 87.6 | 0.603 % | c | 87379 | 24717 89354 | 34491 25385 2667043 105.1 | 0.603 % | c | 131169 | 24717 89354 | 37940 27310 2758646 101.0 | 0.603 % | c | 196853 | 24717 89354 | 41734 20355 1644708 80.8 | 0.603 % | c | 295381 | 24690 89279 | 45908 37880 5122869 135.2 | 0.628 % | c | 443170 | 24690 89279 | 50499 35203 3789405 107.6 | 0.628 % | c | 664853 | 24690 89279 | 55548 38864 6118839 157.4 | 0.628 % | #### 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.84 0.94 0.90 2/54 25828 Raw data (stat): 25828 (runsolver) R 25827 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421314266 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.0006 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 1910 0 0 0 991 6 0 0 25 0 1 0 421314266 9396224 1888 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2294 1888 603 41 0 2253 0 vsize: 9176 [startup+20.0009 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 2584 0 0 0 1989 8 0 0 25 0 1 0 421314266 12091392 2562 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2952 2562 603 41 0 2911 0 vsize: 11808 [startup+30.0018 s] Raw data (loadavg): 0.90 0.94 0.90 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 3497 0 0 0 2986 11 0 0 25 0 1 0 421314266 15855616 3475 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3871 3475 603 41 0 3830 0 vsize: 15484 [startup+40.0017 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4041 0 0 0 3984 13 0 0 25 0 1 0 421314266 18124800 4019 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4425 4019 603 41 0 4384 0 vsize: 17700 [startup+50.0028 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4107 0 0 0 4984 13 0 0 25 0 1 0 421314266 18395136 4085 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4491 4085 603 41 0 4450 0 vsize: 17964 [startup+60.0027 s] Raw data (loadavg): 0.94 0.95 0.90 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4107 0 0 0 5984 13 0 0 25 0 1 0 421314266 18395136 4085 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4491 4085 603 41 0 4450 0 vsize: 17964 [startup+70.0023 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4198 0 0 0 6984 13 0 0 25 0 1 0 421314266 18792448 4176 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4588 4176 603 41 0 4547 0 vsize: 18352 [startup+80.0026 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4198 0 0 0 7985 13 0 0 25 0 1 0 421314266 18792448 4176 4294967295 134512640 134672761 3221224576 3221223700 134566115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4588 4176 603 41 0 4547 0 vsize: 18352 [startup+90.0029 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4710 0 0 0 8983 15 0 0 25 0 1 0 421314266 20938752 4688 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5112 4688 603 41 0 5071 0 vsize: 20448 [startup+100.003 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4710 0 0 0 9983 15 0 0 25 0 1 0 421314266 20938752 4688 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5112 4688 603 41 0 5071 0 vsize: 20448 [startup+110.004 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4710 0 0 0 10984 15 0 0 25 0 1 0 421314266 20938752 4688 4294967295 134512640 134672761 3221224576 3221223532 1075349984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5112 4688 603 41 0 5071 0 vsize: 20448 [startup+120.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4710 0 0 0 11984 15 0 0 25 0 1 0 421314266 20938752 4688 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5112 4688 603 41 0 5071 0 vsize: 20448 [startup+130.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 4710 0 0 0 12984 15 0 0 25 0 1 0 421314266 20938752 4688 4294967295 134512640 134672761 3221224576 3221223532 1075349981 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5112 4688 603 41 0 5071 0 vsize: 20448 [startup+140.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 5406 0 0 0 13982 17 0 0 25 0 1 0 421314266 23748608 5384 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5798 5384 603 41 0 5757 0 vsize: 23192 [startup+150.005 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 5584 0 0 0 14982 17 0 0 25 0 1 0 421314266 24555520 5562 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5995 5562 603 41 0 5954 0 vsize: 23980 [startup+160.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 5584 0 0 0 15982 17 0 0 25 0 1 0 421314266 24555520 5562 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5995 5562 603 41 0 5954 0 vsize: 23980 [startup+170.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 5584 0 0 0 16982 17 0 0 25 0 1 0 421314266 24555520 5562 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5995 5562 603 41 0 5954 0 vsize: 23980 [startup+180.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6079 0 0 0 17981 18 0 0 25 0 1 0 421314266 26574848 6057 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6488 6057 603 41 0 6447 0 vsize: 25952 [startup+190.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6079 0 0 0 18982 18 0 0 25 0 1 0 421314266 26574848 6057 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6488 6057 603 41 0 6447 0 vsize: 25952 [startup+200.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6079 0 0 0 19982 18 0 0 25 0 1 0 421314266 26574848 6057 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6488 6057 603 41 0 6447 0 vsize: 25952 [startup+210.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6079 0 0 0 20982 18 0 0 25 0 1 0 421314266 26574848 6057 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6488 6057 603 41 0 6447 0 vsize: 25952 [startup+220.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6488 0 0 0 21981 20 0 0 25 0 1 0 421314266 28188672 6466 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6466 603 41 0 6841 0 vsize: 27528 [startup+230.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6488 0 0 0 22980 20 0 0 25 0 1 0 421314266 28188672 6466 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6466 603 41 0 6841 0 vsize: 27528 [startup+240.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6488 0 0 0 23980 20 0 0 25 0 1 0 421314266 28188672 6466 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6466 603 41 0 6841 0 vsize: 27528 [startup+250.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6491 0 0 0 24981 20 0 0 25 0 1 0 421314266 28188672 6469 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6469 603 41 0 6841 0 vsize: 27528 [startup+260.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6491 0 0 0 25981 20 0 0 25 0 1 0 421314266 28188672 6469 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6469 603 41 0 6841 0 vsize: 27528 [startup+270.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6491 0 0 0 26981 20 0 0 25 0 1 0 421314266 28188672 6469 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6469 603 41 0 6841 0 vsize: 27528 [startup+280.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6491 0 0 0 27981 20 0 0 25 0 1 0 421314266 28188672 6469 4294967295 134512640 134672761 3221224576 3221223488 134565745 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6469 603 41 0 6841 0 vsize: 27528 [startup+290.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6491 0 0 0 28981 20 0 0 25 0 1 0 421314266 28188672 6469 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6469 603 41 0 6841 0 vsize: 27528 [startup+300.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6491 0 0 0 29982 20 0 0 25 0 1 0 421314266 28188672 6469 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6469 603 41 0 6841 0 vsize: 27528 [startup+310.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 6491 0 0 0 30982 20 0 0 25 0 1 0 421314266 28188672 6469 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6882 6469 603 41 0 6841 0 vsize: 27528 [startup+320.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 7159 0 0 0 31980 22 0 0 25 0 1 0 421314266 31010816 7137 4294967295 134512640 134672761 3221224576 3221223620 1075755419 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7571 7137 603 41 0 7530 0 vsize: 30284 [startup+330.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 7847 0 0 0 32978 24 0 0 25 0 1 0 421314266 33804288 7825 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8253 7825 603 41 0 8212 0 vsize: 33012 [startup+340.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8467 0 0 0 33976 26 0 0 25 0 1 0 421314266 36343808 8445 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8873 8445 603 41 0 8832 0 vsize: 35492 [startup+350.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8542 0 0 0 34976 27 0 0 25 0 1 0 421314266 36614144 8520 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8520 603 41 0 8898 0 vsize: 35756 [startup+360.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8542 0 0 0 35977 27 0 0 25 0 1 0 421314266 36614144 8520 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8520 603 41 0 8898 0 vsize: 35756 [startup+370.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8542 0 0 0 36977 27 0 0 25 0 1 0 421314266 36614144 8520 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8520 603 41 0 8898 0 vsize: 35756 [startup+380.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8542 0 0 0 37976 27 0 0 25 0 1 0 421314266 36614144 8520 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8939 8520 603 41 0 8898 0 vsize: 35756 [startup+390.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 38975 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223728 134565212 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+400.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 39975 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+410.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 40975 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+420.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 41975 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+430.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 42975 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+440.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 43976 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+450.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 44976 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+460.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 45976 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+470.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 46976 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+480.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 47976 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+490.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 48976 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+500.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 49977 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+510.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 50977 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+520.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 51977 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+530.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 52977 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+540.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 53978 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560926 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+550.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 54978 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223712 134560640 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+560.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 55978 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+570.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 56978 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+580.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 57978 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+590.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 58979 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+600.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 59979 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+610.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 60979 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223680 134559829 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+620.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 61979 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+630.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 62979 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+640.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 63980 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+650.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 64980 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+660.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 65980 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+670.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 66981 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+680.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 67981 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+690.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8545 0 0 0 68980 27 0 0 25 0 1 0 421314266 36614144 8523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8939 8523 603 41 0 8898 0 vsize: 35756 [startup+700.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8547 0 0 0 69980 27 0 0 25 0 1 0 421314266 36614144 8525 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8525 603 41 0 8898 0 vsize: 35756 [startup+710.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8551 0 0 0 70980 27 0 0 25 0 1 0 421314266 36614144 8529 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8529 603 41 0 8898 0 vsize: 35756 [startup+720.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8551 0 0 0 71980 27 0 0 25 0 1 0 421314266 36614144 8529 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8529 603 41 0 8898 0 vsize: 35756 [startup+730.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8551 0 0 0 72980 27 0 0 25 0 1 0 421314266 36614144 8529 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8529 603 41 0 8898 0 vsize: 35756 [startup+740.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8551 0 0 0 73980 27 0 0 25 0 1 0 421314266 36614144 8529 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8529 603 41 0 8898 0 vsize: 35756 [startup+750.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8551 0 0 0 74981 27 0 0 25 0 1 0 421314266 36614144 8529 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8529 603 41 0 8898 0 vsize: 35756 [startup+760.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8551 0 0 0 75981 27 0 0 25 0 1 0 421314266 36614144 8529 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8529 603 41 0 8898 0 vsize: 35756 [startup+770.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8551 0 0 0 76981 27 0 0 25 0 1 0 421314266 36614144 8529 4294967295 134512640 134672761 3221224576 3221223744 134560845 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8529 603 41 0 8898 0 vsize: 35756 [startup+780.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8551 0 0 0 77981 27 0 0 25 0 1 0 421314266 36614144 8529 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8529 603 41 0 8898 0 vsize: 35756 [startup+790.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8551 0 0 0 78981 27 0 0 25 0 1 0 421314266 36614144 8529 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8939 8529 603 41 0 8898 0 vsize: 35756 [startup+800.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 8765 0 0 0 79981 28 0 0 25 0 1 0 421314266 37552128 8743 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9168 8743 603 41 0 9127 0 vsize: 36672 [startup+810.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 9518 0 0 0 80979 30 0 0 25 0 1 0 421314266 40534016 9496 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9896 9496 603 41 0 9855 0 vsize: 39584 [startup+820.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 10216 0 0 0 81977 32 0 0 25 0 1 0 421314266 43503616 10194 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10621 10194 603 41 0 10580 0 vsize: 42484 [startup+830.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 10859 0 0 0 82976 34 0 0 25 0 1 0 421314266 46178304 10837 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11274 10837 603 41 0 11233 0 vsize: 45096 [startup+840.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 11583 0 0 0 83974 35 0 0 25 0 1 0 421314266 49135616 11561 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11996 11561 603 41 0 11955 0 vsize: 47984 [startup+850.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 12199 0 0 0 84973 37 0 0 25 0 1 0 421314266 51560448 12177 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12588 12177 603 41 0 12547 0 vsize: 50352 [startup+860.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 12845 0 0 0 85972 38 0 0 25 0 1 0 421314266 54239232 12823 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13242 12823 603 41 0 13201 0 vsize: 52968 [startup+870.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13459 0 0 0 86971 40 0 0 25 0 1 0 421314266 56889344 13437 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13889 13437 603 41 0 13848 0 vsize: 55556 [startup+880.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 87970 41 0 0 25 0 1 0 421314266 58142720 13721 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14195 13721 603 41 0 14154 0 vsize: 56780 [startup+890.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 88970 41 0 0 25 0 1 0 421314266 58142720 13721 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14195 13721 603 41 0 14154 0 vsize: 56780 [startup+900.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 89970 41 0 0 25 0 1 0 421314266 58142720 13721 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14195 13721 603 41 0 14154 0 vsize: 56780 [startup+910.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 90970 41 0 0 25 0 1 0 421314266 58142720 13721 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14195 13721 603 41 0 14154 0 vsize: 56780 [startup+920.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 91971 41 0 0 25 0 1 0 421314266 58142720 13721 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14195 13721 603 41 0 14154 0 vsize: 56780 [startup+930.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 92971 41 0 0 25 0 1 0 421314266 58142720 13721 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14195 13721 603 41 0 14154 0 vsize: 56780 [startup+940.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 93971 41 0 0 25 0 1 0 421314266 58142720 13721 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14195 13721 603 41 0 14154 0 vsize: 56780 [startup+950.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 94971 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+960.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 95971 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+970.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 96972 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+980.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 97972 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+990.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 98972 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1000.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 99972 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1010.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 100973 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 101973 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 102973 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1040.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 103973 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1050.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 104973 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1060.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 105974 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1070.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 106974 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1080.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 107974 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1090.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 108974 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1100.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 109974 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1110.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 110975 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1120.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 111974 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1130.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13743 0 0 0 112974 41 0 0 25 0 1 0 421314266 58077184 13721 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13721 603 41 0 14138 0 vsize: 56716 [startup+1140.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13746 0 0 0 113974 41 0 0 25 0 1 0 421314266 58077184 13724 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13724 603 41 0 14138 0 vsize: 56716 [startup+1150.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13746 0 0 0 114975 41 0 0 25 0 1 0 421314266 58077184 13724 4294967295 134512640 134672761 3221224576 3221223760 134558831 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13724 603 41 0 14138 0 vsize: 56716 [startup+1160.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13746 0 0 0 115975 41 0 0 25 0 1 0 421314266 58077184 13724 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13724 603 41 0 14138 0 vsize: 56716 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13746 0 0 0 116975 41 0 0 25 0 1 0 421314266 58077184 13724 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13724 603 41 0 14138 0 vsize: 56716 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13746 0 0 0 117975 41 0 0 25 0 1 0 421314266 58077184 13724 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13724 603 41 0 14138 0 vsize: 56716 [startup+1190.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13746 0 0 0 118975 41 0 0 25 0 1 0 421314266 58077184 13724 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13724 603 41 0 14138 0 vsize: 56716 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25828 Raw data (stat): 25828 (minisat+) R 25827 22932 22931 0 -1 0 13747 0 0 0 119976 41 0 0 25 0 1 0 421314266 58077184 13725 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14179 13725 603 41 0 14138 0 vsize: 56716 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 25828 Raw data (stat): 25828 (minisat+) Z 25827 22932 22931 0 -1 12 13750 0 0 0 119976 44 0 0 25 0 1 0 421314266 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.07 CPU time (s): 1200.21 CPU user time (s): 1199.76 CPU system time (s): 0.442932 CPU usage (%): 100.011 Max. virtual memory (Kb): 56780 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####